-
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Authors:
Nick Feng,
Alan J. Hu,
Sam Bayless,
Syed M. Iqbal,
Patrick Trentin,
Mike Whalen,
Lee Pike,
John Backes
Abstract:
Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to efficiently generate proofs of unsatisfiability specifically for an important subset of SMT: SAT Modulo Monotonic Theories (SMMT), which includes many useful finite-domain theories (e.g., bit vectors and many graph-theoreti…
▽ More
Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to efficiently generate proofs of unsatisfiability specifically for an important subset of SMT: SAT Modulo Monotonic Theories (SMMT), which includes many useful finite-domain theories (e.g., bit vectors and many graph-theoretic properties) and is used in production at Amazon Web Services. Our method uses propositional definitions of the theory predicates, from which it generates compact Horn approximations of the definitions, which lead to efficient DRAT proofs, leveraging the large investment the SAT community has made in DRAT. In experiments on practical SMMT problems, our proof generation overhead is minimal (7.41% geometric mean slowdown, 28.8% worst-case), and we can generate and check proofs for many problems that were previously intractable.
△ Less
Submitted 18 April, 2024; v1 submitted 19 January, 2024;
originally announced January 2024.
-
From MiniZinc to Optimization Modulo Theories, and Back (Extended Version)
Authors:
Francesco Contaldo,
Patrick Trentin,
Roberto Sebastiani
Abstract:
Optimization Modulo Theories (OMT) is an extension of SMT that allows for finding models that optimize objective functions. In this paper we aim at bridging the gap between Constraint Programming (CP) and OMT, in both directions. First, we have extended the OMT solver OptiMathSAT with a FlatZinc interface -- which can also be used as a FlatZinc-to-OMT encoder for other OMT solvers. This allows OMT…
▽ More
Optimization Modulo Theories (OMT) is an extension of SMT that allows for finding models that optimize objective functions. In this paper we aim at bridging the gap between Constraint Programming (CP) and OMT, in both directions. First, we have extended the OMT solver OptiMathSAT with a FlatZinc interface -- which can also be used as a FlatZinc-to-OMT encoder for other OMT solvers. This allows OMT tools to be used in combination with mzn2fzn on the large amount of CP problems coming from the MiniZinc community. Second, we have introduced a tool for translating SMT and OMT problems on the linear arithmetic and bit-vector theories into MiniZinc. This allows MiniZinc solvers to be used on a large amount of SMT/OMT problems.
We have discussed the main issues we had to cope with in either directions. We have performed an extensive empirical evaluation comparing three state-of-the-art OMT-based tools with many state-of-the-art CP tools on (i) CP problems coming from the MiniZinc challenge, and (ii) OMT problems coming mostly from formal verification. This analysis also allowed us to identify some criticalities, in terms of efficiency and correctness, one has to cope with when addressing CP problems with OMT tools, and vice versa.
△ Less
Submitted 17 February, 2020; v1 submitted 3 December, 2019;
originally announced December 2019.
-
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
Authors:
Patrick Trentin,
Roberto Sebastiani
Abstract:
Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of B…
▽ More
Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of Bit-Vectors (BV) for the integers and that of Floating-Point Numbers (FP) for the reals respectively. Whereas an approach for OMT with (unsigned) BV has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with FP. In this paper we fill this gap. We present a novel OMT approach, based on the novel concept of attractor and dynamic attractor, which extends the work of Nadel & Ryvchin to signed BV and, most importantly, to FP. We have implemented some OMT(BV) and OMT(FP) procedures on top of OptiMathSAT and tested the latter ones on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of the novel approach.
△ Less
Submitted 7 May, 2019;
originally announced May 2019.
-
OpenMath and SMT-LIB
Authors:
James H. Davenport,
Matthew England,
Roberto Sebastiani,
Patrick Trentin
Abstract:
OpenMath and SMT-LIB are languages with very different origins, but both "represent mathematics". We describe SMT-LIB for the OpenMath community and consider adaptations for both languages to support the growing SC-Square initiative.
OpenMath and SMT-LIB are languages with very different origins, but both "represent mathematics". We describe SMT-LIB for the OpenMath community and consider adaptations for both languages to support the growing SC-Square initiative.
△ Less
Submitted 5 March, 2018;
originally announced March 2018.
-
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Authors:
Roberto Sebastiani,
Patrick Trentin
Abstract:
Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. (Partial weighted) MaxSMT --or equivalently OMT with Pseudo-Boolean objective functions, OMT+PB-- is a very-relevant strict subcase of OMT. We classify existing approaches for MaxSMT or OMT+PB in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MAX…
▽ More
Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. (Partial weighted) MaxSMT --or equivalently OMT with Pseudo-Boolean objective functions, OMT+PB-- is a very-relevant strict subcase of OMT. We classify existing approaches for MaxSMT or OMT+PB in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MAXSAT solvers, but they are specific-purpose and not always applicable; OMT-based approaches are general-purpose, but they suffer from intrinsic inefficiencies on MaxSMT/OMT+PB problems.
We identify a major source of such inefficiencies, and we address it by enhancing OMT by means of bidirectional sorting networks. We implemented this idea on top of the OptiMathSAT OMT solver. We run an extensive empirical evaluation on a variety of problems, comparing MaxSAT-based and OMT-based techniques, with and without sorting networks, implemented on top of OptiMathSAT and νZ. The results support the effectiveness of this idea, and provide interesting insights about the different approaches.
△ Less
Submitted 8 February, 2017;
originally announced February 2017.
-
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
Authors:
Roberto Sebastiani,
Patrick Trentin
Abstract:
In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding mode…
▽ More
In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding models that are optimal wrt. some cost functions. In previous work, namely "Optimization Modulo Theory with Linear Rational Cost Functions -- OMT(LAR U T )", we have leveraged SMT solving to handle the minimization of cost functions on linear arithmetic over the rationals, by means of a combination of SMT and LP minimization techniques. In this paper we push the envelope of our OMT approach along three directions: first, we extend it to work also with linear arithmetic on the mixed integer/rational domain, by means of a combination of SMT, LP and ILP minimization techniques; second, we develop a multi-objective version of OMT, so that to handle many cost functions simultaneously; third, we develop an incremental version of OMT, so that to exploit the incrementality of some OMT-encodable problems. An empirical evaluation performed on OMT-encoded verification problems demonstrates the usefulness and efficiency of these extensions.
△ Less
Submitted 16 January, 2015; v1 submitted 21 October, 2014;
originally announced October 2014.
