The Proof-Sensitive interpolation algorithms for propositional logic [1] aim at generating small interpolants in a lightweight manner. The algorithms are implemented in OpenSMT2 and can be used by changing a runtime parameter inside the smt2lib file, as seen here. The benchmarks from [4] and [5] can be found here.

This smt2 file provides a short UNSAT formula.

In order to generate an interpolant, we need to set the option

(set-option :produce-interpolants true)

and call

(get-interpolants)

after the sat-check.

Different interpolation algorithms can be used via the option

(set-option :interpolation-bool-algorithm <algo>)

<algo>

• 0 - M_s [1]
• 1 - P [2]
• 2 - M_w [3]
• 3 - PS [4]
• 4 - PS_w [4]
• 5 - PS_s [4]
• 6 - D_min [3]

This file contains this option set to PS.

By setting the option verbosity to 2, as is shown in this example, we can see that the following interpolant is generated when running

$ opensmt small_bool_itp_algo.smt2

; Interpolant: (or (not x) (not y))

Another useful feature is to certify that the interpolants are sound.

(set-option :certify-interpolants 1)

tests the soundness of the final interpolant, whereas level 2 tests the soundness of every partial interpolant of the resolution proof.

This file contains this option.

Running

$ opensmt small_bool_itp_algo_certify.smt2

we can see the interpolant certification log:

; Verifying final interpolant
        ; A -> I holds
        ; B -> !I holds
        ; Final interpolant is sound

1. An Interpolating Theorem Prover. McMillan, K. 
2. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Pudlák, P.
3. Interpolant Strength. D'Silva, V., Kroening, D,. Purandare, M., and Weissenbacher, G.
4. A Proof-Sensitive Approach for Small Propositional Interpolants. Alt, L., Fedyukovich, G., Hyvärinen, A. E. J., and Sharygina, N.
5. Controlled and Effective Interpolation. Alt, L.