Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
From MaRDI portal
Recommendations
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
- Two tractable subclasses of minimal unsatisfiable formulas
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
Cites work
- A perspective on certain polynomial-time solvable classes of satisfiability
- An $n^{5/2} $ Algorithm for Maximum Matchings in Bipartite Graphs
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
- Computing a maximum cardinality matching in a bipartite graph in time \(O(n^{1,5}\sqrt{m/\log \,n})\)
- scientific article; zbMATH DE number 3837387 (Why is no real title available?)
- scientific article; zbMATH DE number 1342212 (Why is no real title available?)
- scientific article; zbMATH DE number 1142309 (Why is no real title available?)
- scientific article; zbMATH DE number 1432797 (Why is no real title available?)
- Investigations on autark assignments
- Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
- Matching theory
- Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
- On subclasses of minimal unsatisfiable formulas
- Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
- The complexity of facets resolved
- Theorem-Proving for Computers: Some Results on Resolution and Renaming
- TWO THEOREMS IN GRAPH THEORY
- Two tractable subclasses of minimal unsatisfiable formulas
Cited in
(38)- 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
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of 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
- Finding read-once resolution refutations in systems of 2CNF clauses
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- 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
- 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.
- Two tractable subclasses of minimal unsatisfiable formulas
- New width parameters for SAT and \#SAT
- 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
- Constraint Satisfaction Problems Parameterized above or below Tight Bounds: A Survey
- On the computational complexity of read once resolution decidability in 2CNF formulas
- Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
- A new bound for 3-satisfiable MaxSat and its algorithmic application
- 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05
- Computing maximal autarkies with few and simple oracle queries
- Community structure inspired algorithms for SAT and \#SAT
- How Many Conflicts Does It Need to Be Unsatisfiable?
- An extension of deficiency and minimal unsatisfiability of quantified Boolean formulas
- Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices
- A new bound for 3-satisfiable MaxSat and its algorithmic application
- Parameterized constraint satisfaction problems: a survey
- Fixed-parameter tractability of satisfying beyond the number of variables
- An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF
- Computational complexity of quantified Boolean formulas with fixed maximal deficiency
- An upper bound for the circuit complexity of existentially quantified Boolean formulas
This page was built for publication: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853541)
