[Back]

W. Schreiner, F. Reichl:
"First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving";
Talk: International Symposium on Symbolic Computation in Software Science, Linz; 2021-09-08 - 2021-09-10; in: "Electronic Proceedings in Theoretical Computer Science", (2021), ISSN: 2075-2180; 99 - 113.

formulas
over finite domains supported by the mathematical model checker RISCAL: first, the original
approach of "semantic evaluation" (based on an implementation of the denotational semantics of the
RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving
translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation
of the two approaches and a discussion of their fundamental pros and cons, we quantitatively
evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life
applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices,
and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic
evaluation), the various SMT solvers exhibit great performance differences. More important, we
identify classes of formulas where semantic evaluation is able to compete with (or even outperform)
satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas
to SMT-LIB formulas as well as in the current SMT technology.

http://dx.doi.org/10.4204/EPTCS.342.9

https://publik.tuwien.ac.at/files/publik_300317.pdf