Fulltext

Resolution proof transformation for compression and interpolation

Rollini, Simone ; Bruttomesso, Roberto ; Sharygina, Natasha ; Tsitovich, Aliaksei

In: Formal Methods in System Design, 2014, vol. 45, no. 1, p. 1-41

Add to personal list
    Title
    • Resolution proof transformation for compression and interpolation
    Author
    • Rollini, Simone. University of Lugano, Lugano, Switzerland
    • Bruttomesso, Roberto. Atrenta Advanced R&D of Grenoble, Grenoble, France
    • Sharygina, Natasha. University of Lugano, Lugano, Switzerland
    • Tsitovich, Aliaksei. Phonak, Stäfa, Switzerland
    Document Type
    • Postprint
    Language
    • English
    Published in
    • Formal Methods in System Design, 2014, vol. 45, no. 1, p. 1-41. Springer US; http://www.springer-ny.com
    Other Version
    OAI-PMH Identifier
    • oai:doc.rero.ch:326363
    Summary
    Verification methods based on SAT, SMT, and theorem proving often rely on proofs of unsatisfiability as a powerful tool to extract information in order to reduce the overall effort. For example a proof may be traversed to identify a minimal reason that led to unsatisfiability, for computing abstractions, or for deriving Craig interpolants. In this paper we focus on two important aspects that concern efficient handling of proofs of unsatisfiability: compression and manipulation. First of all, since the proof size can be very large in general (exponential in the size of the input problem), it is indeed beneficial to adopt techniques to compress it for further processing. Secondly, proofs can be manipulated as a flexible preprocessing step in preparation for interpolant computation. Both these techniques are implemented in a framework that makes use of local rewriting rules to transform the proofs. We show that a careful use of the rules, combined with existing algorithms, can result in an effective simplification of the original proofs. We have evaluated several heuristics on a wide range of unsatisfiable problems deriving from SAT and SMT test cases.