Sibylle Möhle, Roberto Sebastiani, Armin Biere,
"Four Flavors of Entailment"
, in Pulina L., Seidl M.: The 23rd International Conference on Theory and Applications of Satisfiability Testing, Serie Lecture Notes in Computer Science (LNCS), Vol. 12178, Springer, Cham, 2020, ISBN: 978-3-030-51824-0
Original Titel:
Four Flavors of Entailment
Sprache des Titels:
Englisch
Original Buchtitel:
The 23rd International Conference on Theory and Applications of Satisfiability Testing
Original Kurzfassung:
We present a novel approach for enumerating partial models
of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples.
We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.
Forschungs-