Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
From MaRDI portal
Publication:1408381
DOI10.1016/S0166-218X(02)00406-7zbMath1029.68079OpenAlexW2042705674MaRDI QIDQ1408381
Publication date: 15 September 2003
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0166-218x(02)00406-7
Linear programmingResolutionPolynomial timeDeficiencyAutarkyConjunctive normal formLean clause-setLinear autarkyMatching theoryPropositional satisfiability problemQualitative matrix analysis
Related Items
Computing Maximal Autarkies with Few and Simple Oracle Queries, Community Structure Inspired Algorithms for SAT and #SAT, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, A new bound for 3-satisfiable MaxSat and its algorithmic application, Homomorphisms of conjunctive normal forms., Redundancy in logic. I: CNF propositional formulae, On Variables with Few Occurrences in Conjunctive Normal Forms, On Improving MUS Extraction Algorithms, Autark assignments of Horn CNFs, New width parameters for SAT and \#SAT, On semidefinite least squares and minimal unsatisfiability, Computational complexity of quantified Boolean formulas with fixed maximal deficiency, Fixed-parameter tractability of satisfying beyond the number of variables, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Generalizations of matched CNF formulas, A New Bound for 3-Satisfiable Maxsat and Its Algorithmic Application, Investigations on autark assignments, Present and Future of Practical SAT Solving, 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05, Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
Uses Software
Cites Work
- 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
- On generalized Horn formulas and \(k\)-resolution
- Signsolvability revisited
- Solving satisfiability in less than \(2^ n\) steps
- Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
- Matching theory
- The complexity of facets resolved
- Polynomially solvable satisfiability problems
- Linear programming duality: an introduction to oriented matroids
- Tautologies and positive solvability of linear homogeneous systems
- A hierarchy of tractable satisfiability problems
- An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
- Recognition of \(q\)-Horn formulae in linear time
- Polynomial-time inference of all valid implications for Horn and related formulae
- A polynomial-time algorithm for reducing the number of variables in MAX SAT problem
- New worst-case upper bounds for SAT
- The complexity of read-once resolution
- Autarky pruning in propositional model elimination reduces failure redundancy
- On subclasses of minimal unsatisfiable formulas
- Investigations on autark assignments
- Solving satisfiability problems using elliptic approximations -- effective branching rules
- Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
- A short note on some tractable cases of the satisfiability problem.
- A perspective on certain polynomial-time solvable classes of satisfiability
- New methods for 3-SAT decision and worst-case analysis
- On a generalization of extended resolution
- Two tractable subclasses of minimal unsatisfiable formulas
- Parallel cooperative propositional theorem proving
- On theories with a combinatorial definition of 'equivalence'
- Sign-consistency and solvability of constrained linear systems
- A Complexity Index for Satisfiability Problems
