88 citations · 340 across the 23 of their papers we have counts for
15 papers · 1 filter
Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one…
On CNF Conversion for SAT and SMT Enumeration
Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
Modern SAT and SMT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants…
On Enumerating Short Projected Models
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Propositional model enumeration, or All-SAT, is the task to record all models of a propositional formula. It is a key task in software and hardware verification, system engineering…
Are You Satisfied by This Partial Assignment?
Roberto Sebastiani
Many procedures for SAT and SAT-related problems -- in particular for those requiring the complete enumeration of satisfying truth assignments -- rely their efficiency on the detec…
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…