A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories

DOI10.1007/978-3-540-72788-0_32MaRDI QIDQ3612475zbMATH OpenOpenAlexDBLPWikidataFDO

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Computing small unsatisfiable cores in satisfiability modulo theories
• An approach for extracting a small unsatisfiable core
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Towards a notion of unsatisfiable cores for LTL

Cited in

(17)

• Semantic relevance
• 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

Describes a project that uses

Uses Software

• AMUSE
• MUP

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)