Boolean Equi-propagation for Optimized SAT Encoding

Amit Metodi, Michael Codish, Vitaly Lagoon, and Peter J. Stuckey

Abstract. We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings and leads to speed-ups in solving times.

The paper can be found here.

Experiments


Quasigroup Completion Problem

instance Compiler Sugar (v1.14.7) 3D CSP'08 OSC'09 FS'09
num un/sat comp
(sec.)
cnf size
(clauses)
SAT
(sec.)
cnf size
(clauses)
SAT
(sec.)
cnf size
(clauses)
SAT
(sec.)
(sec.) (sec.) (sec.)
1 sat 0.41 6509 2.46 140315 37.36 6507 0.09 31.55 34.81 6.44
2 sat 0.33 7475 0.02 140920 234.70 7438 0.74 137.60 99.84 44.80
3 sat 0.38 6531 0.02 140714 17.02 6512 0.02 10.57 12.25 2.53
4 sat 0.38 6818 0.61 141581 90.64 6811 0.08 47.24 273.36 157.58
5 sat 0.35 7082 0.32 140431 206.03 7099 0.14 27.33 24.87 22.30
6 sat 0.33 7055 0.45 140625 67.84 7044 1.11 35.78 108.60 12.58
7 sat 0.33 7711 2.36 142200 60.97 7684 0.08 57.23 67.32 341.62
8 sat 0.35 7426 0.05 140784 34.43 7367 0.04 43.88 1.52 6.08
9 sat 0.37 6602 0.28 137589 33.76 6609 0.41 25.15 9.52 3.01
10 sat 0.36 6784 0.17 142303 50.86 6799 0.06 26.16 27.80 12.66
11 unsat 0.45 6491 0.05 140603 39.02 6534 0.03 19.47 30.92 5.30
12 unsat 0.23 1 0.00 139037 0.58 7393 0.00 0.36 0.05 0.81
13 unsat 0.28 1 0.00 141295 0.90 6555 0.00 1.47 0.16 0.80
14 unsat 0.28 1 0.00 140706 2.25 7173 0.00 1.40 0.29 0.80
15 unsat 0.38 6063 0.05 140224 35.93 6104 0.06 32.39 58.41 4.77
Table 1: QCP results for 25x25 instances with 264 holes taken from Third International CSP Solver Competition

Downloads:
* QCP 25x25 with 264 holes instances
* QCP 25x25 with 264 holes order encoding CNFs (.cnf) and maps (.map)
* QCP 25x25 with 264 holes 3D encoding CNFs (.cnf) and maps (.map)
* QCP 25x25 with 264 holes sugar model (.sugar)

inst.
800
holes
order enc. 3D enc.
cnf size
(mil. clauses)
SAT
(sec.)
cnf size
(mil. clauses)
SAT
(sec.)
1 0.11 18.24 0.13 6.87
2 0.11 2.88 0.13 3.70
3 0.11 6.54 0.13 2.50
4 0.11 0.34 0.13 1.47
5 0.11 21.50 0.13 7.09
6 0.11 0.68 0.13 1.78
7 0.11 13.79 0.13 2.75
8 0.11 25.16 0.13 0.48
9 0.11 9.46 0.13 12.92
10 0.11 4.59 0.13 1.43
inst.
1000
holes
order enc. 3D enc.
cnf size
(mil. clauses)
SAT
(sec.)
cnf size
(mil. clauses)
SAT
(sec.)
1 0.31 0.40 0.38 27.78
2 0.31 0.39 0.38 0.33
3 0.31 0.39 0.39 19.76
4 0.31 0.39 0.38 8.73
5 0.31 0.39 0.38 0.35
6 0.30 0.39 0.37 3.13
7 0.30 9.22 0.37 0.34
8 0.32 0.39 0.39 0.36
9 0.31 0.38 0.38 4.21
10 0.30 0.65 0.37 8.26
Table 2: QCP results for 40x40 instances generated using lsencode

Downloads:
* QCP 40x10 with 800 holes instances (.pls)
* QCP 40x10 with 800 holes order encoding CNFs (.cnf) and maps (.map)
* QCP 40x10 with 800 holes 3D encoding CNFs (.cnf) and maps (.map)
* QCP 40x10 with 1000 holes instances (.pls)
* QCP 40x10 with 1000 holes order encoding CNFs (.cnf) and maps (.map)
* QCP 40x10 with 1000 holes 3D encoding CNFs (.cnf) and maps (.map)


Nonograms

instance Compiler BGU
(v1.0.2)

(sec.)
Wolter's
(v1.09)

