Search

Haken proved that every resolution refutation of the pigeonhole formula has at least exponential size. Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size. Here we show that any arbitrary OBDD refutation of the pigeonhole formula has an exponential size, too: we prove that the size of one of the intermediate OBDDs is at least $\Omega(1.025^n)$.

Equality Logic with uninterpreted functions is used for proving the equivalense or refinement between systems (hardware verification, compiler translation, etc). Current approaches for deciding this type of formulas use a transformation of an equality formula to the propositional one of larger size, and then any standard SAT checker can be applied. We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called ER. For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT.

The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the procedure can adopt its heuristics. Therefore the procedure can be used as a basis for efficient implementations of satisfiability checkers for EUF. A part of the introduced method is a technique for reducing the size of formulas, which can also be used as a preprocessing step in other approaches for checking satisfiability of EUF formulas.

Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.

Item does not contain fulltext

The logic of equality and uninterpreted functions (EUF) has been proposed for processor verification. This paper presents a new data structure called Binary Decision Diagrams for representing EUF formulas (EUF-BDDs). We define EUF-BDDs similar to BDDs, but we allow equalities between terms as labels instead of Boolean variables. We provide an approach to build a reduced ordered EUF-BDD (EUF-ROBDD) and prove that every path to a leaf is satisfiable by construction. Moreover, EUF-ROBDDs are logically equivalent representations of EUF-formulae, so they can also be used to represent state spaces in symbolic model checking with data.

In dit proefschrift presenteren we een aantal technieken om vervulbaarheid (satisfiability) vast te stellen binnen beslisbare delen van de eerste orde logica met gelijkheid. Het doel van dit proefschrift is voornamelijk het ontwikkelen van nieuwe technieken in plaats van het ontwikkelen van een effici¨ente implementatie om vervulbaarheid vast te stellen. Als algemeen logisch raamwerk gebruiken we de eerste orde predikaten logica zonder kwantoren. We beschrijven enkele basisprocedures om vervulbaarheid van propositionele formules vast te stellen: de DP procedure, de DPLL procedure, en een techniek gebaseerd op BDDs. Deze technieken zijn eigenlijk families van algoritmen in plaats van losse algoritmen. Hun gedrag wordt bepaald door een aantal keuzen die ze maken gedurende de uitvoering. We geven een formele beschrijving van resolutie, en we analyseren gedetailleerd de relatie tussen resolutie en DPLL. Het is bekend dat een DPLL bewijs van onvervulbaarheid (refutation) rechtstreeks kan worden getransformeerd naar een resolutie bewijs van onvervulbaarheid met een vergelijkbare lengte. In dit proefschrift wordt een transformatie ge¨introduceerd van zo’n DPLL bewijs naar een resolutie bewijs dat de kortst mogelijke lengte heeft. We presenteren GDPLL, een generalisatie van de DPLL procedure. Deze is bruikbaar voor het vervulbaarheidsprobleem voor beslisbare delen van de eerste orde logica zonder kwantoren. Voldoende eigenschappen worden ge¨identificeerd om de correctheid, de be¨eindiging en de volledigheid van GDPLL te bewijzen. We beschrijven manieren om vervulbaarheid vast te stellen binnen de logica met gelijkheid en niet-ge¨interpreteerde functies (EUF). Dit soort logica is voorgesteld om abstracte hardware ontwerpen te verifi¨eren. Het snel kunnen vaststellen van vervulbaarheid binnen deze logica is belangrijk om dergelijke verificaties te laten slagen. In de afgelopen jaren zijn er verschillende procedures voorgesteld om de vervulbaarheid van dergelijke formules vast te stellen. Wij beschrijven een nieuwe aanpak om vervulbaarheid vast te stellen van formules uit de logica met gelijkheid die in de conjunctieve normaal vorm zijn gegeven. Centraal in deze aanpak staat ´e´en enkele bewijsregel genaamd gelijkheidsresolutie. Voor deze ene regel bewijzen wij correctheid en volledigheid. Op grond van deze regel stellen we een volledige procedure voor om vervulbaarheid van dit soort formules vast te stellen, en we bewijzen de correctheid ervan. Daarnaast presenteren we nog een nieuwe procedure om vervulbaarheid vast te stellen van EUF-formules, gebaseerd op de GDPLL methode. Tot slot breiden we BDDs voor propositionele logica uit naar logica met gelijkheid. We bewijzen dat alle paden in deze uitgebreide BDDs vervulbaar zijn. In een constante hoeveelheid tijd kan vastgesteld worden of de formule een tautologie is, een tegenspraak is, of slechts vervulbaar is.

The logic of equality with uninterpreted functions (EUF) has been proposed for processor verification. We describe EDPLL, a calculus for proving satisfiability of formulas in this kind of logic. Being based on the DPLL procedure, EDPLL can adopt heuristics developed for this method.

datatypes can be viewed as sorted ground term algebras. Unification can be used to solve conjunctions of equations. We give a new algorithm to extend this to the full quantifier free fragment, i.e. including formulas with disjunction and negation. The algorithm is based on unification (to deal with equality) and DPLL (to deal with propositional logic). In this paper we present our algorithm as an instance of a generalized DPLL algorithm. We prove soundness and completeness of the class of generalized DPLL algorithms, in particular for the algorithm for ground term algebras.

We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called equality resolution (ER). For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT. Parts of the theory we developed for proving completeness of the proof rule and the algorithm are of interest in itself: we give techniques for removing clauses preserving unsatisfiability, and we give a general theorem globalizing a local commutation criterion for different proof systems. Keywords: equality logic, satisfiability, resolution.

We compare two standard techniques for satisfiability (SAT), which are basic for verification of microprocessor systems. We propose an approach for construction of shorter resolution refutations based on a standard approach called DPLL.