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.

Four Flavors of Entailment / Möhle, Sibylle; Sebastiani, Roberto; Biere, Armin. - STAMPA. - 12178:(2020), pp. 62-71. (Intervento presentato al convegno 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020 tenutosi a Alghero, Italy nel 3rd-10th July 2020) [10.1007/978-3-030-51825-7_5].

Four Flavors of Entailment

Sebastiani, Roberto;
2020-01-01

Abstract

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.
2020
Theory and Applications of Satisfiability Testing: SAT 2020 23rd International Conference Proceedings
Cham, CH
Springer
978-3-030-51824-0
978-3-030-51825-7
Möhle, Sibylle; Sebastiani, Roberto; Biere, Armin
Four Flavors of Entailment / Möhle, Sibylle; Sebastiani, Roberto; Biere, Armin. - STAMPA. - 12178:(2020), pp. 62-71. (Intervento presentato al convegno 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020 tenutosi a Alghero, Italy nel 3rd-10th July 2020) [10.1007/978-3-030-51825-7_5].
File in questo prodotto:
File Dimensione Formato  
sat20.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 406.16 kB
Formato Adobe PDF
406.16 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/287755
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact