We introduce in this paper a lightweight technique for reducing work repetition caused by non-chronological backtracking commonly practiced by DPLL-based SAT solvers. The presented technique can be viewed as a partial component caching scheme. Empirical evaluation of the technique reveals significant improvements on a broad range of industrial instances.
展开▼
