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. Computing  the weighted sum of the inequalities from the conflict, with weights being the Farkas coefficients, results in a contradictory inequality. Given a partitioning of such an 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 this interpolation algorithm as Farkas interpolation, but it is known also as McMillan interpolation as it was presented in his paper [1].

Such a weighted sum of the A-part of the conflict is 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. This yields a separate inequality for each component. The conjunction of these inequalities 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

Note: This section describes an updated set of experiments, for the original description, see the section below!

We experimented with the application of decomposed interpolants in a model checking algorithm PD-KIND [3], implemented in SALLY. Compared to our previous experiments, we have used newer versions of the SMT solvers and an updated version of the model checker, extended to support also different interpolation algorithms of MathSAT.

The version of SALLY used in the experiments currently lives in a forked repository. The precise commit is abf372c. The version of OpenSMT used in these experiments can be found in its GitHub repository, the commit is 686eef9. 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. We also used MathSAT 5.6.0 and Yices2 2.6.0 in our experiments.

Compared to the previous experiments, we ran SALLY with additional options which improve the performance of the PD-KIND engine. When using OpenSMT as the interpolation engine, we ran SALLY with the following command

sally --solver y2o2 --solver-logic QF_LRA --engine pdkind --pdkind-minimize-frames

--pdkind-minimize-interpolants --yices2-mode dpllt --opensmt2-simplify_itp 4 --opensmt2-itp N -i <input_file>

>

where N is 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 --pdkind-minimize-frames

--pdkind-minimize-interpolants --yices2-mode dpllt mathsat5-la-interpolation-mode N -i <input_file>

where N is 0 for Farkas interpolation; 2 for dual Farkas interpolation; and 1 for decomposed interpolants computed by MathSAT heuristic (described in [4]).
 
The benchmarks used in the experiments are available here. Note that some benchmarks are accompanied by .options file. Options found in this file must be added to the command line when running SALLY on such benchmarks.
The raw data collected from the experiments for each benchmark can be found here. Consult the README.md file included for more information.
 
The results from 100 repeated runs (with a different random seed) on selected benchmarks can be found here. These compare the performance of Farkas and decomposing interpolation in OpenSMT on benchmarks which were solved by the latter but not the former in our previous experiments.
 

Experiments - TACAS'19

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

We experimented with the application of decomposed interpolants in a model checking algorithm PD-KIND [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.

 

Reference:

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).

4. Cimatti A., Griggio A., Sebastiani R.: Efficient generation of Craig interpolants in satisfiability modulo theories, ACM Transactions on Computational Logic, Volume 12, Issue 1, 2010, https://dl.acm.org/doi/10.1145/1838552.1838559