1\documentstyle[11pt]{article} 2% \renewcommand{\baselinestretch}{2} 3% \setlength{\textwidth}{6.25in} 4% \setlength{\textheight}{9in} 5\setlength{\hoffset}{-.5in} 6\setlength{\voffset}{-1in} 7\setlength{\parskip}{.1in} 8% \voffset=-.5in \hoffset=-.7in \parskip=.1in 9\textwidth=16cm \textheight=23.5cm 10\newcommand{\otter}{{\sc Otter}} 11% \pagestyle{empty} 12% \pagestyle{myheadings} \markright{DRAFT} 13\begin{document} 14\title{{\Large\bf A Davis-Putnam Program \\ 15and Its Application to 16Finite First-Order Model Search: 17Quasigroup Existence Problems}\thanks{This work was 18supported by the Office of Scientific Computing, 19U.S. Department of Energy, under Contract W-31-109-Eng-38.}} 20\author{{\it William McCune} \\ \\ 21Mathematics and Computer Science Division \\ 22Argonne National Laboratory \\ 23Argonne, Illinois 60439-4844, U.S.A. \\ 24e-mail: mccune@mcs.anl.gov \\ 25phone: 708-252-3065} 26\date{September 1994} 27\maketitle 28% \thispagestyle{empty} 29 30\begin{abstract} 31This document describes the implementation and use of a Davis-Putnam 32procedure for the propositional satisfiability problem. It also 33describes code that takes statements in first-order logic with 34equality and a domain size $n$ then searches for models of size $n$. The 35first-order model-searching code transforms the statements into set of 36propositional clauses such that the first-order statements have a 37model of size $n$ if and only if the propositional clauses are 38satisfiable. The propositional set is then given to the Davis-Putnam 39code; any propositional models that are found can be translated to 40models of the first-order statements. 41The first-order model-searching program accepts statements only in a 42flattened relational clause form without function symbols. Additional 43code was written to take input statements in the language of \otter\ 3.0 44and produce the flattened relational form. 45The program was successfully applied to several open questions 46on the existence of orthogonal quasigroups. 47\end{abstract} 48 49\section{The Davis-Putnam Procedure} 50 51The Davis-Putnam procedure is widely regarded as the best method 52for deciding the satisfiability of a set of propositional clauses. 53I'll assume that the reader is familiar with it. I list here some 54features of our implementation. 55\begin{enumerate} 56\item There are no checks for pure literals. Experience has shown that 57such checks are usually more expensive than they are worth. 58\item Deletion of subsumed clauses is optional. Again, experience 59has shown that it is too expensive. 60\item The variable selected for splitting is the always first literal 61of the first, shortest positive clause. 62\end{enumerate} 63 64\subsection{Implementation} 65 66The data structures for clauses and for propositional variables and 67the algorithms are similar to the ones Mark Stickel uses in LDPP 68\cite{dp-trie}. 69 70Variables are integers $\geq 1$. Associated with the set of variables 71is an array, indexed by the variables, of variable structures. Each 72variable structure contains the following fields. 73\begin{itemize} 74\item {\verb:value:.} 75The current value (true, false, or unassigned) of the variable. 76\item {\verb:enqueued_value:.} 77A field to speed the bottleneck operation of unit propagation (see below). 78\item {\verb:pos_occ:.} 79A list of pointers to clauses that contain the 80variable in a positive literal. 81\item {\verb:neg_occ:.} 82A list of pointers to clauses that contain the 83variable in a negative literal. 84\end{itemize} 85Each clause contains the following fields. 86\begin{itemize} 87\item {\verb:pos:.} 88A list of variables representing positive literals. 89\item {\verb:neg:.} 90A list of variables representing negative literals. 91\item {\verb:active_pos:.} 92The number of positive literals that have not been resolved away. 93\item {\verb:active_neg:.} 94The number of negative literals that have not been resolved away. 95\item {\verb:subsumer:.} 96A field set to the responsible variable if the clause has been 97inactivated by subsumption. 98\end{itemize} 99 100\paragraph{Assignment.} 101When a variable is assigned a value, say true, by splitting or during 102unit propagation, unit resolution is performed by traversing the 103\verb:neg_occ: list of the variable: for each clause that has not 104been subsumed, the \verb:active_neg: field is simply decremented by 1. 105If \verb:active_pos+active_neg: becomes 0, the empty clause has been 106found and backtracking occurs. If \verb:active_pos+active_neg: 107becomes 1, the new unit clause is queued for unit propagation. In 108addition, if subsumption is enabled, (back) subsumption is performed 109by traversing the 110\verb:pos_occ: list of the variable: for each clause that is not 111already subsumed, the \verb:subsumer: field is set to the variable. 112Variables must be unassigned during backtracking, and the process is 113essentially the reverse of assignment. 114 115\paragraph{Unit Propagation.} 116A split causes an assignment. The unit propagation queue is then 117processed (causing further assignments and possibly more units to be 118queued) until empty or the empty clause is found. Each split 119typically causes many assignments, so unit propagation must be done 120efficiently. To avoid duplicates in the queue, and to detect 121the empty clause during the enqueue operation rather than during 122assignment, we set the field \verb:enqueued_value: of the variable 123when the corresponding literal is enqueued. That way we can quickly 124tell whether a literal or its complement is already in the queue. 125 126\paragraph{Unit Preprocessing.} 127If the set of input clauses contains any units, unit propagation is 128applied. During assignment, back subumption is always applied, 129because assignments made during this phase are never undone. 130 131\paragraph{Selecting Variables for Splitting.} 132The variable selected for splitting is the first literal in the first, 133shortest nonsubsumed positive clause. After the unit preprocessing, 134pointers to all of the non-Horn clauses (i.e., clauses with two or more 135positive literals) are collected into a list. In order to select a variable 136for splitting, the list is simply traversed. Subsumed clauses must be 137ignored; if subsumption is enabled, the subsumer field is checked; 138otherwise the clause is scanned for a literal with value true. 139(If all clauses in the list are subsumed, a model has been found.) 140 141\subsection{Pigeonhole Problems} 142 143The pigeonhole problems are a set of artificial propositional problems 144that are used to test the efficiency of propositional theorem provers. 145See the sample input files that come with ANL-DP for examples. Table 146\ref{pigeon} lists the performance of ANL-DP on several instances of 147the pigeonhole problems. The jobs were run on a SPARC 2. 148 149\begin{table}[htbp] \centering 150\caption{ANL-DP on the Pigeonhole Problems} \label{pigeon} 151\begin{tabular}{lrr} 152 & Branches & Seconds \\ 153\hline 1547 pigeons, 6 holes & 719 & .15 \\ 1558 pigeons, 7 holes & 5039 & 1.14 \\ 1569 pigeons, 8 holes & 40319 & 9.16 \\ 15710 pigeons, 9 holes & 362879 & 88.43 \\ 15811 pigeons, 10 holes & 3628799 & 916.62 \\ 159\hline 160\end{tabular} 161\end{table} 162 163\subsection{Using ANL-DP} \label{use-prop} 164 165Propositional input to ANL-DP is a sequence of clauses. 166(See Sec. \ref{use-fo} for input to the first-order model-searching program.) 167Literals are nonzero integers (negative integers represent negative 168literals), and each clause is terminated with 0. 169(Hence, the entire input is just a sequence of integers.) 170The input is taken from \verb:stdin: (the standard input). 171 172ANL-DP accepts the following command-line options. 173\begin{description} 174\item {\verb:-s:.} 175Perform subsumption. (Subsumption is always performed during unit preprocessing.) 176\item {\verb:-p:.} 177Print models as they are found. 178\item {\verb:-m: $n$.} 179Stop when the $n$-th model is found. 180\item {\verb:-t: $n$.} 181Stop after $n$ seconds. 182\item {\verb:-k: $n$.} 183Allocate at most $n$ kbytes for storage of clauses. 184\item {\verb:-x: $n$.} 185Quasigroup experiment $n$. See Section \ref{qg}. 186\item {\verb:-B: {\it file}.} 187Backup assignments to a file. 188\item {\verb:-b: $n$.} 189Backup assignments every $n$ seconds. 190\item {\verb:-R: {\it file}.} 191Restore assignments from a file. The file typically contains just the 192last line of a backup file. Other input, in particular the clauses, 193must be given exactly as in the original search. 194\item {\verb:-n: $n$.} 195This option is used for first-order model searches. The parameter $n$ 196specifies the domain size, and its presence tells the program to 197read first-order flattened relational input clauses instead of propositional 198clauses. 199\end{description} 200 201\section{The First-Order Model-Searching Program} 202 203The first practical program for searching for small models of 204first-order statements was FINDER \cite{finder3}. Another 205model-searching program is MGTP \cite{qg-slaney-fujita-stickel}, which 206uses a somewhat different approach. The third class of programs, 207including LDPP 208\cite{dp-trie}, SATO \cite{dp-trie}, and the one described here, are based 209on Davis-Putnam procedures. None of these programs is clearly better 210than the others, and each has answered open questions about 211quasigroups (see Sec. \ref{qg}). 212 213The Davis-Putnam approach is quite elegant, because the computational 214engine---the Davis-Putnam code---is in no way tailored to 215first-order model searching. First-order clauses and a domain 216size $n$ are input; then ground instances (over the domain) of the first-order 217clauses are generated and given to the Davis-Putnam code. Any 218propositional models that are found can be easily translated to 219first-order models (e.g., an $n\times n$ table for a binary function). 220 221The steps, which are summarized in Figure \ref{trans}, are as follows. 222 223\begin{figure}[h] 224\begin{picture}(400,80)(-35,0) 225 226\thicklines 227 228\put(0,60){FO formula} 229\put(100,60){FO clauses} 230\put(200,60){FO flat clauses} 231\put(300,60){Prop. clauses} 232\put(300,0){Prop. models} 233\put(100,0){FO models} 234 235\put(65,63){\vector(1,0){30}} \put(70,68){(1)} 236\put(160,63){\vector(1,0){35}} \put(168,68){(2)} 237\put(275,63){\vector(1,0){20}} \put(275,68){(3)} 238\put(330,55){\vector(0,-1){40}} \put(333,35){(4)} 239\put(295,3){\vector(-1,0){135}} \put(230,8){(5)} 240 241\thinlines 242% \put(125,55){\vector(0,-1){40}} 243\put(125,17){\dashbox(0,38)} 244\put(125,18){\vector(0,-1){3}} 245 246\end{picture} 247\caption{Searching for First-Order Models} \label{trans} 248\end{figure} 249 250\begin{enumerate} 251\item[(1)] 252Take an arbitrary first-order formula (possibly involving equality), 253and produce a set of clauses. \otter 's clausification code is 254sufficient for this. 255\item[(2)] 256Take a set of first-order clauses, and produce a set of flattened, 257relational clauses that 258contain no constants or function symbols---all arguments of 259the literals are variables. The steps are as follows: 260\begin{enumerate} 261\item[a.] 262For each $n$-ary function symbol 263(including constants), an $n+1$-ary predice symbol is introduced. 264For the examples, function symbols are lower-case letters, and new predicate 265symbols are the corresponding upper-case letters. 266\item[b.] 267To flatten the clauses, the following kind of equality 268transformation is applied to nonvariable terms (excepting arguments 269of positive equalities): $P[t]$ is rewritten to $t\neq x \; |\; P[x]$. 270\item[c.] 271A clause containing a positive equality $\alpha=\beta$, where both arguments 272are nonvariable, 273is made into two clauses: $L\;|\;\alpha=\beta$ becomes 274$L\;|\;\alpha\neq x\;|\;\beta=x$ and $L\;|\;\beta\neq x\;|\;\alpha=x$. 275\item[d.] 276Each functional literal, say $f(x,y)=z$, is rewritten into its 277relational form, say $F(x,y,z)$. (The resulting clauses may contain 278ordinary equality literals as well.) 279\end{enumerate} 280For example, the equality $f(g(x),x)=e$ produces the two clauses 281\begin{verse} 282$\neg G(x,y) \;|\;\neg E(z) \;|\;F(y,x,z)$ \\ 283$\neg G(x,y) \;|\;E(z) \;|\;\neg F(y,x,z)$ 284\end{verse} 285\item[(3)] 286Take a set of flattened relational clauses and a domain size, and 287generate a set of propositional clauses. For each relational clause, 288the set of instances over the domain is constructed. (With domain 289size $n$, a clause with $m$ variables produces $n^m$ instances.) Each 290atom is encoded into a unique integer that becomes the propositional 291variable. Also, we must assert that the $(n+1)$-ary predicates 292introduced above represent total functions, so for each, we assert two 293sets of propositional clauses. For example, for ternary relation $F$, 294we must say that the last argument is a function of the others, 295\begin{verse} 296$\neg F(x,y,z_1) \;|\; \neg F(x,y,z_2)$, for $z_1 < z_2$ (well-defined) 297\end{verse} 298and that the function is total and its value always lies in the domain 299(elements of the domain are named $0, 1, \cdots, n-1$): 300\begin{verse} 301$F(x,y,0) \;|\; F(x,y,1) \;|\; \cdots \;|\; F(x,y,n-1)$ (closed and total). 302\end{verse} 303If the flattened relational clauses contain any equality literals, 304the $n^2$ units for the equality relation are asserted. 305Nothing special needs to be done for ordinary predicate symbols. 306\item[(4)] 307The Davis-Putnam procedure searches for models of the propositional 308clauses. 309\item[(5)] 310For each propositional model, we generate the corresponding first-order model. 311The clauses given in (3) above ensure that from the propositional model, 312we can build a function for each function symbol (including constants). 313\end{enumerate} 314 315\subsection{Additional Constraints} 316 317For various reasons, the most important being to reduce the number of 318isomorphic models that are found, the user can specify part of the 319model by supplying ground clauses over the domain. For example, 320if a noncommutative group is being sought, with constants $a$ and $b$ 321as noncommuting elements, 322the user can assign 0 to the identity, 1 to $a$, and 2 to $b$. 323In this case, nothing is lost by making them distinct. 324 325Symbols can be given the following properties. 326\begin{description} 327\item{\verb:quasigroup:.} 328This can be applied to ternary relations that represent binary functions. 329The multiplication table of a quasigroup has one of each element in each 330row and each column. 331\item{\verb:bijection:.} 332This can be applied to binary relations that represent unary functions. 333\item{\verb:equality:.} 334This can be applied to binary relations. It is just equality of domain 335elements. 336\item{\verb:order:.} 337This can be applied to binary relations. This is just the less-than 338relation on the domain elements. 339\item{\verb:holey:.} 340This can be applied to ternary relations that represent binary functions. 341See Sec. \ref{holey}. 342\item{\verb:hole:.} 343This can be applied to binary relations. 344See Sec. \ref{holey}. 345\end{description} 346 347\subsection{Using the Program to Search for First-Order Models} \label{use-fo} 348 349The first-order searcher is part of ANL-DP, and it is invoked 350as described in Sec. \ref{use-prop}. The command-line option 351``\verb:-n: $n$'' specifies the domain size and indicates that 352the input will be given as first-order flat clauses. Here is an 353example input specifying a noncommutative group. 354\begin{verbatim} 355 function F 3 quasigroup 356 function E 1 ----- 357 function G 2 bijection 358 function A 1 ----- 359 function B 1 ----- 360 end_of_symbols 361 362 -E v0 F v0 v1 v1 . 363 -E v0 -G v1 v2 F v2 v1 v0 . 364 E v0 -G v1 v2 -F v2 v1 v0 . 365 -F v0 v1 v2 -F v3 v2 v4 -F v3 v0 v5 F v5 v1 v4 . 366 -F v0 v1 v2 F v3 v2 v4 -F v3 v0 v5 -F v5 v1 v4 . 367 -F v0 v1 v2 -B v0 -A v1 -F v1 v0 v2 . 368 end_of_clauses 369 370 E 0 371 A 1 372 B 2 373 end_of_assignments 374\end{verbatim} 375\begin{description} 376\item{Symbol Declarations.} 377In the first section of the input, each symbol is declared with four 378strings: type (\verb:function: or \verb:relation:), symbol, arity ($n$+1 379for functions), and properties (\verb:equality:, \verb:order:, 380\verb:quasigroup:, \verb:bijection:, or \verb:-----:). 381\item{Clauses.} 382Flat relational clauses appear in the second section. Variables can 383be any strings. {\em Whitespace is required before the periods that 384terminates clauses.} 385\item{Assignments.} 386Ground units (without periods) can appear in the third section. 387\end{description} 388 389\subsection{Using \otter\ to Generate the Flat Clauses} 390 391\otter\ 3.0.2 \cite{otter3} and later versions can take ordinary formulas or 392clauses and produce the flat relational clauses for input to ANL-DP. 393Here is an \otter\ input file for a noncommutative group that will 394produce something like the file in Sec. \ref{use-fo}. 395\begin{verbatim} 396 set(dp_transform). 397 398 list(usable). 399 f(e,x) = x. 400 f(g(x),x) = e. 401 f(f(x,y),z) = f(x,f(y,z)). 402 f(a,b) != f(b,a). 403 end_of_list. 404 405 list(passive). 406 properties(f(_,_), quasigroup). 407 properties(g(_), bijection). 408 assign(e, 0). 409 assign(a, 1). 410 assign(b, 2). 411 end_of_list. 412\end{verbatim} 413The command \verb:set(dp_transform): tells \otter\ to generate 414input for an ANL-DP search and then exit. 415 416The output of \otter\ contains extraneous text, so it must be passed 417though a filter before ANL-DP can receive it. See the example files 418and scripts in the distribution directories. 419 420\subsection{The Order Relation} \label{order} 421 422The ordered semigroup example in the FINDER 3.0 manual 423\cite[Sec. 4.1.5]{finder3} motivated me to have ANL-DP recognize the 424less-than relation on domain elements. The input (in \otter\ form) 425for the ordered semigroup problems is as follows. 426\begin{verbatim} 427 set(dp_transform). 428 list(usable). 429 f(f(x,y),z) = f(x,f(y,z)). 430 -(f(x,y) < f(x,z)) | y < z. 431 -(f(y,x) < f(z,x)) | y < z. 432 end_of_list. 433\end{verbatim} 434(\otter\ recognizes \verb:<: as the order relation and gives it 435the property ``order'' in its output.) 436Table \ref{order-tab} compares the results of FINDER and ANL-DP, both 437run on SPARC 2 computers, on the ordered semigroup problems. FINDER's 438search algorithm was developed with this type of problem in mind; 439ANL-DP simply adds the $n^2$ unit clauses for the less-than relation. 440I believe this distinction explains most of the disparity of the 441times. 442 443\begin{table}[htb] \centering 444\caption{Ordered Semigroup Problems -- FINDER vs. ANL-DP} \label{order-tab} 445\begin{tabular}{crrr} 446Order & Models & FINDER & ANL-DP \\ 447\hline 4483 & 44 & 0.1 & 0.1 \\ 4494 & 386 & 0.6 & 2.6 \\ 4505 & 3852 & 9.2 & 58.0 \\ 451\end{tabular} 452\end{table} 453 454\subsection{Application to Quasigroup Problems} \label{qg} 455 456In the multiplication table of an order-$n$ quasigroup, each row and 457each column are a permutation of the $n$ elements. For these problems, 458we are interested only in idempotent (i.e., $xx=x$) models. 459Additional constraints are given for the seven problems listed in 460Table \ref{qg-tab}. (Notes: (1) For QG1 and QG2, the disjunction to 461the right of the implication is ordinarily a conjunction; the forms 462are equivalent for quasigroups, and models are found more 463easily with disjunction. (2) The second and third equalities for QG5 464and the second equality for QG7 are dependent.) See \cite{qg-survey} and 465\cite{qg-slaney-fujita-stickel} for details on the quasigroup problems. 466 467\begin{table}[htb] \centering 468\caption{The Quasigroup Problems} \label{qg-tab} 469\begin{tabular}{ll} 470Name & Constraints \\ 471\hline 472QG1 & $xy=u \;\wedge\; zw=u \;\wedge\; vy=x \;\wedge\; vw= z \rightarrow x=z \;\vee\; y=w$ \\ 473QG2 & $xy=u \;\wedge\; zw=u \;\wedge\; vx=y \;\wedge\; vz= w \rightarrow x=z \;\vee\; y=w$ \\ 474QG3 & $(xy)(yx)=x$ \\ 475QG4 & $(xy)(yx)=y$ \\ 476QG5 & $((xy)x)x=y \;\wedge\; x((yx)x)=y \;\wedge\; (x(yx))x=y$ \\ 477QG6 & $(xy)y = x(xy)$ \\ 478QG7 & $((xy)x)y=x \;\wedge\; ((xy)y)(xy)=x$ \\ 479\hline 480\end{tabular} 481\end{table} 482 483We also used the following cycle constraint on the last column to 484eliminate some isomorphic models \cite{qg-slaney-fujita-stickel}: 485\begin{verse} 486$\neg f(x,n,z)$, for $z < x-1$. 487\end{verse} 488The constraint requires that cycles in the last column be made up 489of contiguous elements. This constraint is specified to ANL-DP with 490the command-line option ``\verb:-x1:''; {\em the quasigroup operation 491must be \verb:f: (lower-case) for this to work}. 492 493Table \ref{qg-tab-compare} gives summaries of the performance of 494ANL-DP (C, list structure), SATO-2 (C, trie structure), and LDPP$'$ 495(Lisp, list structure) on some cases of the quasigroup problems. 496The SATO and LDPP figures are taken from \cite{dp-trie}. 497All runs were made on a SPARC 2 or similar computer. All programs used 498the cycle constraint and similar selection functions for splitting. I 499believe that differences in the number of branches are due mostly to 500the order of clauses and literals. Search time is given in seconds. 501 502\begin{table}[htb] \centering 503\caption{Quasigroup Problems -- Comparison} \label{qg-tab-compare} 504\begin{tabular}{rc|rr|rr|rr} 505 & & \multicolumn{2}{c}{ANL-DP} & \multicolumn{2}{c}{SATO-2}& \multicolumn{2}{c}{LDPP$'$} \\ 506 Problem & Models & Branches & Search & Branches & Search & Branches & Search \\ 507 \hline 508 QG1.7 & 8 & 388 & 2.05 & 376 & 1 & 389 & 26\\ 509 .8 & 16 & 100731 & 852.81 & 102610 & 379 & 101129 & 3463\\ 510 \hline 511 QG2.7 & 14 & 361 & 2.23 & 340 & 1 & 205 & 8\\ 512 .8 & 2 & 77158 & 810.75 & 80245 & 341 & 33835 & 1358\\ 513 \hline 514 QG3.8 & 18 & 1017 & 2.82 & 1072 & 3 & 573 & 5\\ 515 .9 & - & 39461 & 155.12 & 48545 & 157 & 24763 & 208\\ 516 \hline 517 QG4.8 & - & 891 & 2.40 & 925 & 2 & 602 & 4\\ 518 .9 & 178 & 52939 & 209.76 & 52826 & 168 & 27479 & 228\\ 519 \hline 520 QG5.9 & - & 14 & .22 & 19 & .2 & 15 & .4\\ 521 .10 & - & 37 & .52 & 62 & .5 & 38 & .9\\ 522 .11 & 5 & 112 & 2.16 & 111 & 2 & 125 & 5\\ 523 .12 & - & 369 & 6.61 & 369 & 7 & 369 & 15\\ 524 .13 & - & 9588 & 242.54 & 10764 & 224 & 12686 & 639\\ 525 \hline 526 QG6.9 & 4 & 17 & .25 & 24 & .2 & 18 & .4\\ 527 .10 & - & 58 & .54 & 150 & .7 & 59 & .8\\ 528 .11 & - & 537 & 5.36 & 519 & 6 & 539 & 11\\ 529 .12 & - & 7306 & 95.41 & 5728 & 92 & 7288 & 177\\ 530 \hline 531 QG7.9 & 4 & 7 & .19 & 7 & .2 & 8 & .3\\ 532 .10 & - & 39 & .38 & 54 & .4 & 40 & .7\\ 533 .11 & - & 291 & 2.98 & 254 & 3 & 294 & 6\\ 534 .12 & - & 1578 & 17.87 & 1281 & 22 & 1592 & 38\\ 535 .13 & 64 & 33946 & 493.67 & 27988 & 592 & 34726 & 1050\\ 536\hline 537\end{tabular} 538\end{table} 539\newpage 540 541Table \ref{qg-tab-stats} lists some additional statistics for ANL-DP 542on the quasigroup problems. ``Generated'' and ``Searched'' are the number 543of propositional clauses generated and the number remaining after 544subsumption and the initial unit propagation. ``Create'' is the time 545(in seconds) used to construct the propositional clauses. 546 547\begin{table}[htb] \centering 548\caption{Quasigroup Problems -- ANL-DP Full Statistics} \label{qg-tab-stats} 549\begin{tabular}{rrrrrrrr} 550Problem & Models & Branches & Generated & Searched & Memory & Create & Search \\ 551\hline 552 QG1.7 & 8 & 388 & 120954 & 8952 & 886 K & 4.79 & 2.05 \\ 553 .8 & 16 & 100731 & 267805 & 28877 & 2061 K & 10.85 & 852.81 \\ 554\hline 555 QG2.7 & 14 & 361 & 120954 & 9830 & 886 K & 4.72 & 2.23 \\ 556 .8 & 2 & 77158 & 267805 & 30902 & 2061 K & 10.88 & 810.75 \\ 557\hline 558 QG3.8 & 18 & 1017 & 9757 & 3830 & 303 K & 0.26 & 2.82 \\ 559 .9 & - & 39461 & 15670 & 6966 & 601 K & 0.39 & 155.12 \\ 560\hline 561 QG4.8 & - & 891 & 9757 & 3830 & 303 K & 0.25 & 2.40 \\ 562 .9 & 178 & 52939 & 15670 & 6966 & 601 K & 0.37 & 209.76 \\ 563\hline 564QG5.9 & - & 14 & 28792 & 9694 & 894 K & 0.85 & 0.22 \\ 565 .10 & - & 37 & 43946 & 17274 & 1193 K & 1.39 & 0.52 \\ 566 .11 & 5 & 112 & 64428 & 28488 & 1786 K & 2.05 & 2.16 \\ 567 .12 & - & 369 & 91363 & 44302 & 2674 K & 2.93 & 6.61 \\ 568 .13 & - & 9588 & 125984 & 65790 & 3562 K & 4.02 & 242.54 \\ 569\hline 570QG6.9 & 4 & 17 & 22231 & 7653 & 601 K & 0.66 & 0.25 \\ 571 .10 & - & 58 & 33946 & 13579 & 900 K & 1.02 & 0.54 \\ 572 .11 & - & 537 & 49787 & 22332 & 1493 K & 1.54 & 5.36 \\ 573 .12 & - & 7306 & 70627 & 34662 & 2088 K & 2.24 & 95.41 \\ 574\hline 575QG7.9 & 4 & 7 & 22231 & 5838 & 601 K & 0.61 & 0.19 \\ 576 .10 & - & 39 & 33946 & 11038 & 900 K & 1.04 & 0.38 \\ 577 .11 & - & 291 & 49787 & 18944 & 1493 K & 1.48 & 2.98 \\ 578 .12 & - & 1578 & 70627 & 30309 & 2088 K & 2.14 & 17.87 \\ 579 .13 & 64 & 33946 & 97423 & 45967 & 2683 K & 3.14 & 493.67 \\ 580\hline 581\end{tabular} 582\end{table} 583 584\subsubsection{Cyclically Generated Quasigroups} 585 586The command-line option \verb:-x2: constrains models of quasigroup \verb:f: 587to have the property $f(x+1,y+1)=f(x,y)+1$, where addition is (mod $n$); 588that is, all the diagonals count up (mod {\em domain-size}). 589 590The command-line option \verb:-x:$i$, where $11\leq i \leq 19$, 591constrains models of quasigroup \verb:f: in the following way. 592Consider the square of size $x=i-10$ in the lower right corner and the 593remaining square of size $m=n-x$ in the upper left corner. The 594diagonals of the upper left square count up (mod $m$), except for 595diagonals that consist of the same element in $m,\cdots,n-1$. Also, 596the first $m$ elements of the last $x$ rows and columns count up (mod 597$m$). For example (see \cite[Example 8.1]{qg-survey} with the input 598(note that the only upper left corner is idempotent) 599 600{\small \begin{verbatim} 601 set(dp_transform). 602 603 list(usable). 604 % (3,1,2)-COLS 605 f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w. 606 end_of_list. 607 608 list(passive). 609 properties(f(_,_), quasigroup). 610 assign(f(0,0),0). 611 end_of_list. 612\end{verbatim}} \noindent 613and the options ``\verb:-n 10 -x13 -p:'', we get 614{\small \begin{verbatim} 615 Model #1 at 333.47 seconds (SPARC 10): 616 617 f | 0 1 2 3 4 5 6 7 8 9 618 --------------------------- 619 0 | 0 4 1 7 9 2 8 3 6 5 620 1 | 8 1 5 2 7 9 3 4 0 6 621 2 | 4 8 2 6 3 7 9 5 1 0 622 3 | 9 5 8 3 0 4 7 6 2 1 623 4 | 7 9 6 8 4 1 5 0 3 2 624 5 | 6 7 9 0 8 5 2 1 4 3 625 6 | 3 0 7 9 1 8 6 2 5 4 626 | 627 7 | 1 2 3 4 5 6 0 7 8 9 628 8 | 2 3 4 5 6 0 1 8 9 7 629 9 | 5 6 0 1 2 3 4 9 7 8 630\end{verbatim}} \noindent 631The \verb:-x:$i$ option can also be used when searching for 632quasigroups with holes. 633 634\subsubsection{Quasigroups with Holes} \label{holey} 635 636We simply list an example. The input (compare with above input) 637{\small \begin{verbatim} 638 set(dp_transform). 639 640 list(usable). 641 same_hole(x,x) | f(x,x) = x. 642 % (3,1,2)-COLS 643 f(x,y)!=u | f(z,w)!=u | f(v,x)!=y | f(v,z)!= w | x=z | y=w. 644 end_of_list. 645 646 list(passive). 647 properties(f(_,_), quasigroup_holey). 648 properties(same_hole(_,_), hole). 649 % The program makes same_hole symmetric and transitive. 650 assign(same_hole(7,8), T). assign(same_hole(8,9), T). 651 end_of_list. 652\end{verbatim}} \noindent 653with the command-line options ``\verb:-n10 -x13 -p:'' produces the following: 654\newpage 655{\small \begin{verbatim} 656 Model #1 at 50.07 seconds (SPARC 2): 657 658 f | 0 1 2 3 4 5 6 7 8 9 659 -------------------------- 660 0 | 0 6 7 5 8 9 3 1 2 4 661 1 | 4 1 0 7 6 8 9 2 3 5 662 2 | 9 5 2 1 7 0 8 3 4 6 663 3 | 8 9 6 3 2 7 1 4 5 0 664 4 | 2 8 9 0 4 3 7 5 6 1 665 5 | 7 3 8 9 1 5 4 6 0 2 666 6 | 5 7 4 8 9 2 6 0 1 3 667 7 | 3 4 5 6 0 1 2 - - - 668 8 | 6 0 1 2 3 4 5 - - - 669 9 | 1 2 3 4 5 6 0 - - - 670\end{verbatim}} 671 672\subsubsection{Open Quasigroup Questions Answered} 673 674\paragraph{Orthogonal Mendelsohn Triple Systems (OMTS).} 675Corollary 5.2 of \cite{somts} states 676\begin{quote} 677The necessary condition for the existence of a pair of OMTS($v$), 678that is, $v\equiv$ 0 or 1 (mod 3), is also sufficient except for 679$v$=3,6 and possibly excepting $v\in \{9,10,12,18\}$. 680\end{quote} 681See \cite{somts} for definitions. The input 682{\small \begin{verbatim} 683 set(dp_transform). 684 list(usable). 685 f(x,x) = x. 686 h(x,x) = x. 687 f(x,f(y,x))=y. 688 h(x,h(y,x))=y. 689 f(x,y)!=u | f(z,w)!=u | h(x,y)!=v | h(z,w)!=v | x=z | y=w. 690 end_of_list. 691 list(passive). 692 properties(f(_,_), quasigroup). 693 properties(h(_,_), quasigroup). 694 end_of_list. 695\end{verbatim}} \noindent 696with the options ``\verb:-n9 -x1 -p:'' produces the following 697quasigroups, which correspond to a pair of orthogonal Mendelsohn 698triple systems of order 9. 699{\small \begin{verbatim} 700 Model #1 at 54.58 seconds (SPARC 2): 701 702 f | 0 1 2 3 4 5 6 7 8 h | 0 1 2 3 4 5 6 7 8 703 ------------------------ ------------------------ 704 0 | 0 8 5 2 7 4 3 6 1 0 | 0 2 6 4 3 1 8 5 7 705 1 | 8 1 7 6 3 2 5 4 0 1 | 5 1 0 8 2 3 7 6 4 706 2 | 3 5 2 8 6 0 4 1 7 2 | 1 4 2 6 7 8 0 3 5 707 3 | 6 4 0 3 8 7 1 5 2 3 | 4 5 7 3 0 6 2 8 1 708 4 | 5 7 6 1 4 8 2 0 3 4 | 3 8 1 0 4 7 5 2 6 709 5 | 2 6 1 7 0 5 8 3 4 5 | 7 0 8 1 6 5 3 4 2 710 6 | 7 3 4 0 2 1 6 8 5 6 | 2 7 3 5 8 4 6 1 0 711 7 | 4 2 8 5 1 3 0 7 6 7 | 8 6 4 2 5 0 1 7 3 712 8 | 1 0 3 4 5 6 7 2 8 8 | 6 3 5 7 1 2 4 0 8 713\end{verbatim}} \noindent 714An analogous search for OMTS(10) ran for several days without 715finding a model. 716 717\paragraph{QG3($2^8$).} A quasigroup of type $h^n$ has order $h*n$ 718and $n$ holes of size $h$. Frank Bennett posed \cite{bennett-email} 719the question of the existence of QG3($2^8$). (Mark Stickel had 720already answered positively the question of the existence of QG3($2^6$) 721\cite{bennett-email}.) 722The ANL-DP input 723{\small \begin{verbatim} 724 relation = 2 equality 725 relation same_hole 2 hole 726 function f 3 quasigroup_holey 727 end_of_symbols 728 729 f v0 v0 v0 same_hole v0 v0 . 730 -f v0 v1 v2 -f v1 v0 v3 f v3 v2 v1 . 731 -f v0 v1 v2 -f v0 v2 v1 = v0 v1 . 732 -f v0 v1 v2 -f v2 v1 v0 = v0 v1 . 733 end_of_clauses 734 735 same_hole 0 7 736 same_hole 1 8 737 same_hole 2 9 738 same_hole 3 10 739 same_hole 4 11 740 same_hole 5 12 741 same_hole 6 13 742 same_hole 14 15 743 end_of_assignments 744\end{verbatim}} \noindent 745with the options ``\verb:-n16 -p:'' produces the following holey quasigroup. 746{\small \begin{verbatim} 747 Model #1 at 76086.21 seconds (i468 DX2/66): 748 749 f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 750 ------------------------------------------------------ 751 0 | - 2 3 12 1 4 5 - 10 11 14 15 13 8 6 9 752 1 | 3 - 6 5 15 0 14 12 - 4 11 7 10 2 9 13 753 2 | 11 15 - 0 10 14 12 13 7 - 5 6 3 4 1 8 754 3 | 2 13 1 - 9 7 4 15 11 12 - 0 14 5 8 6 755 4 | 5 10 7 1 - 6 9 8 14 3 15 - 2 0 13 12 756 5 | 13 4 11 14 0 - 8 6 15 7 9 10 - 1 2 3 757 6 | 4 0 15 9 14 11 - 3 12 5 2 8 7 - 10 1 758 7 | - 6 8 13 2 9 15 - 5 14 4 12 1 11 3 10 759 8 | 14 - 4 6 3 2 10 9 - 0 13 5 15 7 12 11 760 9 | 15 3 - 11 6 8 7 1 13 - 12 14 0 10 4 5 761 10 | 6 5 14 - 7 15 11 2 9 1 - 13 8 12 0 4 762 11 | 8 12 10 2 - 1 3 14 6 13 7 - 9 15 5 0 763 12 | 10 9 0 8 13 - 1 11 4 15 6 3 - 14 7 2 764 13 | 9 14 12 15 5 3 - 10 2 8 0 1 4 - 11 7 765 14 | 1 7 13 4 12 10 0 5 3 6 8 2 11 9 - - 766 15 | 12 11 5 7 8 13 2 4 0 10 1 9 6 3 - - 767\end{verbatim}} \noindent 768(In case the reader is wondering why the holes are irregular in the 769lower right corner, the reason is that preliminary runs on QG3($2^6$) 770ran faster with a similar hole configuration than with a regular 771configuration.) 772 773\paragraph{QG7(17,5).} Frank Bennett posed \cite{bennett-email} the question 774of whether the the quasigroup identity (QG7a) $x(yx) = (yx)y$ implies 775either $(xy)x = x(yx)$ or $xy(yx) = y$. He suggested looking at 776models of order 17 with a hole of size 5, if they exist, as possible 777counterexamples. The identity (QG7b) $((xy)x)y = x$, which is 778conjugate-equivalent \cite{qg-survey} to (QG7a), is much easier to 779work with, so we put ANL-DP to work with the input 780{\small \begin{verbatim} 781 relation same_hole 2 hole 782 function f 3 quasigroup_holey 783 end_of_symbols 784 785 f v0 v0 v0 same_hole v0 v0 . 786 -f v0 v1 v2 -f v2 v0 v3 f v3 v1 v0 . 787 end_of_clauses 788 789 same_hole 12 13 790 same_hole 13 14 791 same_hole 14 15 792 same_hole 15 16 793 end_of_assignments 794\end{verbatim}} \noindent 795and the options ``\verb:-n17 -x1 -p:'', which produced the following 796{\small \begin{verbatim} 797 Model #1 at 172914.77 seconds (SPARC 2): 798 799 f | 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 800 --------------------------------------------------------- 801 0 | 0 2 1 16 13 11 12 8 5 15 14 7 4 6 9 10 3 802 1 | 16 1 3 2 10 13 9 12 15 4 6 14 5 7 8 11 0 803 2 | 3 16 2 0 15 9 14 10 12 7 5 13 11 8 4 6 1 804 3 | 1 0 16 3 8 15 11 14 6 12 13 4 10 9 5 7 2 805 4 | 8 13 10 15 4 6 5 16 2 14 0 12 9 3 11 1 7 806 5 | 13 9 15 11 16 5 7 6 14 3 12 1 8 2 10 0 4 807 6 | 11 12 9 14 7 16 6 4 13 0 15 2 3 10 1 8 5 808 7 | 12 10 14 8 5 4 16 7 1 13 3 15 2 11 0 9 6 809 8 | 15 6 5 12 14 1 2 13 8 10 9 16 0 4 7 3 11 810 9 | 7 15 12 4 0 14 13 3 16 9 11 10 1 5 6 2 8 811 10 | 5 14 13 6 12 3 0 15 11 16 10 8 7 1 2 4 9 812 11 | 14 4 7 13 2 12 15 1 9 8 16 11 6 0 3 5 10 813 12 | 10 11 4 5 3 2 8 9 7 6 1 0 - - - - - 814 13 | 9 8 6 7 11 10 3 2 0 1 4 5 - - - - - 815 14 | 4 5 8 9 1 0 10 11 3 2 7 6 - - - - - 816 15 | 6 7 11 10 9 8 1 0 4 5 2 3 - - - - - 817 16 | 2 3 0 1 6 7 4 5 10 11 8 9 - - - - - 818\end{verbatim}} \noindent 819The conjugate-equivalent quasigroup corresponding to (QG7a) was then 820generated and found to falsify the two identities in question, 821giving a counterexample to the problem. 822 823% \section{Conclusion} 824 825\nocite{qg-ijcai} 826 827\bibliographystyle{plain} 828% \bibliography{bib} 829 830\begin{thebibliography}{1} 831 832\bibitem{bennett-email} 833F.~E. Bennett. 834\newblock Correspondence by electronic mail, 1994. 835 836\bibitem{qg-survey} 837F.~E. Bennett and L.~Zhu. 838\newblock Conjugate-orthogonal Latin squares and related structures. 839\newblock In J.~H. Dinitz and D.~R. Stinson, editors, {\em Contemporary Design 840 Theory: A Collection of Surveys}, pages 41--96. John Wiley \& Sons, 1992. 841 842\bibitem{somts} 843F.~E. Bennett and L.~Zhu. 844\newblock Self-orthogonal {M}endelsohn triple systems. 845\newblock Preprint, 1994. 846 847\bibitem{qg-ijcai} 848M.~Fujita, J.~Slaney, and F.~E. Bennett. 849\newblock Automatic generation of some results in finite algebra. 850\newblock In {\em International Joint Conference on Artificial Intelligence}, 851 1993. 852 853\bibitem{otter3} 854W.~McCune. 855\newblock {\sc Otter} 3.0 {R}eference {M}anual and {G}uide. 856\newblock Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, Ill., 857 1994. 858 859\bibitem{finder3} 860J.~Slaney. 861\newblock FINDER version 3.0 notes and guide. 862\newblock Tech. report, Centre for Information Science Research, Australian 863 National University, 1993. 864 865\bibitem{qg-slaney-fujita-stickel} 866J.~Slaney, M.~Fujita, and M.~Stickel. 867\newblock Automated reasoning and exhaustive search: Quasigroup existence 868 problems. 869\newblock {\em Computers and Mathematics with Applications}, 1994. 870\newblock To appear. 871 872\bibitem{dp-trie} 873H.~Zhang and M.~Stickel. 874\newblock Implementing the {D}avis-{P}utnam algorithm by tries. 875\newblock Preprint, 1994. 876 877\end{thebibliography} 878 879 880\end{document} 881 882