This is a preliminary report of work in progress on the development of the Eos SMT/SMA-solver. Eos is the first solver built from the start based on the CDSAT (Conflict-Driven SATisfiability) paradigm for solving satisfiability problems modulo theories and assignments. The latter means that assignments to first-order terms may appear in the input. CDSAT generalizes MCSAT (Model-Constructing SATisfiability), hence CDCL (Conflict-Driven Clause Learning), to theory combination. CDSAT reasons in a union of theories by combining in a conflict-driven manner theory inference systems, called theory modules. The current version of Eos has modules for propositional logic, equality with uninterpreted function symbols (UF), and linear real arithmetic. The module for propositional logic is a MiniSAT-inspired SAT solver. A key feature of MCSAT/CDSAT is theory conflict explanation by theory inferences: to this end, the Eos module for UF applies congruence closure inferences, and the Eos module for real arithmetic uses Fourier-Motzkin resolution; both rules may generate new (i.e., non-input) literals. The core solver in Eos implements the CDSAT transition system and several heuristics used in state-of-the-art CDCL-based SAT solvers. Some of these heuristics (e.g., random restarts) can be reused directly in the context of CDSAT, while others are adapted. Eos employs a generalization of the VSIDS heuristics to make decisions on both propositional and first-order terms, and the watched literals scheme for both BCP (Boolean Constraint Propagation) and deductions involving arithmetic terms and uninterpreted terms.

The Eos SMT/SMA-solver: a preliminary report

Maria Paola Bonacina
;
MAZZI, GIULIO
2019

Abstract

This is a preliminary report of work in progress on the development of the Eos SMT/SMA-solver. Eos is the first solver built from the start based on the CDSAT (Conflict-Driven SATisfiability) paradigm for solving satisfiability problems modulo theories and assignments. The latter means that assignments to first-order terms may appear in the input. CDSAT generalizes MCSAT (Model-Constructing SATisfiability), hence CDCL (Conflict-Driven Clause Learning), to theory combination. CDSAT reasons in a union of theories by combining in a conflict-driven manner theory inference systems, called theory modules. The current version of Eos has modules for propositional logic, equality with uninterpreted function symbols (UF), and linear real arithmetic. The module for propositional logic is a MiniSAT-inspired SAT solver. A key feature of MCSAT/CDSAT is theory conflict explanation by theory inferences: to this end, the Eos module for UF applies congruence closure inferences, and the Eos module for real arithmetic uses Fourier-Motzkin resolution; both rules may generate new (i.e., non-input) literals. The core solver in Eos implements the CDSAT transition system and several heuristics used in state-of-the-art CDCL-based SAT solvers. Some of these heuristics (e.g., random restarts) can be reused directly in the context of CDSAT, while others are adapted. Eos employs a generalization of the VSIDS heuristics to make decisions on both propositional and first-order terms, and the watched literals scheme for both BCP (Boolean Constraint Propagation) and deductions involving arithmetic terms and uninterpreted terms.
Satisfiability Modulo Theories, Satisfiability Modulo Assignments, Conflict-Driven Satisfiability, Theory Combination
File in questo prodotto:
File Dimensione Formato  
extAbstract.pdf

accesso aperto

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