max planck institut
informatik
informatik
Update 25.02.09: On this page we report on the progress of iLoRe, a prover which implements a decision procedure for SMT problems containing certain kinds of quantified formulas. In particular, it features both an eager and an incremental approach to local reasoning. This page gives results which did not fit into the submission "Incremental Instance Generation in Local Reasoning" to CAV 09 because of space restrictions, or which have been achieved after the submission.
Below you can first find some additional benchmarks carried out with version 0.1.4 of iLoRe, which is the version that we also used for the benchmarks in the paper submission. Version 0.1.4 does not support the fine-grained instantiation LIG_uc (with unsatisfiable cores), so these comparisons are only between the eager and the coarse-grained LIG method (which always takes the maximal LIG inference).
After that, we have some new results for version 0.1.5, which includes a preliminary implementation of the fine-grained LIG_uc procedure (limiting generation of instances additionally by computation of unsatisfiable cores). Version 0.1.5 also features more efficient detection of saturation for the incremental method, and we include first results for satisfiable benchmarks.
We compare the incremental and the eager approach to local reasoning on benchmark problems taken from SMT-LIB and augmented with additional axioms which satisfy a locality property with respect to the base theory. Problems from QF_UFLIA/wisas/ and QF_UFLIA/mathsat/Wisa have been augmented with monotonicity or injectivity axioms (for all functions or only the (select_)format function, respectively). Thus, for every original problem from these directories, we tested 4 different extended problems. Below is a scatter plot comparing the behaviour of the incremental and the eager method on the extensions of all problems from QF_UFLIA/wisas:
While the incremental method is faster on the majority of problems, there are some for which the incremental method needs much more time than the eager one. These are 10 problems from SMT-LIB (4 different extensions of each problem in the scatter plot), which have in common that already the original problems are unsatisfiable, but solving the satisfiability problem for the original problem is actually much harder than adding a few hundred axiom instances and solving the extended problem.
If we only look at those problems from QF_UFLIA/wisas/ which are originally satisfiable, the picture is quite different:
Here, the incremental method is clearly superior, with only a few problems where the eager method is considerably faster, but many in which the eager methods needs more than 10 times as long as the incremental one.
Finally, we tested the implementation on problems from QF_UFLIA/mathsat/Wisa (modified as above), but the results are not very meaningful: the problems are too easy, both methods solve each of them in less than 0.2 s:
We have some new results with a preliminary version of the LIG_uc algorithm. In the pictures below you can see how the algorithm with unsatisfiable cores compares to LIG without unsatisfiable cores and the eager instantiation method. The first picture is for the blowup example as given in the paper (but carried out on a different machine, so times are not comparable to those in the paper). The second picture is for a version of the problem that is made satisfiable by leaving out the last constraint (F).
We can see that LIG_uc needs a bit more time than LIG on the unsatisfiable problems. A fine-grained analysis of the usage of processing time for different tasks shows that for larger problems, 70 to 80% of the overall runtime is used on the unsatisfiable core extraction. So even though this is a preliminary implementation, the only way to improve significantly on these times is to change the unsat core extraction (which resides in the SMT solver).
The picture is different for the satisfiable problems. Here, LIG_uc is significantly faster than even LIG on larger problems.
We cannot currently compare LIG_uc to the other methods for the WiSA benchmarks from above because the beta version of Z3 2.0 which we use for unsatisfiable core extraction produces errors on these problems. We are in contact with Leonardo de Moura in order to fix these problems.