Approximating minimal unsatisfiable subformulae by means of adaptive core search
From MaRDI portal
Publication:1408373
DOI10.1016/S0166-218X(02)00399-2zbMath1029.68075MaRDI QIDQ1408373
Publication date: 15 September 2003
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
68Q25: Analysis of algorithms and problem complexity
Related Items
Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases, Resolution proof transformation for compression and interpolation, An approach for extracting a small unsatisfiable core, Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, Using local search to find MSSes and MUSes, On exact selection of minimally unsatisfiable subformulae, Local-search extraction of mUSes, Redundancy in logic. II: 2CNF and Horn propositional formulae, Redundancy in logic. III: Non-monotonic reasoning, Redundancy in logic. I: CNF propositional formulae, MUST: Provide a Finer-Grained Explanation of Unsatisfiability
Uses Software
Cites Work
- Solving satisfiability in less than \(2^ n\) steps
- Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
- Solving propositional satisfiability problems
- Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
- Branching rules for satisfiability
- Implementing the Davis-Putnam method
- Graph-Based Algorithms for Boolean Function Manipulation
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- GRASP: a search algorithm for propositional satisfiability
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
