Many applications depend on solving the satisfiability of formulae involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory (SMT). This article presents a new method for satisfiability modulo a combination of theories, named CDSAT, for Conflict-Driven SATisfiability. CDSAT also solves Satisfiability Modulo Assignment (SMA) problems that may include assignments to first-order terms. A conflict-driven procedure assigns values to variables to build a model, and performs inferences on demand in order to solve conflicts between assignments and formulae. CDSAT extends this paradigm to generic combinations of disjoint theories, each characterized by a collection of inference rules called theory module. CDSAT coordinates the theory modules in such a way that the conflict-driven reasoning happens in the union of the theories, not only in propositional logic. As there is no fixed hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. We prove the soundness, completeness, and termination of CDSAT, identifying sufficient requirements on theories and modules that ensure these properties.

Conflict-driven satisfiability for theory combination: transition system and completeness

Maria Paola Bonacina
;
2020-01-01

Abstract

Many applications depend on solving the satisfiability of formulae involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory (SMT). This article presents a new method for satisfiability modulo a combination of theories, named CDSAT, for Conflict-Driven SATisfiability. CDSAT also solves Satisfiability Modulo Assignment (SMA) problems that may include assignments to first-order terms. A conflict-driven procedure assigns values to variables to build a model, and performs inferences on demand in order to solve conflicts between assignments and formulae. CDSAT extends this paradigm to generic combinations of disjoint theories, each characterized by a collection of inference rules called theory module. CDSAT coordinates the theory modules in such a way that the conflict-driven reasoning happens in the union of the theories, not only in propositional logic. As there is no fixed hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. We prove the soundness, completeness, and termination of CDSAT, identifying sufficient requirements on theories and modules that ensure these properties.
2020
Theory combination, Conflict-driven decision procedures, Model building, Satisfiability modulo assignment
File in questo prodotto:
File Dimensione Formato  
JAR2020CDSATtransition.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 616.04 kB
Formato Adobe PDF
616.04 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/11562/988820
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 8
social impact