Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
From MaRDI portal
Publication:1853541
DOI10.1016/S0304-3975(01)00337-1zbMath1061.68072WikidataQ60060025 ScholiaQ60060025MaRDI QIDQ1853541
Herbert Fleischner, Stefan Szeider, Oliver Kullmann
Publication date: 21 January 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)
Related Items (35)
Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Community Structure Inspired Algorithms for SAT and #SAT ⋮ Constraint Satisfaction Problems Parameterized above or below Tight Bounds: A Survey ⋮ Local-search extraction of mUSes ⋮ Redundancy in logic. II: 2CNF and Horn propositional formulae ⋮ Redundancy in logic. III: Non-monotonic reasoning ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ A new bound for 3-satisfiable MaxSat and its algorithmic application ⋮ Unnamed Item ⋮ How Many Conflicts Does It Need to Be Unsatisfiable? ⋮ An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF ⋮ Approximating minimal unsatisfiable subformulae by means of adaptive core search ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Homomorphisms of conjunctive normal forms. ⋮ On the parameterized complexity of \((k,s)\)-SAT ⋮ On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas ⋮ Redundancy in logic. I: CNF propositional formulae ⋮ New width parameters for SAT and \#SAT ⋮ Finding read-once resolution refutations in systems of 2CNF clauses ⋮ Computational complexity of quantified Boolean formulas with fixed maximal deficiency ⋮ Fixed-parameter tractability of satisfying beyond the number of variables ⋮ A new lower bound on the maximum number of satisfied clauses in Max-SAT and its algorithmic applications ⋮ Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable ⋮ An upper bound for the circuit complexity of existentially quantified Boolean formulas ⋮ On exact selection of minimally unsatisfiable subformulae ⋮ The complexity of homomorphisms and renamings for minimal unsatisfiable formulas ⋮ Generalizations of matched CNF formulas ⋮ Extension and equivalence problems for clause minimal formulae ⋮ A New Bound for 3-Satisfiable Maxsat and Its Algorithmic Application ⋮ Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems ⋮ A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas ⋮ Using local search to find MSSes and MUSes ⋮ 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05 ⋮ 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.
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computing a maximum cardinality matching in a bipartite graph in time \(O(n^{1,5}\sqrt{m/\log \,n})\)
- Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
- Matching theory
- The complexity of facets resolved
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
- Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
- On subclasses of minimal unsatisfiable formulas
- Investigations on autark assignments
- Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
- A perspective on certain polynomial-time solvable classes of satisfiability
- Two tractable subclasses of minimal unsatisfiable formulas
- TWO THEOREMS IN GRAPH THEORY
- Theorem-Proving for Computers: Some Results on Resolution and Renaming
- An $n^{5/2} $ Algorithm for Maximum Matchings in Bipartite Graphs
This page was built for publication: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
