# SAT-encoded Quasigroup (or Latin square) instances

Given a set S, a Latin square indexed by S is an |S|x|S| array such that each row and each column of the array is a permutation of the elements in S. |S| is called the order of the Latin square. A Latin square of order v is specified by:

• (1) (x * u = y, x * w = y) ==> u = w
• (2) (u * x = y, w * x = y) ==> u = w
• (3) (x * y = u, x * y = w) ==> u = w
• (4) (x * y = 0) | (x * y = 1) | ... | (x * y = (v-1))
Some additional constraints may be added. The constraints used here are named as follows:

 Name Constraint qg1 (x * y = u, z * w = u, v * y = x, v * w = z) ==> x = z qg2 (x * y = u, z * w = u, y * v = x, w * v = z) ==> x = z qg3 (x * y) * (y * x) = x qg4 (x * y) * (y * x) = y qg5 ((x * y) * x) * x = y qg6 (x * y) * y = x * (x * y) qg7 ((x * y) * x) * y = x

Table 1:Additional constraints for quasigroup instances.

#### Benchmark instances

A Latin square of order v is encoded by v^3 propositional variables. The number of propositional clauses are listed below:

 instance vars clauses satisfiable? qg1-07.cnf 343 68083 yes qg1-08.cnf 512 148957 yes qg2-07.cnf 343 68083 yes qg2-08.cnf 512 148957 yes qg3-08.cnf 512 10469 yes qg3-09.cnf 729 16732 no qg4-08.cnf 512 9685 no qg4-09.cnf 729 15580 yes qg5-09.cnf 729 28540 no qg5-10.cnf 1000 43636 no qg5-11.cnf 1331 64054 yes qg5-12.cnf 1728 90919 no qg5-13.cnf 2197 125464 no qg6-09.cnf 729 21844 yes qg6-10.cnf 1000 33466 no qg6-11.cnf 1331 49204 no qg6-12.cnf 1728 69931 no qg7-09.cnf 729 22060 yes qg7-10.cnf 1000 33736 no qg7-11.cnf 1331 49534 no qg7-12.cnf 1728 70327 no qg7-13.cnf 2197 97072 yes

Table 1: SAT-encodings of Quasigroup (or Latin square) instances.

The file qg1-07.cnf contains the propositional clauses in DIMACS format for Latin square of order 7 with constraint qg1, etc. These instances are used in [ZS00], where more details on Latin squares are given and the performances of a dozen of different implementations of the Davis-Putnam method were compared. In

#### Bibliography

 [ZS00] Hantao Zhang and Mark E. StickelImplementing the Davis-Putnam Method. Journal of Automated Reasoning, Special issue on Propositional Satisfiability , to appear, 2000

#### Acknowledgements

The instances have been contributed by Hantao Zhang.