Beyond Unit Propagation in SAT Solving

摘要

The tremendous improvement in SAT solving has made SAT solvers a core engine for many real world applications. Though still being a branch-and-bound approach purposive engineering of the original algorithm has enhanced state-of-the-art solvers to tackle huge and difficult SAT instances. The bulk of solving time is spent on iteratively propagating variable assignments that are implied by decisions. In this paper we present two approaches on how to extend the broadly applied Unit Propagation technique where a variable assignment is implied iff a clause has all but one of its literals assigned to false. We propose efficient ways to utilize more reasoning in the main component of current SAT solvers so as to be less dependent on felicitous branching decisions.