/usr/share/doc/mace2/anldp.html is in mace2 3.3f-1.1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
"http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>
<TITLE>A Davis-Putnam Program
and Its Application to
Finite First-Order Model Search:
Quasigroup Existence Problems
</TITLE>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
<META name="GENERATOR" content="hevea 1.10">
<STYLE type="text/css">
.li-itemize{margin:1ex 0ex;}
.li-enumerate{margin:1ex 0ex;}
.dd-description{margin:0ex 0ex 1ex 4ex;}
.dt-description{margin:0ex;}
.toc{list-style:none;}
.thefootnotes{text-align:left;margin:0ex;}
.dt-thefootnotes{margin:0em;}
.dd-thefootnotes{margin:0em 0em 0em 2em;}
.footnoterule{margin:1em auto 1em 0px;width:50%;}
.caption{padding-left:2ex; padding-right:2ex; margin-left:auto; margin-right:auto}
.title{margin:2ex auto;text-align:center}
.center{text-align:center;margin-left:auto;margin-right:auto;}
.flushleft{text-align:left;margin-left:0ex;margin-right:auto;}
.flushright{text-align:right;margin-left:auto;margin-right:0ex;}
DIV TABLE{margin-left:inherit;margin-right:inherit;}
PRE{text-align:left;margin-left:0ex;margin-right:auto;}
BLOCKQUOTE{margin-left:4ex;margin-right:4ex;text-align:left;}
TD P{margin:0px;}
.boxed{border:1px solid black}
.textboxed{border:1px solid black}
.vbar{border:none;width:2px;background-color:black;}
.hbar{border:none;height:2px;width:100%;background-color:black;}
.hfill{border:none;height:1px;width:200%;background-color:black;}
.vdisplay{border-collapse:separate;border-spacing:2px;width:auto; empty-cells:show; border:2px solid red;}
.vdcell{white-space:nowrap;padding:0px;width:auto; border:2px solid green;}
.display{border-collapse:separate;border-spacing:2px;width:auto; border:none;}
.dcell{white-space:nowrap;padding:0px;width:auto; border:none;}
.dcenter{margin:0ex auto;}
.vdcenter{border:solid #FF8000 2px; margin:0ex auto;}
.minipage{text-align:left; margin-left:0em; margin-right:auto;}
.marginpar{border:solid thin black; width:20%; text-align:left;}
.marginparleft{float:left; margin-left:0ex; margin-right:1ex;}
.marginparright{float:right; margin-left:1ex; margin-right:0ex;}
.theorem{text-align:left;margin:1ex auto 1ex 0ex;}
.part{margin:2ex auto;text-align:center}
</STYLE>
</HEAD>
<BODY >
<!--HEVEA command line is: /usr/bin/hevea otter33.hva anldp.tex -->
<!--CUT DEF section 1 --><TABLE CLASS="title"><TR><TD><H1 CLASS="titlemain"><FONT SIZE=5><B>A Davis-Putnam Program<BR>
and Its Application to
Finite First-Order Model Search:
Quasigroup Existence Problems</B></FONT><SUP><A NAME="text1" HREF="#note1">*</A></SUP></H1><H3 CLASS="titlerest"><I>William McCune</I><BR><BR>
Mathematics and Computer Science Division<BR>
Argonne National Laboratory<BR>
Argonne, Illinois 60439-4844, U.S.A.<BR>
e-mail: mccune@mcs.anl.gov<BR>
phone: 708-252-3065</H3><H3 CLASS="titlerest">September 1994</H3></TD></TR>
</TABLE><BLOCKQUOTE CLASS="abstract"><B>Abstract: </B>
This document describes the implementation and use of a Davis-Putnam
procedure for the propositional satisfiability problem. It also
describes code that takes statements in first-order logic with
equality and a domain size <I>n</I> then searches for models of size <I>n</I>. The
first-order model-searching code transforms the statements into set of
propositional clauses such that the first-order statements have a
model of size <I>n</I> if and only if the propositional clauses are
satisfiable. The propositional set is then given to the Davis-Putnam
code; any propositional models that are found can be translated to
models of the first-order statements.
The first-order model-searching program accepts statements only in a
flattened relational clause form without function symbols. Additional
code was written to take input statements in the language of <SPAN STYLE="font-variant:small-caps">Otter</SPAN> 3.0
and produce the flattened relational form.
The program was successfully applied to several open questions
on the existence of orthogonal quasigroups.
</BLOCKQUOTE><!--TOC section The Davis-Putnam Procedure-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc1">1</A>  The Davis-Putnam Procedure</H2><!--SEC END --><P>The Davis-Putnam procedure is widely regarded as the best method
for deciding the satisfiability of a set of propositional clauses.
I’ll assume that the reader is familiar with it. I list here some
features of our implementation.
</P><OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
There are no checks for pure literals. Experience has shown that
such checks are usually more expensive than they are worth.
</LI><LI CLASS="li-enumerate">Deletion of subsumed clauses is optional. Again, experience
has shown that it is too expensive.
</LI><LI CLASS="li-enumerate">The variable selected for splitting is the always first literal
of the first, shortest positive clause.
</LI></OL><!--TOC subsection Implementation-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc2">1.1</A>  Implementation</H3><!--SEC END --><P>The data structures for clauses and for propositional variables and
the algorithms are similar to the ones Mark Stickel uses in LDPP
[<A HREF="#dp-trie">8</A>].</P><P>Variables are integers ≥ 1. Associated with the set of variables
is an array, indexed by the variables, of variable structures. Each
variable structure contains the following fields.
</P><UL CLASS="itemize"><LI CLASS="li-itemize">
<CODE>value</CODE>.
The current value (true, false, or unassigned) of the variable.
</LI><LI CLASS="li-itemize"><CODE>enqueued_value</CODE>.
A field to speed the bottleneck operation of unit propagation (see below).
</LI><LI CLASS="li-itemize"><CODE>pos_occ</CODE>.
A list of pointers to clauses that contain the
variable in a positive literal.
</LI><LI CLASS="li-itemize"><CODE>neg_occ</CODE>.
A list of pointers to clauses that contain the
variable in a negative literal.
</LI></UL><P>
Each clause contains the following fields.
</P><UL CLASS="itemize"><LI CLASS="li-itemize">
<CODE>pos</CODE>.
A list of variables representing positive literals.
</LI><LI CLASS="li-itemize"><CODE>neg</CODE>.
A list of variables representing negative literals.
</LI><LI CLASS="li-itemize"><CODE>active_pos</CODE>.
The number of positive literals that have not been resolved away.
</LI><LI CLASS="li-itemize"><CODE>active_neg</CODE>.
The number of negative literals that have not been resolved away.
</LI><LI CLASS="li-itemize"><CODE>subsumer</CODE>.
A field set to the responsible variable if the clause has been
inactivated by subsumption.
</LI></UL><!--TOC paragraph Assignment.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Assignment.</H5><!--SEC END --><P>
When a variable is assigned a value, say true, by splitting or during
unit propagation, unit resolution is performed by traversing the
<CODE>neg_occ</CODE> list of the variable: for each clause that has not
been subsumed, the <CODE>active_neg</CODE> field is simply decremented by 1.
If <CODE>active_pos+active_neg</CODE> becomes 0, the empty clause has been
found and backtracking occurs. If <CODE>active_pos+active_neg</CODE>
becomes 1, the new unit clause is queued for unit propagation. In
addition, if subsumption is enabled, (back) subsumption is performed
by traversing the
<CODE>pos_occ</CODE> list of the variable: for each clause that is not
already subsumed, the <CODE>subsumer</CODE> field is set to the variable.
Variables must be unassigned during backtracking, and the process is
essentially the reverse of assignment.</P><!--TOC paragraph Unit Propagation.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Unit Propagation.</H5><!--SEC END --><P>
A split causes an assignment. The unit propagation queue is then
processed (causing further assignments and possibly more units to be
queued) until empty or the empty clause is found. Each split
typically causes many assignments, so unit propagation must be done
efficiently. To avoid duplicates in the queue, and to detect
the empty clause during the enqueue operation rather than during
assignment, we set the field <CODE>enqueued_value</CODE> of the variable
when the corresponding literal is enqueued. That way we can quickly
tell whether a literal or its complement is already in the queue.</P><!--TOC paragraph Unit Preprocessing.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Unit Preprocessing.</H5><!--SEC END --><P>
If the set of input clauses contains any units, unit propagation is
applied. During assignment, back subumption is always applied,
because assignments made during this phase are never undone.</P><!--TOC paragraph Selecting Variables for Splitting.-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Selecting Variables for Splitting.</H5><!--SEC END --><P>
The variable selected for splitting is the first literal in the first,
shortest nonsubsumed positive clause. After the unit preprocessing,
pointers to all of the non-Horn clauses (i.e., clauses with two or more
positive literals) are collected into a list. In order to select a variable
for splitting, the list is simply traversed. Subsumed clauses must be
ignored; if subsumption is enabled, the subsumer field is checked;
otherwise the clause is scanned for a literal with value true.
(If all clauses in the list are subsumed, a model has been found.)</P><!--TOC subsection Pigeonhole Problems-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc3">1.2</A>  Pigeonhole Problems</H3><!--SEC END --><P>The pigeonhole problems are a set of artificial propositional problems
that are used to test the efficiency of propositional theorem provers.
See the sample input files that come with ANL-DP for examples. Table
<A HREF="#pigeon">1</A> lists the performance of ANL-DP on several instances of
the pigeonhole problems. The jobs were run on a SPARC 2.</P><BLOCKQUOTE CLASS="table"><DIV CLASS="center"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV> <DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Table 1: ANL-DP on the Pigeonhole Problems</TD></TR>
</TABLE></DIV> <A NAME="pigeon"></A>
<TABLE CELLSPACING=6 CELLPADDING=0><TR><TD ALIGN=left NOWRAP> </TD><TD ALIGN=right NOWRAP>Branches</TD><TD ALIGN=right NOWRAP>Seconds</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=3></TD></TR>
<TR><TD ALIGN=left NOWRAP>7 pigeons, 6 holes</TD><TD ALIGN=right NOWRAP>719</TD><TD ALIGN=right NOWRAP>.15</TD></TR>
<TR><TD ALIGN=left NOWRAP>8 pigeons, 7 holes</TD><TD ALIGN=right NOWRAP>5039</TD><TD ALIGN=right NOWRAP>1.14</TD></TR>
<TR><TD ALIGN=left NOWRAP>9 pigeons, 8 holes</TD><TD ALIGN=right NOWRAP>40319</TD><TD ALIGN=right NOWRAP>9.16</TD></TR>
<TR><TD ALIGN=left NOWRAP>10 pigeons, 9 holes</TD><TD ALIGN=right NOWRAP>362879</TD><TD ALIGN=right NOWRAP>88.43</TD></TR>
<TR><TD ALIGN=left NOWRAP>11 pigeons, 10 holes</TD><TD ALIGN=right NOWRAP>3628799</TD><TD ALIGN=right NOWRAP>916.62</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=3></TD></TR>
</TABLE>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></DIV></BLOCKQUOTE><!--TOC subsection Using ANL-DP-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc4">1.3</A>  Using ANL-DP</H3><!--SEC END --><P> <A NAME="use-prop"></A></P><P>Propositional input to ANL-DP is a sequence of clauses.
(See Sec. <A HREF="#use-fo">2.2</A> for input to the first-order model-searching program.)
Literals are nonzero integers (negative integers represent negative
literals), and each clause is terminated with 0.
(Hence, the entire input is just a sequence of integers.)
The input is taken from <CODE>stdin</CODE> (the standard input).</P><P>ANL-DP accepts the following command-line options.
</P><DL CLASS="description"><DT CLASS="dt-description">
</DT><DD CLASS="dd-description"><CODE>-s</CODE>.
Perform subsumption. (Subsumption is always performed during unit preprocessing.)
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-p</CODE>.
Print models as they are found.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-m</CODE> <I>n</I>.
Stop when the <I>n</I>-th model is found.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-t</CODE> <I>n</I>.
Stop after <I>n</I> seconds.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-k</CODE> <I>n</I>.
Allocate at most <I>n</I> kbytes for storage of clauses.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-x</CODE> <I>n</I>.
Quasigroup experiment <I>n</I>. See Section <A HREF="#qg">2.5</A>.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-B</CODE> <I>file</I>.
Backup assignments to a file.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-b</CODE> <I>n</I>.
Backup assignments every <I>n</I> seconds.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-R</CODE> <I>file</I>.
Restore assignments from a file. The file typically contains just the
last line of a backup file. Other input, in particular the clauses,
must be given exactly as in the original search.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>-n</CODE> <I>n</I>.
This option is used for first-order model searches. The parameter <I>n</I>
specifies the domain size, and its presence tells the program to
read first-order flattened relational input clauses instead of propositional
clauses.
</DD></DL><!--TOC section The First-Order Model-Searching Program-->
<H2 CLASS="section"><!--SEC ANCHOR --><A NAME="htoc5">2</A>  The First-Order Model-Searching Program</H2><!--SEC END --><P>The first practical program for searching for small models of
first-order statements was FINDER [<A HREF="#finder3">6</A>]. Another
model-searching program is MGTP [<A HREF="#qg-slaney-fujita-stickel">7</A>], which
uses a somewhat different approach. The third class of programs,
including LDPP
[<A HREF="#dp-trie">8</A>], SATO [<A HREF="#dp-trie">8</A>], and the one described here, are based
on Davis-Putnam procedures. None of these programs is clearly better
than the others, and each has answered open questions about
quasigroups (see Sec. <A HREF="#qg">2.5</A>).</P><P>The Davis-Putnam approach is quite elegant, because the computational
engine—the Davis-Putnam code—is in no way tailored to
first-order model searching. First-order clauses and a domain
size <I>n</I> are input; then ground instances (over the domain) of the first-order
clauses are generated and given to the Davis-Putnam code. Any
propositional models that are found can be easily translated to
first-order models (e.g., an <I>n</I>× <I>n</I> table for a binary function).</P><P>The steps, which are summarized in Figure <A HREF="#trans">1</A>, are as follows.</P><BLOCKQUOTE CLASS="figure"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
<IMG SRC="anldp001.png"><DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Figure 1: Searching for First-Order Models</TD></TR>
</TABLE></DIV> <A NAME="trans"></A>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE><OL CLASS="enumerate" type=1><LI CLASS="li-enumerate">
Take an arbitrary first-order formula (possibly involving equality),
and produce a set of clauses. <SPAN STYLE="font-variant:small-caps">Otter</SPAN>’s clausification code is
sufficient for this.
</LI><LI CLASS="li-enumerate">
Take a set of first-order clauses, and produce a set of flattened,
relational clauses that
contain no constants or function symbols—all arguments of
the literals are variables. The steps are as follows:
<OL CLASS="enumerate" type=a><LI CLASS="li-enumerate">
For each <I>n</I>-ary function symbol
(including constants), an <I>n</I>+1-ary predice symbol is introduced.
For the examples, function symbols are lower-case letters, and new predicate
symbols are the corresponding upper-case letters.
</LI><LI CLASS="li-enumerate">
To flatten the clauses, the following kind of equality
transformation is applied to nonvariable terms (excepting arguments
of positive equalities): <I>P</I>[<I>t</I>] is rewritten to <I>t</I>≠ <I>x</I>   |  <I>P</I>[<I>x</I>].
</LI><LI CLASS="li-enumerate">
A clause containing a positive equality α=β, where both arguments
are nonvariable,
is made into two clauses: <I>L</I> | α=β becomes
<I>L</I> | α≠ <I>x</I> | β=<I>x</I> and <I>L</I> | β≠ <I>x</I> | α=<I>x</I>.
</LI><LI CLASS="li-enumerate">
Each functional literal, say <I>f</I>(<I>x</I>,<I>y</I>)=<I>z</I>, is rewritten into its
relational form, say <I>F</I>(<I>x</I>,<I>y</I>,<I>z</I>). (The resulting clauses may contain
ordinary equality literals as well.)
</LI></OL>
For example, the equality <I>f</I>(<I>g</I>(<I>x</I>),<I>x</I>)=<I>e</I> produces the two clauses
<BLOCKQUOTE CLASS="quote">
¬ <I>G</I>(<I>x</I>,<I>y</I>)  | ¬ <I>E</I>(<I>z</I>)  | <I>F</I>(<I>y</I>,<I>x</I>,<I>z</I>)<BR>
¬ <I>G</I>(<I>x</I>,<I>y</I>)  | <I>E</I>(<I>z</I>)  | ¬ <I>F</I>(<I>y</I>,<I>x</I>,<I>z</I>)
</BLOCKQUOTE>
</LI><LI CLASS="li-enumerate">
Take a set of flattened relational clauses and a domain size, and
generate a set of propositional clauses. For each relational clause,
the set of instances over the domain is constructed. (With domain
size <I>n</I>, a clause with <I>m</I> variables produces <I>n</I><SUP><I>m</I></SUP> instances.) Each
atom is encoded into a unique integer that becomes the propositional
variable. Also, we must assert that the (<I>n</I>+1)-ary predicates
introduced above represent total functions, so for each, we assert two
sets of propositional clauses. For example, for ternary relation <I>F</I>,
we must say that the last argument is a function of the others,
<BLOCKQUOTE CLASS="quote">
¬ <I>F</I>(<I>x</I>,<I>y</I>,<I>z</I><SUB>1</SUB>)  |  ¬ <I>F</I>(<I>x</I>,<I>y</I>,<I>z</I><SUB>2</SUB>), for <I>z</I><SUB>1</SUB> < <I>z</I><SUB>2</SUB> (well-defined)
</BLOCKQUOTE>
and that the function is total and its value always lies in the domain
(elements of the domain are named 0, 1, ⋯, <I>n</I>−1):
<BLOCKQUOTE CLASS="quote">
<I>F</I>(<I>x</I>,<I>y</I>,0)  |  <I>F</I>(<I>x</I>,<I>y</I>,1)  |  ⋯  |  <I>F</I>(<I>x</I>,<I>y</I>,<I>n</I>−1) (closed and total).
</BLOCKQUOTE>
If the flattened relational clauses contain any equality literals,
the <I>n</I><SUP>2</SUP> units for the equality relation are asserted.
Nothing special needs to be done for ordinary predicate symbols.
</LI><LI CLASS="li-enumerate">
The Davis-Putnam procedure searches for models of the propositional
clauses.
</LI><LI CLASS="li-enumerate">
For each propositional model, we generate the corresponding first-order model.
The clauses given in (3) above ensure that from the propositional model,
we can build a function for each function symbol (including constants).
</LI></OL><!--TOC subsection Additional Constraints-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc6">2.1</A>  Additional Constraints</H3><!--SEC END --><P>For various reasons, the most important being to reduce the number of
isomorphic models that are found, the user can specify part of the
model by supplying ground clauses over the domain. For example,
if a noncommutative group is being sought, with constants <I>a</I> and <I>b</I>
as noncommuting elements,
the user can assign 0 to the identity, 1 to <I>a</I>, and 2 to <I>b</I>.
In this case, nothing is lost by making them distinct.</P><P>Symbols can be given the following properties.
</P><DL CLASS="description"><DT CLASS="dt-description">
</DT><DD CLASS="dd-description"><CODE>quasigroup</CODE>.
This can be applied to ternary relations that represent binary functions.
The multiplication table of a quasigroup has one of each element in each
row and each column.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>bijection</CODE>.
This can be applied to binary relations that represent unary functions.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>equality</CODE>.
This can be applied to binary relations. It is just equality of domain
elements.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>order</CODE>.
This can be applied to binary relations. This is just the less-than
relation on the domain elements.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>holey</CODE>.
This can be applied to ternary relations that represent binary functions.
See Sec. <A HREF="#holey">2.5.2</A>.
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description"><CODE>hole</CODE>.
This can be applied to binary relations.
See Sec. <A HREF="#holey">2.5.2</A>.
</DD></DL><!--TOC subsection Using the Program to Search for First-Order Models-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc7">2.2</A>  Using the Program to Search for First-Order Models</H3><!--SEC END --><P> <A NAME="use-fo"></A></P><P>The first-order searcher is part of ANL-DP, and it is invoked
as described in Sec. <A HREF="#use-prop">1.3</A>. The command-line option
“<CODE>-n</CODE> <I>n</I>” specifies the domain size and indicates that
the input will be given as first-order flat clauses. Here is an
example input specifying a noncommutative group.
</P><PRE CLASS="verbatim"> function F 3 quasigroup
function E 1 -----
function G 2 bijection
function A 1 -----
function B 1 -----
end_of_symbols
-E v0 F v0 v1 v1 .
-E v0 -G v1 v2 F v2 v1 v0 .
E v0 -G v1 v2 -F v2 v1 v0 .
-F v0 v1 v2 -F v3 v2 v4 -F v3 v0 v5 F v5 v1 v4 .
-F v0 v1 v2 F v3 v2 v4 -F v3 v0 v5 -F v5 v1 v4 .
-F v0 v1 v2 -B v0 -A v1 -F v1 v0 v2 .
end_of_clauses
E 0
A 1
B 2
end_of_assignments
</PRE><DL CLASS="description"><DT CLASS="dt-description">
</DT><DD CLASS="dd-description">Symbol Declarations.
In the first section of the input, each symbol is declared with four
strings: type (<CODE>function</CODE> or <CODE>relation</CODE>), symbol, arity (<I>n</I>+1
for functions), and properties (<CODE>equality</CODE>, <CODE>order</CODE>,
<CODE>quasigroup</CODE>, <CODE>bijection</CODE>, or <CODE>-----</CODE>).
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description">Clauses.
Flat relational clauses appear in the second section. Variables can
be any strings. <EM>Whitespace is required before the periods that
terminates clauses.</EM>
</DD><DT CLASS="dt-description"></DT><DD CLASS="dd-description">Assignments.
Ground units (without periods) can appear in the third section.
</DD></DL><!--TOC subsection Using <SPAN STYLE="font-variant:small-caps">Otter</SPAN> to Generate the Flat Clauses-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc8">2.3</A>  Using <SPAN STYLE="font-variant:small-caps">Otter</SPAN> to Generate the Flat Clauses</H3><!--SEC END --><P><SPAN STYLE="font-variant:small-caps">Otter</SPAN> 3.0.2 [<A HREF="#otter3">5</A>] and later versions can take ordinary formulas or
clauses and produce the flat relational clauses for input to ANL-DP.
Here is an <SPAN STYLE="font-variant:small-caps">Otter</SPAN> input file for a noncommutative group that will
produce something like the file in Sec. <A HREF="#use-fo">2.2</A>.
</P><PRE CLASS="verbatim"> set(dp_transform).
list(usable).
f(e,x) = x.
f(g(x),x) = e.
f(f(x,y),z) = f(x,f(y,z)).
f(a,b) != f(b,a).
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
properties(g(_), bijection).
assign(e, 0).
assign(a, 1).
assign(b, 2).
end_of_list.
</PRE><P>The command <CODE>set(dp_transform)</CODE> tells <SPAN STYLE="font-variant:small-caps">Otter</SPAN> to generate
input for an ANL-DP search and then exit. </P><P>The output of <SPAN STYLE="font-variant:small-caps">Otter</SPAN> contains extraneous text, so it must be passed
though a filter before ANL-DP can receive it. See the example files
and scripts in the distribution directories.</P><!--TOC subsection The Order Relation-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc9">2.4</A>  The Order Relation</H3><!--SEC END --><P> <A NAME="order"></A></P><P>The ordered semigroup example in the FINDER 3.0 manual
[<A HREF="#finder3">6</A>, Sec. 4.1.5] motivated me to have ANL-DP recognize the
less-than relation on domain elements. The input (in <SPAN STYLE="font-variant:small-caps">Otter</SPAN> form)
for the ordered semigroup problems is as follows.
</P><PRE CLASS="verbatim"> set(dp_transform).
list(usable).
f(f(x,y),z) = f(x,f(y,z)).
-(f(x,y) < f(x,z)) | y < z.
-(f(y,x) < f(z,x)) | y < z.
end_of_list.
</PRE><P>(<SPAN STYLE="font-variant:small-caps">Otter</SPAN> recognizes <CODE><</CODE> as the order relation and gives it
the property “order” in its output.)
Table <A HREF="#order-tab">2</A> compares the results of FINDER and ANL-DP, both
run on SPARC 2 computers, on the ordered semigroup problems. FINDER’s
search algorithm was developed with this type of problem in mind;
ANL-DP simply adds the <I>n</I><SUP>2</SUP> unit clauses for the less-than relation.
I believe this distinction explains most of the disparity of the
times.</P><BLOCKQUOTE CLASS="table"><DIV CLASS="center"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV> <DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Table 2: Ordered Semigroup Problems – FINDER vs. ANL-DP</TD></TR>
</TABLE></DIV> <A NAME="order-tab"></A>
<TABLE CELLSPACING=6 CELLPADDING=0><TR><TD ALIGN=center NOWRAP>Order</TD><TD ALIGN=right NOWRAP>Models</TD><TD ALIGN=right NOWRAP>FINDER</TD><TD ALIGN=right NOWRAP>ANL-DP</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=4></TD></TR>
<TR><TD ALIGN=center NOWRAP>3</TD><TD ALIGN=right NOWRAP>44</TD><TD ALIGN=right NOWRAP>0.1</TD><TD ALIGN=right NOWRAP>0.1</TD></TR>
<TR><TD ALIGN=center NOWRAP>4</TD><TD ALIGN=right NOWRAP>386</TD><TD ALIGN=right NOWRAP>0.6</TD><TD ALIGN=right NOWRAP>2.6</TD></TR>
<TR><TD ALIGN=center NOWRAP>5</TD><TD ALIGN=right NOWRAP>3852</TD><TD ALIGN=right NOWRAP>9.2</TD><TD ALIGN=right NOWRAP>58.0</TD></TR>
</TABLE>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></DIV></BLOCKQUOTE><!--TOC subsection Application to Quasigroup Problems-->
<H3 CLASS="subsection"><!--SEC ANCHOR --><A NAME="htoc10">2.5</A>  Application to Quasigroup Problems</H3><!--SEC END --><P> <A NAME="qg"></A></P><P>In the multiplication table of an order-<I>n</I> quasigroup, each row and
each column are a permutation of the <I>n</I> elements. For these problems,
we are interested only in idempotent (i.e., <I>xx</I>=<I>x</I>) models.
Additional constraints are given for the seven problems listed in
Table <A HREF="#qg-tab">3</A>. (Notes: (1) For QG1 and QG2, the disjunction to
the right of the implication is ordinarily a conjunction; the forms
are equivalent for quasigroups, and models are found more
easily with disjunction. (2) The second and third equalities for QG5
and the second equality for QG7 are dependent.) See [<A HREF="#qg-survey">2</A>] and
[<A HREF="#qg-slaney-fujita-stickel">7</A>] for details on the quasigroup problems.</P><BLOCKQUOTE CLASS="table"><DIV CLASS="center"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV> <DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Table 3: The Quasigroup Problems</TD></TR>
</TABLE></DIV> <A NAME="qg-tab"></A>
<TABLE CELLSPACING=6 CELLPADDING=0><TR><TD ALIGN=left NOWRAP>Name</TD><TD ALIGN=left NOWRAP>Constraints</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=2></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG1</TD><TD ALIGN=left NOWRAP><I>xy</I>=<I>u</I>  ∧  <I>zw</I>=<I>u</I>  ∧  <I>vy</I>=<I>x</I>  ∧  <I>vw</I>= <I>z</I> → <I>x</I>=<I>z</I>  ∨  <I>y</I>=<I>w</I></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG2</TD><TD ALIGN=left NOWRAP><I>xy</I>=<I>u</I>  ∧  <I>zw</I>=<I>u</I>  ∧  <I>vx</I>=<I>y</I>  ∧  <I>vz</I>= <I>w</I> → <I>x</I>=<I>z</I>  ∨  <I>y</I>=<I>w</I></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG3</TD><TD ALIGN=left NOWRAP>(<I>xy</I>)(<I>yx</I>)=<I>x</I></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG4</TD><TD ALIGN=left NOWRAP>(<I>xy</I>)(<I>yx</I>)=<I>y</I></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG5</TD><TD ALIGN=left NOWRAP>((<I>xy</I>)<I>x</I>)<I>x</I>=<I>y</I>  ∧  <I>x</I>((<I>yx</I>)<I>x</I>)=<I>y</I>  ∧  (<I>x</I>(<I>yx</I>))<I>x</I>=<I>y</I></TD></TR>
<TR><TD ALIGN=left NOWRAP>QG6</TD><TD ALIGN=left NOWRAP>(<I>xy</I>)<I>y</I> = <I>x</I>(<I>xy</I>)</TD></TR>
<TR><TD ALIGN=left NOWRAP>QG7</TD><TD ALIGN=left NOWRAP>((<I>xy</I>)<I>x</I>)<I>y</I>=<I>x</I>  ∧  ((<I>xy</I>)<I>y</I>)(<I>xy</I>)=<I>x</I></TD></TR>
<TR><TD CLASS="hbar" COLSPAN=2></TD></TR>
</TABLE>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></DIV></BLOCKQUOTE><P>We also used the following cycle constraint on the last column to
eliminate some isomorphic models [<A HREF="#qg-slaney-fujita-stickel">7</A>]:
</P><BLOCKQUOTE CLASS="quote">
¬ <I>f</I>(<I>x</I>,<I>n</I>,<I>z</I>), for <I>z</I> < <I>x</I>−1.
</BLOCKQUOTE><P>
The constraint requires that cycles in the last column be made up
of contiguous elements. This constraint is specified to ANL-DP with
the command-line option “<CODE>-x1</CODE>”; <EM>the quasigroup operation
must be </EM><CODE><EM>f</EM></CODE><EM> (lower-case) for this to work</EM>.</P><P>Table <A HREF="#qg-tab-compare">4</A> gives summaries of the performance of
ANL-DP (C, list structure), SATO-2 (C, trie structure), and LDPP′
(Lisp, list structure) on some cases of the quasigroup problems.
The SATO and LDPP figures are taken from [<A HREF="#dp-trie">8</A>].
All runs were made on a SPARC 2 or similar computer. All programs used
the cycle constraint and similar selection functions for splitting. I
believe that differences in the number of branches are due mostly to
the order of clauses and literals. Search time is given in seconds.</P><BLOCKQUOTE CLASS="table"><DIV CLASS="center"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV> <DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Table 4: Quasigroup Problems – Comparison</TD></TR>
</TABLE></DIV> <A NAME="qg-tab-compare"></A>
<TABLE BORDER=1 CELLSPACING=0 CELLPADDING=1><TR><TD ALIGN=right NOWRAP> </TD><TD ALIGN=center NOWRAP> </TD><TD ALIGN=center NOWRAP COLSPAN=2>ANL-DP</TD><TD ALIGN=center NOWRAP COLSPAN=2>SATO-2</TD><TD ALIGN=center NOWRAP COLSPAN=2>LDPP′</TD></TR>
<TR><TD ALIGN=right NOWRAP> Problem</TD><TD ALIGN=center NOWRAP>Models</TD><TD ALIGN=right NOWRAP>Branches</TD><TD ALIGN=right NOWRAP>Search</TD><TD ALIGN=right NOWRAP>Branches</TD><TD ALIGN=right NOWRAP>Search</TD><TD ALIGN=right NOWRAP>Branches</TD><TD ALIGN=right NOWRAP>Search</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG1.7</TD><TD ALIGN=center NOWRAP>8</TD><TD ALIGN=right NOWRAP>388</TD><TD ALIGN=right NOWRAP>2.05</TD><TD ALIGN=right NOWRAP>376</TD><TD ALIGN=right NOWRAP>1</TD><TD ALIGN=right NOWRAP>389</TD><TD ALIGN=right NOWRAP>26</TD></TR>
<TR><TD ALIGN=right NOWRAP> .8</TD><TD ALIGN=center NOWRAP>16</TD><TD ALIGN=right NOWRAP>100731</TD><TD ALIGN=right NOWRAP>852.81</TD><TD ALIGN=right NOWRAP>102610</TD><TD ALIGN=right NOWRAP>379</TD><TD ALIGN=right NOWRAP>101129</TD><TD ALIGN=right NOWRAP>3463</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG2.7</TD><TD ALIGN=center NOWRAP>14</TD><TD ALIGN=right NOWRAP>361</TD><TD ALIGN=right NOWRAP>2.23</TD><TD ALIGN=right NOWRAP>340</TD><TD ALIGN=right NOWRAP>1</TD><TD ALIGN=right NOWRAP>205</TD><TD ALIGN=right NOWRAP>8</TD></TR>
<TR><TD ALIGN=right NOWRAP> .8</TD><TD ALIGN=center NOWRAP>2</TD><TD ALIGN=right NOWRAP>77158</TD><TD ALIGN=right NOWRAP>810.75</TD><TD ALIGN=right NOWRAP>80245</TD><TD ALIGN=right NOWRAP>341</TD><TD ALIGN=right NOWRAP>33835</TD><TD ALIGN=right NOWRAP>1358</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG3.8</TD><TD ALIGN=center NOWRAP>18</TD><TD ALIGN=right NOWRAP>1017</TD><TD ALIGN=right NOWRAP>2.82</TD><TD ALIGN=right NOWRAP>1072</TD><TD ALIGN=right NOWRAP>3</TD><TD ALIGN=right NOWRAP>573</TD><TD ALIGN=right NOWRAP>5</TD></TR>
<TR><TD ALIGN=right NOWRAP> .9</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>39461</TD><TD ALIGN=right NOWRAP>155.12</TD><TD ALIGN=right NOWRAP>48545</TD><TD ALIGN=right NOWRAP>157</TD><TD ALIGN=right NOWRAP>24763</TD><TD ALIGN=right NOWRAP>208</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG4.8</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>891</TD><TD ALIGN=right NOWRAP>2.40</TD><TD ALIGN=right NOWRAP>925</TD><TD ALIGN=right NOWRAP>2</TD><TD ALIGN=right NOWRAP>602</TD><TD ALIGN=right NOWRAP>4</TD></TR>
<TR><TD ALIGN=right NOWRAP> .9</TD><TD ALIGN=center NOWRAP>178</TD><TD ALIGN=right NOWRAP>52939</TD><TD ALIGN=right NOWRAP>209.76</TD><TD ALIGN=right NOWRAP>52826</TD><TD ALIGN=right NOWRAP>168</TD><TD ALIGN=right NOWRAP>27479</TD><TD ALIGN=right NOWRAP>228</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG5.9</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>14</TD><TD ALIGN=right NOWRAP>.22</TD><TD ALIGN=right NOWRAP>19</TD><TD ALIGN=right NOWRAP>.2</TD><TD ALIGN=right NOWRAP>15</TD><TD ALIGN=right NOWRAP>.4</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>37</TD><TD ALIGN=right NOWRAP>.52</TD><TD ALIGN=right NOWRAP>62</TD><TD ALIGN=right NOWRAP>.5</TD><TD ALIGN=right NOWRAP>38</TD><TD ALIGN=right NOWRAP>.9</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=center NOWRAP>5</TD><TD ALIGN=right NOWRAP>112</TD><TD ALIGN=right NOWRAP>2.16</TD><TD ALIGN=right NOWRAP>111</TD><TD ALIGN=right NOWRAP>2</TD><TD ALIGN=right NOWRAP>125</TD><TD ALIGN=right NOWRAP>5</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>369</TD><TD ALIGN=right NOWRAP>6.61</TD><TD ALIGN=right NOWRAP>369</TD><TD ALIGN=right NOWRAP>7</TD><TD ALIGN=right NOWRAP>369</TD><TD ALIGN=right NOWRAP>15</TD></TR>
<TR><TD ALIGN=right NOWRAP> .13</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>9588</TD><TD ALIGN=right NOWRAP>242.54</TD><TD ALIGN=right NOWRAP>10764</TD><TD ALIGN=right NOWRAP>224</TD><TD ALIGN=right NOWRAP>12686</TD><TD ALIGN=right NOWRAP>639</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG6.9</TD><TD ALIGN=center NOWRAP>4</TD><TD ALIGN=right NOWRAP>17</TD><TD ALIGN=right NOWRAP>.25</TD><TD ALIGN=right NOWRAP>24</TD><TD ALIGN=right NOWRAP>.2</TD><TD ALIGN=right NOWRAP>18</TD><TD ALIGN=right NOWRAP>.4</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>58</TD><TD ALIGN=right NOWRAP>.54</TD><TD ALIGN=right NOWRAP>150</TD><TD ALIGN=right NOWRAP>.7</TD><TD ALIGN=right NOWRAP>59</TD><TD ALIGN=right NOWRAP>.8</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>537</TD><TD ALIGN=right NOWRAP>5.36</TD><TD ALIGN=right NOWRAP>519</TD><TD ALIGN=right NOWRAP>6</TD><TD ALIGN=right NOWRAP>539</TD><TD ALIGN=right NOWRAP>11</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>7306</TD><TD ALIGN=right NOWRAP>95.41</TD><TD ALIGN=right NOWRAP>5728</TD><TD ALIGN=right NOWRAP>92</TD><TD ALIGN=right NOWRAP>7288</TD><TD ALIGN=right NOWRAP>177</TD></TR>
<TR><TD ALIGN=right NOWRAP> QG7.9</TD><TD ALIGN=center NOWRAP>4</TD><TD ALIGN=right NOWRAP>7</TD><TD ALIGN=right NOWRAP>.19</TD><TD ALIGN=right NOWRAP>7</TD><TD ALIGN=right NOWRAP>.2</TD><TD ALIGN=right NOWRAP>8</TD><TD ALIGN=right NOWRAP>.3</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>39</TD><TD ALIGN=right NOWRAP>.38</TD><TD ALIGN=right NOWRAP>54</TD><TD ALIGN=right NOWRAP>.4</TD><TD ALIGN=right NOWRAP>40</TD><TD ALIGN=right NOWRAP>.7</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>291</TD><TD ALIGN=right NOWRAP>2.98</TD><TD ALIGN=right NOWRAP>254</TD><TD ALIGN=right NOWRAP>3</TD><TD ALIGN=right NOWRAP>294</TD><TD ALIGN=right NOWRAP>6</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=center NOWRAP>-</TD><TD ALIGN=right NOWRAP>1578</TD><TD ALIGN=right NOWRAP>17.87</TD><TD ALIGN=right NOWRAP>1281</TD><TD ALIGN=right NOWRAP>22</TD><TD ALIGN=right NOWRAP>1592</TD><TD ALIGN=right NOWRAP>38</TD></TR>
<TR><TD ALIGN=right NOWRAP> .13</TD><TD ALIGN=center NOWRAP>64</TD><TD ALIGN=right NOWRAP>33946</TD><TD ALIGN=right NOWRAP>493.67</TD><TD ALIGN=right NOWRAP>27988</TD><TD ALIGN=right NOWRAP>592</TD><TD ALIGN=right NOWRAP>34726</TD><TD ALIGN=right NOWRAP>1050</TD></TR>
</TABLE>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></DIV></BLOCKQUOTE><P>Table <A HREF="#qg-tab-stats">5</A> lists some additional statistics for ANL-DP
on the quasigroup problems. “Generated” and “Searched” are the number
of propositional clauses generated and the number remaining after
subsumption and the initial unit propagation. “Create” is the time
(in seconds) used to construct the propositional clauses.</P><BLOCKQUOTE CLASS="table"><DIV CLASS="center"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV> <DIV CLASS="caption"><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left>Table 5: Quasigroup Problems – ANL-DP Full Statistics</TD></TR>
</TABLE></DIV> <A NAME="qg-tab-stats"></A>
<TABLE CELLSPACING=6 CELLPADDING=0><TR><TD ALIGN=right NOWRAP>Problem</TD><TD ALIGN=right NOWRAP>Models</TD><TD ALIGN=right NOWRAP>Branches</TD><TD ALIGN=right NOWRAP>Generated</TD><TD ALIGN=right NOWRAP>Searched</TD><TD ALIGN=right NOWRAP>Memory</TD><TD ALIGN=right NOWRAP>Create</TD><TD ALIGN=right NOWRAP>Search</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP> QG1.7</TD><TD ALIGN=right NOWRAP>8</TD><TD ALIGN=right NOWRAP>388</TD><TD ALIGN=right NOWRAP>120954</TD><TD ALIGN=right NOWRAP>8952</TD><TD ALIGN=right NOWRAP>886 K</TD><TD ALIGN=right NOWRAP>4.79</TD><TD ALIGN=right NOWRAP>2.05</TD></TR>
<TR><TD ALIGN=right NOWRAP> .8</TD><TD ALIGN=right NOWRAP>16</TD><TD ALIGN=right NOWRAP>100731</TD><TD ALIGN=right NOWRAP>267805</TD><TD ALIGN=right NOWRAP>28877</TD><TD ALIGN=right NOWRAP>2061 K</TD><TD ALIGN=right NOWRAP>10.85</TD><TD ALIGN=right NOWRAP>852.81</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP> QG2.7</TD><TD ALIGN=right NOWRAP>14</TD><TD ALIGN=right NOWRAP>361</TD><TD ALIGN=right NOWRAP>120954</TD><TD ALIGN=right NOWRAP>9830</TD><TD ALIGN=right NOWRAP>886 K</TD><TD ALIGN=right NOWRAP>4.72</TD><TD ALIGN=right NOWRAP>2.23</TD></TR>
<TR><TD ALIGN=right NOWRAP> .8</TD><TD ALIGN=right NOWRAP>2</TD><TD ALIGN=right NOWRAP>77158</TD><TD ALIGN=right NOWRAP>267805</TD><TD ALIGN=right NOWRAP>30902</TD><TD ALIGN=right NOWRAP>2061 K</TD><TD ALIGN=right NOWRAP>10.88</TD><TD ALIGN=right NOWRAP>810.75</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP> QG3.8</TD><TD ALIGN=right NOWRAP>18</TD><TD ALIGN=right NOWRAP>1017</TD><TD ALIGN=right NOWRAP>9757</TD><TD ALIGN=right NOWRAP>3830</TD><TD ALIGN=right NOWRAP>303 K</TD><TD ALIGN=right NOWRAP>0.26</TD><TD ALIGN=right NOWRAP>2.82</TD></TR>
<TR><TD ALIGN=right NOWRAP> .9</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>39461</TD><TD ALIGN=right NOWRAP>15670</TD><TD ALIGN=right NOWRAP>6966</TD><TD ALIGN=right NOWRAP>601 K</TD><TD ALIGN=right NOWRAP>0.39</TD><TD ALIGN=right NOWRAP>155.12</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP> QG4.8</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>891</TD><TD ALIGN=right NOWRAP>9757</TD><TD ALIGN=right NOWRAP>3830</TD><TD ALIGN=right NOWRAP>303 K</TD><TD ALIGN=right NOWRAP>0.25</TD><TD ALIGN=right NOWRAP>2.40</TD></TR>
<TR><TD ALIGN=right NOWRAP> .9</TD><TD ALIGN=right NOWRAP>178</TD><TD ALIGN=right NOWRAP>52939</TD><TD ALIGN=right NOWRAP>15670</TD><TD ALIGN=right NOWRAP>6966</TD><TD ALIGN=right NOWRAP>601 K</TD><TD ALIGN=right NOWRAP>0.37</TD><TD ALIGN=right NOWRAP>209.76</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP>QG5.9</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>14</TD><TD ALIGN=right NOWRAP>28792</TD><TD ALIGN=right NOWRAP>9694</TD><TD ALIGN=right NOWRAP>894 K</TD><TD ALIGN=right NOWRAP>0.85</TD><TD ALIGN=right NOWRAP>0.22</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>37</TD><TD ALIGN=right NOWRAP>43946</TD><TD ALIGN=right NOWRAP>17274</TD><TD ALIGN=right NOWRAP>1193 K</TD><TD ALIGN=right NOWRAP>1.39</TD><TD ALIGN=right NOWRAP>0.52</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=right NOWRAP>5</TD><TD ALIGN=right NOWRAP>112</TD><TD ALIGN=right NOWRAP>64428</TD><TD ALIGN=right NOWRAP>28488</TD><TD ALIGN=right NOWRAP>1786 K</TD><TD ALIGN=right NOWRAP>2.05</TD><TD ALIGN=right NOWRAP>2.16</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>369</TD><TD ALIGN=right NOWRAP>91363</TD><TD ALIGN=right NOWRAP>44302</TD><TD ALIGN=right NOWRAP>2674 K</TD><TD ALIGN=right NOWRAP>2.93</TD><TD ALIGN=right NOWRAP>6.61</TD></TR>
<TR><TD ALIGN=right NOWRAP> .13</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>9588</TD><TD ALIGN=right NOWRAP>125984</TD><TD ALIGN=right NOWRAP>65790</TD><TD ALIGN=right NOWRAP>3562 K</TD><TD ALIGN=right NOWRAP>4.02</TD><TD ALIGN=right NOWRAP>242.54</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP>QG6.9</TD><TD ALIGN=right NOWRAP>4</TD><TD ALIGN=right NOWRAP>17</TD><TD ALIGN=right NOWRAP>22231</TD><TD ALIGN=right NOWRAP>7653</TD><TD ALIGN=right NOWRAP>601 K</TD><TD ALIGN=right NOWRAP>0.66</TD><TD ALIGN=right NOWRAP>0.25</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>58</TD><TD ALIGN=right NOWRAP>33946</TD><TD ALIGN=right NOWRAP>13579</TD><TD ALIGN=right NOWRAP>900 K</TD><TD ALIGN=right NOWRAP>1.02</TD><TD ALIGN=right NOWRAP>0.54</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>537</TD><TD ALIGN=right NOWRAP>49787</TD><TD ALIGN=right NOWRAP>22332</TD><TD ALIGN=right NOWRAP>1493 K</TD><TD ALIGN=right NOWRAP>1.54</TD><TD ALIGN=right NOWRAP>5.36</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>7306</TD><TD ALIGN=right NOWRAP>70627</TD><TD ALIGN=right NOWRAP>34662</TD><TD ALIGN=right NOWRAP>2088 K</TD><TD ALIGN=right NOWRAP>2.24</TD><TD ALIGN=right NOWRAP>95.41</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
<TR><TD ALIGN=right NOWRAP>QG7.9</TD><TD ALIGN=right NOWRAP>4</TD><TD ALIGN=right NOWRAP>7</TD><TD ALIGN=right NOWRAP>22231</TD><TD ALIGN=right NOWRAP>5838</TD><TD ALIGN=right NOWRAP>601 K</TD><TD ALIGN=right NOWRAP>0.61</TD><TD ALIGN=right NOWRAP>0.19</TD></TR>
<TR><TD ALIGN=right NOWRAP> .10</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>39</TD><TD ALIGN=right NOWRAP>33946</TD><TD ALIGN=right NOWRAP>11038</TD><TD ALIGN=right NOWRAP>900 K</TD><TD ALIGN=right NOWRAP>1.04</TD><TD ALIGN=right NOWRAP>0.38</TD></TR>
<TR><TD ALIGN=right NOWRAP> .11</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>291</TD><TD ALIGN=right NOWRAP>49787</TD><TD ALIGN=right NOWRAP>18944</TD><TD ALIGN=right NOWRAP>1493 K</TD><TD ALIGN=right NOWRAP>1.48</TD><TD ALIGN=right NOWRAP>2.98</TD></TR>
<TR><TD ALIGN=right NOWRAP> .12</TD><TD ALIGN=right NOWRAP>-</TD><TD ALIGN=right NOWRAP>1578</TD><TD ALIGN=right NOWRAP>70627</TD><TD ALIGN=right NOWRAP>30309</TD><TD ALIGN=right NOWRAP>2088 K</TD><TD ALIGN=right NOWRAP>2.14</TD><TD ALIGN=right NOWRAP>17.87</TD></TR>
<TR><TD ALIGN=right NOWRAP> .13</TD><TD ALIGN=right NOWRAP>64</TD><TD ALIGN=right NOWRAP>33946</TD><TD ALIGN=right NOWRAP>97423</TD><TD ALIGN=right NOWRAP>45967</TD><TD ALIGN=right NOWRAP>2683 K</TD><TD ALIGN=right NOWRAP>3.14</TD><TD ALIGN=right NOWRAP>493.67</TD></TR>
<TR><TD CLASS="hbar" COLSPAN=8></TD></TR>
</TABLE>
<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></DIV></BLOCKQUOTE><!--TOC subsubsection Cyclically Generated Quasigroups-->
<H4 CLASS="subsubsection"><!--SEC ANCHOR --><A NAME="htoc11">2.5.1</A>  Cyclically Generated Quasigroups</H4><!--SEC END --><P>The command-line option <CODE>-x2</CODE> constrains models of quasigroup <CODE>f</CODE>
to have the property <I>f</I>(<I>x</I>+1,<I>y</I>+1)=<I>f</I>(<I>x</I>,<I>y</I>)+1, where addition is (mod <I>n</I>);
that is, all the diagonals count up (mod <EM>domain-size</EM>).</P><P>The command-line option <CODE>-x</CODE><I>i</I>, where 11≤ <I>i</I> ≤ 19,
constrains models of quasigroup <CODE>f</CODE> in the following way.
Consider the square of size <I>x</I>=<I>i</I>−10 in the lower right corner and the
remaining square of size <I>m</I>=<I>n</I>−<I>x</I> in the upper left corner. The
diagonals of the upper left square count up (mod <I>m</I>), except for
diagonals that consist of the same element in <I>m</I>,⋯,<I>n</I>−1. Also,
the first <I>m</I> elements of the last <I>x</I> rows and columns count up (mod
<I>m</I>). For example (see [<A HREF="#qg-survey">2</A>, Example 8.1] with the input
(note that the only upper left corner is idempotent)</P><PRE CLASS="verbatim"> set(dp_transform).
list(usable).
% (3,1,2)-COLS
f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
assign(f(0,0),0).
end_of_list.
</PRE><P> and the options “<CODE>-n 10 -x13 -p</CODE>”, we get
</P><PRE CLASS="verbatim"> Model #1 at 333.47 seconds (SPARC 10):
f | 0 1 2 3 4 5 6 7 8 9
---------------------------
0 | 0 4 1 7 9 2 8 3 6 5
1 | 8 1 5 2 7 9 3 4 0 6
2 | 4 8 2 6 3 7 9 5 1 0
3 | 9 5 8 3 0 4 7 6 2 1
4 | 7 9 6 8 4 1 5 0 3 2
5 | 6 7 9 0 8 5 2 1 4 3
6 | 3 0 7 9 1 8 6 2 5 4
|
7 | 1 2 3 4 5 6 0 7 8 9
8 | 2 3 4 5 6 0 1 8 9 7
9 | 5 6 0 1 2 3 4 9 7 8
</PRE><P> The <CODE>-x</CODE><I>i</I> option can also be used when searching for
quasigroups with holes.</P><!--TOC subsubsection Quasigroups with Holes-->
<H4 CLASS="subsubsection"><!--SEC ANCHOR --><A NAME="htoc12">2.5.2</A>  Quasigroups with Holes</H4><!--SEC END --><P> <A NAME="holey"></A></P><P>We simply list an example. The input (compare with above input)
</P><PRE CLASS="verbatim"> set(dp_transform).
list(usable).
same_hole(x,x) | f(x,x) = x.
% (3,1,2)-COLS
f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup_holey).
properties(same_hole(_,_), hole).
% The program makes same_hole symmetric and transitive.
assign(same_hole(7,8), T). assign(same_hole(8,9), T).
end_of_list.
</PRE><P> with the command-line options “<CODE>-n10 -x13 -p</CODE>” produces the following:
</P><PRE CLASS="verbatim"> Model #1 at 50.07 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 9
--------------------------
0 | 0 6 7 5 8 9 3 1 2 4
1 | 4 1 0 7 6 8 9 2 3 5
2 | 9 5 2 1 7 0 8 3 4 6
3 | 8 9 6 3 2 7 1 4 5 0
4 | 2 8 9 0 4 3 7 5 6 1
5 | 7 3 8 9 1 5 4 6 0 2
6 | 5 7 4 8 9 2 6 0 1 3
7 | 3 4 5 6 0 1 2 - - -
8 | 6 0 1 2 3 4 5 - - -
9 | 1 2 3 4 5 6 0 - - -
</PRE><!--TOC subsubsection Open Quasigroup Questions Answered-->
<H4 CLASS="subsubsection"><!--SEC ANCHOR --><A NAME="htoc13">2.5.3</A>  Open Quasigroup Questions Answered</H4><!--SEC END --><!--TOC paragraph Orthogonal Mendelsohn Triple Systems (OMTS).-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->Orthogonal Mendelsohn Triple Systems (OMTS).</H5><!--SEC END --><P>
Corollary 5.2 of [<A HREF="#somts">3</A>] states
</P><BLOCKQUOTE CLASS="quote">
The necessary condition for the existence of a pair of OMTS(<I>v</I>),
that is, <I>v</I>≡ 0 or 1 (mod 3), is also sufficient except for
<I>v</I>=3,6 and possibly excepting <I>v</I>∈ {9,10,12,18}.
</BLOCKQUOTE><P>
See [<A HREF="#somts">3</A>] for definitions. The input
</P><PRE CLASS="verbatim"> set(dp_transform).
list(usable).
f(x,x) = x.
h(x,x) = x.
f(x,f(y,x))=y.
h(x,h(y,x))=y.
f(x,y)!=u | f(z,w)!=u | h(x,y)!=v | h(z,w)!=v | x=z | y=w.
end_of_list.
list(passive).
properties(f(_,_), quasigroup).
properties(h(_,_), quasigroup).
end_of_list.
</PRE><P> with the options “<CODE>-n9 -x1 -p</CODE>” produces the following
quasigroups, which correspond to a pair of orthogonal Mendelsohn
triple systems of order 9.
</P><PRE CLASS="verbatim"> Model #1 at 54.58 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 h | 0 1 2 3 4 5 6 7 8
------------------------ ------------------------
0 | 0 8 5 2 7 4 3 6 1 0 | 0 2 6 4 3 1 8 5 7
1 | 8 1 7 6 3 2 5 4 0 1 | 5 1 0 8 2 3 7 6 4
2 | 3 5 2 8 6 0 4 1 7 2 | 1 4 2 6 7 8 0 3 5
3 | 6 4 0 3 8 7 1 5 2 3 | 4 5 7 3 0 6 2 8 1
4 | 5 7 6 1 4 8 2 0 3 4 | 3 8 1 0 4 7 5 2 6
5 | 2 6 1 7 0 5 8 3 4 5 | 7 0 8 1 6 5 3 4 2
6 | 7 3 4 0 2 1 6 8 5 6 | 2 7 3 5 8 4 6 1 0
7 | 4 2 8 5 1 3 0 7 6 7 | 8 6 4 2 5 0 1 7 3
8 | 1 0 3 4 5 6 7 2 8 8 | 6 3 5 7 1 2 4 0 8
</PRE><P> An analogous search for OMTS(10) ran for several days without
finding a model.</P><!--TOC paragraph QG3(2<SUP>8</SUP>).-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->QG3(2<SUP>8</SUP>).</H5><!--SEC END --><P> A quasigroup of type <I>h</I><SUP><I>n</I></SUP> has order <I>h</I>*<I>n</I>
and <I>n</I> holes of size <I>h</I>. Frank Bennett posed [<A HREF="#bennett-email">1</A>]
the question of the existence of QG3(2<SUP>8</SUP>). (Mark Stickel had
already answered positively the question of the existence of QG3(2<SUP>6</SUP>)
[<A HREF="#bennett-email">1</A>].)
The ANL-DP input
</P><PRE CLASS="verbatim"> relation = 2 equality
relation same_hole 2 hole
function f 3 quasigroup_holey
end_of_symbols
f v0 v0 v0 same_hole v0 v0 .
-f v0 v1 v2 -f v1 v0 v3 f v3 v2 v1 .
-f v0 v1 v2 -f v0 v2 v1 = v0 v1 .
-f v0 v1 v2 -f v2 v1 v0 = v0 v1 .
end_of_clauses
same_hole 0 7
same_hole 1 8
same_hole 2 9
same_hole 3 10
same_hole 4 11
same_hole 5 12
same_hole 6 13
same_hole 14 15
end_of_assignments
</PRE><P> with the options “<CODE>-n16 -p</CODE>” produces the following holey quasigroup.
</P><PRE CLASS="verbatim"> Model #1 at 76086.21 seconds (i468 DX2/66):
f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
------------------------------------------------------
0 | - 2 3 12 1 4 5 - 10 11 14 15 13 8 6 9
1 | 3 - 6 5 15 0 14 12 - 4 11 7 10 2 9 13
2 | 11 15 - 0 10 14 12 13 7 - 5 6 3 4 1 8
3 | 2 13 1 - 9 7 4 15 11 12 - 0 14 5 8 6
4 | 5 10 7 1 - 6 9 8 14 3 15 - 2 0 13 12
5 | 13 4 11 14 0 - 8 6 15 7 9 10 - 1 2 3
6 | 4 0 15 9 14 11 - 3 12 5 2 8 7 - 10 1
7 | - 6 8 13 2 9 15 - 5 14 4 12 1 11 3 10
8 | 14 - 4 6 3 2 10 9 - 0 13 5 15 7 12 11
9 | 15 3 - 11 6 8 7 1 13 - 12 14 0 10 4 5
10 | 6 5 14 - 7 15 11 2 9 1 - 13 8 12 0 4
11 | 8 12 10 2 - 1 3 14 6 13 7 - 9 15 5 0
12 | 10 9 0 8 13 - 1 11 4 15 6 3 - 14 7 2
13 | 9 14 12 15 5 3 - 10 2 8 0 1 4 - 11 7
14 | 1 7 13 4 12 10 0 5 3 6 8 2 11 9 - -
15 | 12 11 5 7 8 13 2 4 0 10 1 9 6 3 - -
</PRE><P> (In case the reader is wondering why the holes are irregular in the
lower right corner, the reason is that preliminary runs on QG3(2<SUP>6</SUP>)
ran faster with a similar hole configuration than with a regular
configuration.)</P><!--TOC paragraph QG7(17,5).-->
<H5 CLASS="paragraph"><!--SEC ANCHOR -->QG7(17,5).</H5><!--SEC END --><P> Frank Bennett posed [<A HREF="#bennett-email">1</A>] the question
of whether the the quasigroup identity (QG7a) <I>x</I>(<I>yx</I>) = (<I>yx</I>)<I>y</I> implies
either (<I>xy</I>)<I>x</I> = <I>x</I>(<I>yx</I>) or <I>xy</I>(<I>yx</I>) = <I>y</I>. He suggested looking at
models of order 17 with a hole of size 5, if they exist, as possible
counterexamples. The identity (QG7b) ((<I>xy</I>)<I>x</I>)<I>y</I> = <I>x</I>, which is
conjugate-equivalent [<A HREF="#qg-survey">2</A>] to (QG7a), is much easier to
work with, so we put ANL-DP to work with the input
</P><PRE CLASS="verbatim"> relation same_hole 2 hole
function f 3 quasigroup_holey
end_of_symbols
f v0 v0 v0 same_hole v0 v0 .
-f v0 v1 v2 -f v2 v0 v3 f v3 v1 v0 .
end_of_clauses
same_hole 12 13
same_hole 13 14
same_hole 14 15
same_hole 15 16
end_of_assignments
</PRE><P> and the options “<CODE>-n17 -x1 -p</CODE>”, which produced the following
</P><PRE CLASS="verbatim"> Model #1 at 172914.77 seconds (SPARC 2):
f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
---------------------------------------------------------
0 | 0 2 1 16 13 11 12 8 5 15 14 7 4 6 9 10 3
1 | 16 1 3 2 10 13 9 12 15 4 6 14 5 7 8 11 0
2 | 3 16 2 0 15 9 14 10 12 7 5 13 11 8 4 6 1
3 | 1 0 16 3 8 15 11 14 6 12 13 4 10 9 5 7 2
4 | 8 13 10 15 4 6 5 16 2 14 0 12 9 3 11 1 7
5 | 13 9 15 11 16 5 7 6 14 3 12 1 8 2 10 0 4
6 | 11 12 9 14 7 16 6 4 13 0 15 2 3 10 1 8 5
7 | 12 10 14 8 5 4 16 7 1 13 3 15 2 11 0 9 6
8 | 15 6 5 12 14 1 2 13 8 10 9 16 0 4 7 3 11
9 | 7 15 12 4 0 14 13 3 16 9 11 10 1 5 6 2 8
10 | 5 14 13 6 12 3 0 15 11 16 10 8 7 1 2 4 9
11 | 14 4 7 13 2 12 15 1 9 8 16 11 6 0 3 5 10
12 | 10 11 4 5 3 2 8 9 7 6 1 0 - - - - -
13 | 9 8 6 7 11 10 3 2 0 1 4 5 - - - - -
14 | 4 5 8 9 1 0 10 11 3 2 7 6 - - - - -
15 | 6 7 11 10 9 8 1 0 4 5 2 3 - - - - -
16 | 2 3 0 1 6 7 4 5 10 11 8 9 - - - - -
</PRE><P> The conjugate-equivalent quasigroup corresponding to (QG7a) was then
generated and found to falsify the two identities in question,
giving a counterexample to the problem.</P><!--TOC section References-->
<H2 CLASS="section"><!--SEC ANCHOR -->References</H2><!--SEC END --><DL CLASS="thebibliography"><DT CLASS="dt-thebibliography">
<A NAME="bennett-email"><FONT COLOR=purple>[1]</FONT></A></DT><DD CLASS="dd-thebibliography">
F. E. Bennett.
Correspondence by electronic mail, 1994.</DD><DT CLASS="dt-thebibliography"><A NAME="qg-survey"><FONT COLOR=purple>[2]</FONT></A></DT><DD CLASS="dd-thebibliography">
F. E. Bennett and L. Zhu.
Conjugate-orthogonal Latin squares and related structures.
In J. H. Dinitz and D. R. Stinson, editors, <EM>Contemporary Design
Theory: A Collection of Surveys</EM>, pages 41–96. John Wiley & Sons, 1992.</DD><DT CLASS="dt-thebibliography"><A NAME="somts"><FONT COLOR=purple>[3]</FONT></A></DT><DD CLASS="dd-thebibliography">
F. E. Bennett and L. Zhu.
Self-orthogonal Mendelsohn triple systems.
Preprint, 1994.</DD><DT CLASS="dt-thebibliography"><A NAME="qg-ijcai"><FONT COLOR=purple>[4]</FONT></A></DT><DD CLASS="dd-thebibliography">
M. Fujita, J. Slaney, and F. E. Bennett.
Automatic generation of some results in finite algebra.
In <EM>International Joint Conference on Artificial Intelligence</EM>,
1993.</DD><DT CLASS="dt-thebibliography"><A NAME="otter3"><FONT COLOR=purple>[5]</FONT></A></DT><DD CLASS="dd-thebibliography">
W. McCune.
<SPAN STYLE="font-variant:small-caps">Otter</SPAN> 3.0 Reference Manual and Guide.
Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, Ill.,
1994.</DD><DT CLASS="dt-thebibliography"><A NAME="finder3"><FONT COLOR=purple>[6]</FONT></A></DT><DD CLASS="dd-thebibliography">
J. Slaney.
FINDER version 3.0 notes and guide.
Tech. report, Centre for Information Science Research, Australian
National University, 1993.</DD><DT CLASS="dt-thebibliography"><A NAME="qg-slaney-fujita-stickel"><FONT COLOR=purple>[7]</FONT></A></DT><DD CLASS="dd-thebibliography">
J. Slaney, M. Fujita, and M. Stickel.
Automated reasoning and exhaustive search: Quasigroup existence
problems.
<EM>Computers and Mathematics with Applications</EM>, 1994.
To appear.</DD><DT CLASS="dt-thebibliography"><A NAME="dp-trie"><FONT COLOR=purple>[8]</FONT></A></DT><DD CLASS="dd-thebibliography">
H. Zhang and M. Stickel.
Implementing the Davis-Putnam algorithm by tries.
Preprint, 1994.</DD></DL><!--BEGIN NOTES document-->
<HR CLASS="footnoterule"><DL CLASS="thefootnotes"><DT CLASS="dt-thefootnotes">
<A NAME="note1" HREF="#text1">*</A></DT><DD CLASS="dd-thefootnotes">This work was
supported by the Office of Scientific Computing,
U.S. Department of Energy, under Contract W-31-109-Eng-38.
</DD></DL>
<!--END NOTES-->
<!--CUT END -->
<!--HTMLFOOT-->
<!--ENDHTML-->
<!--FOOTER-->
<HR SIZE=2><BLOCKQUOTE CLASS="quote"><EM>This document was translated from L<sup>A</sup>T<sub>E</sub>X by
</EM><A HREF="http://hevea.inria.fr/index.html"><EM>H</EM><EM><FONT SIZE=2><sup>E</sup></FONT></EM><EM>V</EM><EM><FONT SIZE=2><sup>E</sup></FONT></EM><EM>A</EM></A><EM>.</EM></BLOCKQUOTE></BODY>
</HTML>
|