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.