On Improving MUS Extraction Algorithms

DOI10.1007/978-3-642-21581-0_14zbMath1330.68273OpenAlexW1769298637MaRDI QIDQ3007681

Inês Lynce, João P. Marques-Silva

Publication date: 17 June 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-21581-0_14

Mathematics Subject Classification ID

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

Related Items

Speeding up MUS Extraction with Preprocessing and Chunking ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Towards backbone computing: A Greedy-Whitening based approach ⋮ Minimally Unsatisfiable Boolean Circuits ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ SAT-based rigorous explanations for decision lists ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT

Uses Software

• PicoSAT
• Sat4j
• MUP
• AMUSE
• QUICKXPLAIN

Cites Work

• Unnamed Item
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Using local search to find MSSes and MUSes
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• On exact selection of minimally unsatisfiable subformulae
• Local-search extraction of mUSes
• Redundancy in logic. I: CNF propositional formulae
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Searching for Autarkies to Trim Unsatisfiable Clause Sets
• Finding Guaranteed MUSes Fast
• Generalizing Core-Guided Max-SAT
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction