Silné důkazové systémy

Abstract

R-OBDD je nový Cook-Reckhowův důkazový systém pro výrokovou logiku založen na kombinaci OBDD důkazového systému a rezolučního důkazového systému. R-OBDD má sílu OBDD důkazového systému - tautologie s exponenciálně velkými důkazy v rezoluci jako PHPn nebo Tseitinovy kontradikce mají v R-OBDD systému polynomiální důkazy (R-OBDD p-simuluje jak OBDD důkazový systém, tak rezoluci). Na druhé straně, odvozovací pravidla R-OBDD systému byly navrhnuty, aby se podobaly odvozovacím pravidlům rezoluce. Tím pádem je možné vytvořit modifikaci DPLL algoritmu, která bude pracovat v R-OBDD systému a zároveň použít některé heuristiky známé z algoritmů založených na DPLL. Vzniká možnost vytvořit efektivnejší algoritmus na řešení problému splnitelnosti formule (SAT). Ukážeme návrh algoritmu, který je adaptací DPLL algoritmu pro R-OBDD důkazový systém. Přikldáme důkaz z jeho korektnosti a ukážeme, že jeho běh nad nesplnitelnou formulí je možné transformovat do stromového důkazu v R-OBDD systému.

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