A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
From MaRDI portal
Publication:3612475
DOI10.1007/978-3-540-72788-0_32zbMATH Open1214.68348DBLPconf/sat/CimattiGS07OpenAlexW1593691693WikidataQ62041314 ScholiaQ62041314MaRDI QIDQ3612475FDOQ3612475
Authors: Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani 
Publication date: 10 March 2009
Published in: Theory and Applications of Satisfiability Testing – SAT 2007 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-72788-0_32
Recommendations
Cited In (17)
- A framework for certified Boolean branch-and-bound optimization
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Resolution proof transformation for compression and interpolation
- Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
- Mining propositional simplification proofs for small validating clauses
- Practical algorithms for unsatisfiability proof and core generation in SAT solvers
- Computing small unsatisfiable cores in satisfiability modulo theories
- A unified framework for DPLL(T) + certificates
- Algorithms for computing minimal unsatisfiable subsets of constraints
- An approach for extracting a small unsatisfiable core
- Debugging design errors by using unsatisfiable cores
- CoReS: a tool for computing core graphs via SAT/SMT solvers
- CoReS: a tool for computing core graphs via SAT/SMT solvers
- Efficient Generation of Unsatisfiability Proofs and Cores in SAT
- Accelerating parameter synthesis using semi-algebraic constraints
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- Semantic relevance
Uses Software
This page was built for publication: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612475)
