Decomposed interpolants

Decomposed interpolants generalize the traditional way of computing interpolants in linear real arithmetic (LRA). For every LRA conflict there exists a vector of Farkas coefficients witnessing its unsatisfiability. When a weighted sum of the inequalities from the conflict, with weigths being the Farkas coefficients, the result is an contradictory inequality. Given a partitioning of such unsatisfiable system of linear inequalities into an A and B part, the interpolant is typically computed as the weighted sum of the A part. We refer to interpolantion algorithm as Farkas interpolantion, but it is known also as McMillan interpolation as it was presented in his paper [1].

Farkas interpolant for a given LRA conflict is thus always a single inequality. Our approach tries to break down the Farkas interpolant using techniques from linear algebra to identify independent components of the vector of Farkas coefficients. If more than one component is identified the weighted sums are computed for each component separately, yielding more than one inequality. The conjunction of inequalities obtained this way is also an interpolant for the original problem. Moreover, it is logically stronger than Farkas interpolant. For more details see our TACAS'19 paper.

 

Experiments

This section desribes in more detail our experiments with the usage of decomposed interpolants in model-checking scenario published in [2]

We experimented with application of decomposed interpolants in a model checking algorithm PDKIND [3], implemented in SALLY.

The version of SALLY used in the experiments currently lives in a forked repository. The precise commit is tagged as tacas19. The version of OpenSMT used in these experiments is also tagged with the same tag, tacas19. Follow these instructions to compile and install OpenSMT. To print the statistics about the decomposed interpolants, set the cmake option PRINT_DECOMPOSED_STATS to ON. Yices2 is also required.

The benchmarks were run with the following command:

sally --solver y2o2 --solver-logic QF_LRA --engine pdkind -i <input_file> --opensmt2-simplify_itp 2 --opensmt2-itp N

where N can be:

  • 0 for Farkas interpolation
  • 2 for dual Farkas interpolation
  • 4 for decomposed interpolants
  • 5 for dual decomposed interpolants

 

For the runs with MathSAT we used the following command:

sally --solver y2m5 --solver-logic QF_LRA --engine pdkind -i <input_file> --y2m5-mathsat5-flatten

The set of benchmarks can be found here. It is a combination of benchmarks provided by SALLY from here and here.

The results per benchmark can be found here.

The results for running the same benchmark with different random seed for OpenSMT can be found here.

 


1. McMillan, K.L., An interpolating theorem prover, Theoretical Computer Science, Volume 345, Issue 1, 2005, pp. 101-121, ISSN 0304-3975.

2. Blicha M., Hyvärinen A.E.J., Kofroň J., Sharygina N. (2019) Decomposing Farkas Interpolants. In: Vojnar T., Zhang L. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019. Lecture Notes in Computer Science, vol 11427. Springer, Cham

3. Jovanović, D., Dutertre, B.: Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD). pp. 85–92 (Oct 2016).