Recent and Ongoing Developments of Model-Constructing Satisfiability Stephane Graham-Lengrand SRI International

摘要

Model-constructing satisfiability is an approach to SMT-solving developed by Jova-novic et al., generalising work on satisfiability in non-linear arithmetic [9], The approach lifts the principles of Conflict-Driven Clause Learning (CDCL) from classical propositional reasoning to theory reasoning. It is incarnated by the MCSAT calculus [4, 8] and is implemented in the Yices SMT-solver [5].