Factoring Out Assumptions to Speed Up MUS Extraction

DOI10.1007/978-3-642-39071-5_21zbMath1390.68601OpenAlexW2167400570MaRDI QIDQ5326470

Armin Biere, Jean-Marie Lagniez

Publication date: 5 August 2013

Published in: Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39071-5_21

Mathematics Subject Classification ID

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

Related Items (9)

Memory-limited model-based diagnosis ⋮ Speeding up MUS Extraction with Preprocessing and Chunking ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ SAT-Based Horn Least Upper Bounds ⋮ Conformant planning as a case study of incremental QBF solving ⋮ On getting rid of the preprocessing minimization step in MUC-finding algorithms ⋮ Definability for model counting ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT

Uses Software

• AMUSE
• RSat

This page was built for publication: Factoring Out Assumptions to Speed Up MUS Extraction