Effect of Restarts on Clause Learning

This page contains detailed results of a superset of the experiments described in The Effect of Restarts on the Efficiency of Clause Learning, Jinbo Huang, Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI-07). Executables of the SAT solver used to run these experiments, Tinisat 0.1, are also available for download.

Download Tinisat 0.1

Platform	Binary	Zipped
Linux	47 KB	22 KB
Linux (statically linked)	1.1 MB	407 KB
Mac	52 KB	19 KB
Windows	72 KB	39 KB
Cygwin	134 KB	44 KB

Usage: tinisat cnf-file [x [y]] where x and y are numbers. When both x and y are given restart policy (x, y) is used. When only x is given (Luby's, unit=x) is used. By default (Luby's, unit=32) is used. Using a sufficiently large x will effectively turn off restarts.

Results

Tinisat-N (no restarts)	Tinisat-L1 (Luby's, unit=1)	Other Solvers:
Tinisat-B (550, 1)	Tinisat-L2 (Luby's, unit=2)	BerkMin
Tinisat-Z (700, 1)	Tinisat-L4 (Luby's, unit=4)	Chaff II
Tinisat-S (16000, 1)	Tinisat-L8 (Luby's, unit=8)	MiniSat v1.14
Tinisat-G (32, 1.1)	Tinisat-L16 (Luby's, unit=16)	RSat v1.03
Tinisat-M (100, 1.5)	Tinisat-L32 (Luby's, unit=32)	Siege v4
	Tinisat-L64 (Luby's, unit=64)
	Tinisat-L128 (Luby's, unit=128)
	Tinisat-L256 (Luby's, unit=256)
	Tinisat-L512 (Luby's, unit=512)
	Tinisat-L1024 (Luby's, unit=1024)
	Tinisat-L2048 (Luby's, unit=2048)
	Tinisat-L4096 (Luby's, unit=4096)
	Tinisat-L8192 (Luby's, unit=8192)

Notes

Benchmarks used for the experiments are from Miroslav Velev's SAT benchmarks.
Experiments were conducted on a cluster of 16 AMD Athlon 64 processors running at 2GHz with 2GB of RAM under SuSE Linux 9.3 Professional. A time limit of 2 hours was imposed on all runs of the solvers.