Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

DOI10.1007/s10878-008-9142-4zbMath1173.90510OpenAlexW2081776044MaRDI QIDQ1037449

Sandrine Paroz, Christian Desrosiers, Philippe Galinier, Alain Hertz

Publication date: 16 November 2009

Published in: Journal of Combinatorial Optimization (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10878-008-9142-4

zbMATH Keywords

heuristicssatisfiabilityminimal unsatisfiable subformulas (MUS)

Mathematics Subject Classification ID

Approximation methods and heuristics in mathematical programming (90C59) Combinatorial optimization (90C27)

Related Items

A New Approach to Partial MUS Enumeration ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Minimally Unsatisfiable Boolean Circuits ⋮ On Improving MUS Extraction Algorithms ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores

Uses Software

• SATO
• Chaff
• BerkMin
• Tabu search
• MUP
• AMUSE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithms for the maximum satisfiability problem
• Solution techniques for the large set covering problem
• Boosting complete techniques thanks to local search methods
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search.
• Guided local search for solving SAT and weighted MAX-SAT problems
• Efficient algorithms for finding critical subgraphs
• BerkMin: A fast and robust SAT-solver
• Identifying Minimally Infeasible Subsystems of Inequalities
• Finding a Useful Subset of Constraints for Analysis in an Infeasible Linear Program
• Relational concept learning by cooperative evolution
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems