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.