A Complete Adaptive Algorithm for Propositional Satisfiability

An approach to propositional satisfiability using an adaptive procedure is described. Its main feature is a new branching rule, which is able to identify, at an early stage, hard sub-formulae. Such branching rule is based on a simple and easy computable criterion, whose merit function is updated by a learning mechanism, and guides the exploration of a clause-based branching tree. Completeness is guaranteed. Moreover, a new search technique named core search is used to speed-up the above procedure while preserving completeness. This is inspired by the well-known approaches of row and column generation used in mathematical programming. Encouraging computational results and comparisons are presented.