Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style


Ondrej Mikle

Charles University in Prague
Faculty of Mathematics and Physics
Prague, 2007

Strong Proof Systems



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.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

ISSN 1433-8092 | Imprint