Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this article, we add lemma learning to CDSAT; we show that theory modules for several theories of practical interest fulfill the requirements for completeness and termination of CDSAT; and we present two ways to enrich CDSAT with proof generation. First, we present a proof-carrying CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, we apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs

Maria Paola Bonacina
;
2022

Abstract

Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this article, we add lemma learning to CDSAT; we show that theory modules for several theories of practical interest fulfill the requirements for completeness and termination of CDSAT; and we present two ways to enrich CDSAT with proof generation. First, we present a proof-carrying CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, we apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.
Lemma learning, Proof generation, Satisfiability modulo theories, Satisfiability modulo assignment
File in questo prodotto:
File Dimensione Formato  
Bonacina2022_Article_Conflict-DrivenSatisfiabilityF.pdf

accesso aperto

Tipologia: Versione dell'editore
Licenza: Creative commons
Dimensione 1.56 MB
Formato Adobe PDF
1.56 MB 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: http://hdl.handle.net/11562/1041622
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact