Propositional satisfiability (SAT) is a fundamental problem of immense practical importance. While SAT is NP-complete when clauses can contain 3 literals or more, the problem can be solved in linear time when the given formula contains only binary clauses (2SAT). Many complete search algorithms for SAT solving have taken advantage of 2SAT information that occurs in the statement of the problem in order to simplify the solving process, only one that we are aware of uses 2SAT information that arises in the process of the search, as clauses are simplified. There are a number of possibilities for making use of 2SAT information to improve the SAT solving process: maintaining 2SAT satisfiability during search, detecting unit consequences of the 2SAT clauses, and Krom subsumption using 2SAT clauses. In this paper we investigate the tradeoffs of increasing complex 2SAT handling versus the search space reduction and execution time. We give experimental results illustrating that the SAT solver resulting from the best tradeoff is competitive with state of the art Davis-Putnam methods, on hard problems involving a substantial 2SAT component.
展开▼