(sec.)
Sugar (v1.14.7) (1)
id size comp
(sec.)
cnf size
(clauses)
SAT
(sec.)
comp
(sec.)
cnf size
(clauses)
SAT
(sec.)
9717 (30x30) 0.13 14496 124.43 1.61 27892 21.03
10000 (50x40) 0.28 44336 40.66 2.55 68732 83.92
9892 (40x50) 0.57 30980 0.44 2.51 75471 5.92
2556 (45x65) 0.13 2870 0.00 15.85 0.4 2.12 45002 0.10
10088 (63x52) 0.64 78482 1.26 0.27 0.08 3.07 122290 2.50
2712 (47x47) 0.31 43350 0.92 5.98 4.95 2.36 69202 1.70
8478 (50x50) 0.40 51027 0.95 0.89 2.41 80939 10.76
6727 (80x80) 1.11 156138 2.86 0.5 0.17 5.40 241792 4.08
8098 (19x19) 0.02 3296 0.06 209.54 8.63 0.74 4834 0.03
6574 (25x25) 0.10 7426 0.03 37.56 2.94 1.30 15325 0.07
Table 3: Human Nonograms Results (300 sec. timeout). Puzzles exported from webpbn export page.

(1) Using input based on Sugar's example and searching for a single solution (while the others search for two solutions).

Downloads:
* The aboved human puzzles (.nin)
* Compiled CNF (.cnf) and, maps (.map)
* Sugar models (.sugar)

time (sec.)
0.20 0.50 1.00 10.00 30.00 60.00
BGU 279 3161 4871 4978 4989 4995
Wolter's 4635 4782 4840 4952 4974 4976
Compiler 13 4878 4994 5000 5000 5000
Table 4: 5,000 Random Nonograms Results used in the webpbn nonogram survey page.

Downloads:
* 5000 Random 30x30 Nonograms puzzles (.nin)


BIBD

instance Compiler (SymB) Minion (v0.10) SatELite (SymB) Sugar (v1.14.7) (SymB)
<v, b, r, k, λ> comp
(sec.)
cnf size
(clauses)
SAT
(sec.)
[M'06]
(sec.)
SymB
(sec.)
SymB+
(sec.)
prepro
(sec.)
cnf size
(clauses)
SAT
(sec.)
comp
(sec.)
cnf size
(clauses)
SAT
(sec.)
<7,350,150,3,50> 1.34 494131 1.23 0.47 1.12 0.38 1.27 566191 1.65 39.36 1607830 8.99
<7,420,180,3,60> 1.65 698579 1.73 0.54 1.36 0.42 1.67 802576 2.18 12.01 2488136 13.24
<7,560,240,3,80> 3.73 1211941 13.60 0.66 1.77 0.52 2.73 1397188 5.18 11.74 2753113 36.43
<8,84,42,4,18> 0.25 64432 0.17 2.41 0.70 0.31 73780 0.15 3.01 206092 0.70
<8,98,49,4,21> 0.33 84993 0.23 5.63 1.54 0.34 97588 0.33 3.18 350711 1.41
<12,132,33,3,6> 0.95 180238 0.73 5.51 1.76 1.18 184764 0.57 83.37 1332241 7.09
<13,26,8,4,2> 0.12 17570 0.05 5.46 0.47 0.16 0.22 17391 0.10 13.50 95977 0.23
<15,45,24,8,12> 0.51 116016 8.46 75.87 0.64 134146 4.24 466086
<15,70,14,3,2> 0.56 81563 0.39 12.22 1.42 0.31 1.02 79542 0.20 23.58 540089 1.87
<16,80,15,3,2> 0.81 109442 0.56 107.43 13.40 0.35 1.14 105242 0.35 64.81 623773 2.26
<19,19,9,9,4> 0.23 39931 0.09 53.23 38.30 0.31 0.4 44714 0.09 2.27 125976 0.49
<19,57,9,3,1> 0.34 113053 0.17 1.71 0.35 10.45 111869 0.14 - -
<21,21,5,5,1> 0.02 0 0.00 1.26 0.67 0.15 0.01 0 0.00 31.91 3716 0.01
<25,25,9,9,3> 0.64 92059 1.33 0.92 1.01 97623 8.93 42.65 569007 8.52
<25,30,6,5,1> 0.10 24594 0.06 1.37 0.31 1.2 23828 0.05 16.02 93388 0.42
<31,31,6,6,1> 0.08 8571 0.03 2.10 0.36 0.28 8001 0.03 10.14 64388 0.31
Table 5: BIBD results (180 sec. timeout)

Downloads:
* Compiled CNFs (.cnf) and maps (.map)
* Minion models (.minion)
* Sugar models (.sugar) and maps (.map)
* Before SatELite CNFs (.cnf) and maps (.map)
* After SatELite CNFs (.cnf) and maps (.map)