Formalizacija, implementacija i primene SAT rešavača

Abstract

Software verification and formal theorem proving are intro- duced. SAT problem is informally defined and techniques used in modern SAT solvers are introduced. I Formalization - A higher order meta-logic used for all further formalizations of SAT problem and SAT solvers is described. A formalization of propositional logic of CNF formulae is given. Several abstract state transition systems for SAT (basic search, DPLL search, backjumping, learning, restarting, and conflict analysis) are formalized. For each of these systems, soundness, termination, completeness and, therefore, total correctness have been proved. II Implementation - The implementation of a core of a modern SAT solver is described in an imperative pseudocode whose correctness is proved by using Hoare logic. The classic DPLL procedure and the core of a modern SAT solver are embedded into higher order logic and the correctness of this form of implementation is proved. A flexible object-oriented architecture of a modern SAT solver is presented and the solver ArgoSAT is described. III Applications - Automated timetabling based on SAT solving is described. The SMT problem is introduced and applications of SAT solvers for its solving are described. The link grammars, used for natural language syntax descriptions, are introduced and possible applications of SAT solvers within link-grammar parsers are given. Discussion and Conclusions - Related work is discussed and comparison of the results obtained in this thesis with relevant related results is given. Possible directions of further work are given. Final conclusions are drawn