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. © 2011 Springer-Verlag.
CITATION STYLE
Kaufmann, M., & Kottler, S. (2011). Beyond unit propagation in SAT solving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6630 LNCS, pp. 267–279). https://doi.org/10.1007/978-3-642-20662-7_23
Mendeley helps you to discover research relevant for your work.