Evaluating search heuristics and optimization techniques in propositional satisfiability

This paper is devoted to the experimental evaluation of severalstate-of-the-art search heuristics and optimization techniques in proposi-tional satisfiability (SAT). The test set consists of random 3CNF formulasas well as real world instances from planning, scheduling, circuit analysis,bounded model checking, and security protocols. All the heuristics andtechniques have been implemented in a new library for SAT, called sim.The comparison is fair because in sim the selected heuristics and tech-niques are realized on a common platform. The comparison is significativebecause sim as a solver performs very well when compared to other state-of-the-art solvers.