### Ondrej Mikle

Charles University in Prague

Faculty of Mathematics and Physics

Prague, 2007

## Strong Proof Systems

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