Abstract:
Propositional Satisfiability (SAT) is often used as the underlying model for a significant number of applications in different fields of Computer Science and Engineering. Algorithmic solutions for SAT include, among others, local search, backtrack search and algebraic manipulation. In addition, algo- rithmic solutions used for solving other fundamental problems have been applied to solving SAT. In this paper we describe how to incorporate in SAT algorithms algorithmic strategies that are commonly used for solving decision problems associated with combinational circuits. In particular, we show that recur- sive learning can naturally be embedded in generic backtrack search algorithms for solving SAT. Fur- thermore, we provide empirical evidence that the proposed algorithm can be competitive in classes of instances commonly considered hard for existing SAT algorithms.