Abstract
R-OBDD is a new Cook-Reckhow propositional proof system based on combination of OBDD proof system and resolution proof system. R-OBDD has the strength of OBDD proof system -- hard tautologies for resolution like $PHP_n$ or Tseitin contradictions have polynomially sized proofs in R-OBDD (R-OBDD p-simulates OBDD proof system as well as resolution). On the other hand, inference rules of R-OBDD are designed to be similar to inference rules of resolution, thus allowing to create a modified version of DPLL algorithm and possibly using heuristics used in various DPLL-like algorithms. This gives a possibility for a SAT solver more efficient than SAT solvers based on resolution proof system. We present design of a SAT solver, which is an adaptation of DPLL algorithm for the R-OBDD proof system. The algorithm is accompanied with proof of its correctness and we show that the run of the algorithm on an unsatisfiable formula can be transformed into tree-like refutation in the R-OBDD proof system.
1 Preliminaries 1.1 Propositional logic 1.2 Proof complexity 1.3 Resolution 1.3.1 Pigeonhole principle - PHPn 2 OBDD proof system 2.1 OBDD 2.2 Inference rules 2.3 Strength of OBDD proofs 3 R-OBDD 3.1 Motivation 3.2 Definitions 3.3 Inference rules 3.4 The proof system 4 Automated theorem proving in R-OBDD 4.1 R-OBDD solver DPLL modification for R-OBDD 4.2 Discussion
