3 citations · 5 across the 6 of their papers we have counts for
6 papers
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless +5
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 eff…
From MiniZinc to Optimization Modulo Theories, and Back (Extended Version)
Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
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 Constra…
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers
Patrick Trentin, Roberto Sebastiani
Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmet…
OpenMath and SMT-LIB
James H. Davenport, Matthew England, Roberto Sebastiani +1
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 l…
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Roberto Sebastiani, Patrick Trentin
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 Pseud…
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
Roberto Sebastiani, Patrick Trentin
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 previo…