SAT with partial clauses and back-leaps

This paper presents four new powerful SAT optimization techniques: partial clauses, back-leaps, immediate implications, and local decisions. These optimization techniques can be combined with SAT mechanisms used in Chaff, SATO, and GRASP to develop a new solver that significantly outperforms its predecessors on a large set of benchmarks. Performance improvements for standard benchmark groups vary from 1.5x to 60x. Performance improvements measured using VLIW microprocessor benchmarks amount to 3.31 x.