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

DOI10.1007/978-3-540-72788-0_32zbMath1214.68348OpenAlexW1593691693WikidataQ62041314 ScholiaQ62041314MaRDI QIDQ3612475

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)

Related Items (8)

A unified framework for DPLL(T) + certificates ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ 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 ⋮ Algorithms for computing minimal unsatisfiable subsets of constraints ⋮ Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates ⋮ Semantic relevance

Uses Software

• MUP
• AMUSE

This page was built for publication: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories