PeRIPLO System Description

Overview

PeRIPLO is an open-source SAT-solver written in C++, built on MiniSAT 2.2.0., currently released under the GNU General Public Licence.

The tool was born from OpenSMT to provide resolution proof manipulation and interpolant generation routines specifically for SAT-based model checking in FunFrog and eVolCheck.

PeRIPLO accepts as input a SAT benchmark in SMT-LIB2 format. The tool can be used both as a standalone program and as a library; its routines are respectively accessible via configuration file and via API.

Proof Logging and Transformation

If the input benchmark is unsatisfiable, PeRIPLO is able to output a resolution proof of unsatisfiability, in SMT-LIB2 or in DOT format.

The tool allows to manipulate and compress resolution proofs, by means of the following techniques:

  • the Local Transformation Framework of [1] and [2]
  • the Recycle Pivots (with Intersection) method of [3] and [4]
  • a variant of the Lower Units method of [4]
  • a variant of the Structural Hashing method of [5]

An overview of the techniques implemented in PeRIPLO can be found in [9].

Interpolant Generation

PeRIPLO implements the Labeled Interpolation System of [6] to produce interpolants.

The tool allows to generate both single interpolants and sequences of interpolants, addressing the following properties as used in SAT-based model checking:

  • Path Interpolation
  • Simultaneous Abstraction
  • Generalized Simultaneous Abstraction
  • State-Transition Interpolation
  • Tree Interpolation

These properties and their relationship with the Labeled Interpolation System are discussed in [7] and [8].

Future Work

New features and capabilities will be added whenever needed. Comments, suggestions and requests are very welcome at rollinis at usi.ch .

 

References

  1. R. Bruttomesso, S.F. Rollini, N. Sharygina, and A. Tsitovich. Flexible Interpolation with Local Proof Transformations. In ICCAD, 2010.
  2. S.F. Rollini, R. Bruttomesso and N. Sharygina. An Efficient and Flexible Approach to Resolution Proof Reduction. In HVC, 2010.
  3. O. Bar-Ilan, O. Fuhrmann, S. Hoory, O. Shacham and O. Strichman. Linear-Time Reductions of Resolution Proofs. In HVC, 2008.
  4. P. Fontaine, S. Merz and B. W.Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. In CADE, 2011.
  5. S. Cotton. Two Techniques for Minimizing Resolution Proofs. In SAT, 2010.
  6. V. D'Silva, D. Kroening, M. Purandare and G. Weissenbacher. Interpolant Strength. In VMCAI, 2010.
  7. S.F. Rollini, O. Sery and N. Sharygina. Leveraging Interpolant Strength in Model Checking. In CAV, 2012.
  8. A. Gurfinkel, S.F. Rollini and N. Sharygina. Interpolation Properties and SAT-based Model Checking. In ATVA, 2013
  9. S.F. Rollini, R. Bruttomesso, N. Sharygina and A.Tsitovich. Resolution Proof Transformation for Compression and Interpolation.