PeRIPLO System Description
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  and 
- the Recycle Pivots (with Intersection) method of  and 
- a variant of the Lower Units method of 
- a variant of the Structural Hashing method of 
An overview of the techniques implemented in PeRIPLO can be found in .
PeRIPLO implements the Labeled Interpolation System of  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  and .
New features and capabilities will be added whenever needed. Comments, suggestions and requests are very welcome at rollinis at usi.ch .
- R. Bruttomesso, S.F. Rollini, N. Sharygina, and A. Tsitovich. Flexible Interpolation with Local Proof Transformations. In ICCAD, 2010.
- S.F. Rollini, R. Bruttomesso and N. Sharygina. An Efficient and Flexible Approach to Resolution Proof Reduction. In HVC, 2010.
- O. Bar-Ilan, O. Fuhrmann, S. Hoory, O. Shacham and O. Strichman. Linear-Time Reductions of Resolution Proofs. In HVC, 2008.
- P. Fontaine, S. Merz and B. W.Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. In CADE, 2011.
- S. Cotton. Two Techniques for Minimizing Resolution Proofs. In SAT, 2010.
- V. D'Silva, D. Kroening, M. Purandare and G. Weissenbacher. Interpolant Strength. In VMCAI, 2010.
- S.F. Rollini, O. Sery and N. Sharygina. Leveraging Interpolant Strength in Model Checking. In CAV, 2012.
- A. Gurfinkel, S.F. Rollini and N. Sharygina. Interpolation Properties and SAT-based Model Checking. In ATVA, 2013
- S.F. Rollini, R. Bruttomesso, N. Sharygina and A.Tsitovich. Resolution Proof Transformation for Compression and Interpolation.