Investigations on autark assignments

DOI10.1016/S0166-218X(00)00262-6zbMath0965.03018MaRDI QIDQ1841885

Oliver Kullmann

Publication date: 26 July 2001

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

linear programmingpropositional logicresolutionsatisfiabilitypolynomial timedeficiencyconjunctive normal formautark assignment\(q\)-Horn formulaslinear autarkymatched formulasminimally unsatisfiable clause-sets

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05)

Related Items (24)

Counting minimal unsatisfiable subsets ⋮ Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ A Decision-Making Procedure for Resolution-Based SAT-Solvers ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Homomorphisms of conjunctive normal forms. ⋮ Bounds on the size of PC and URC formulas ⋮ An overview of parallel SAT solving ⋮ Autark assignments of Horn CNFs ⋮ Finding the Hardest Formulas for Resolution ⋮ An Automata View to Goal-Directed Methods ⋮ Resolution cannot polynomially simulate compressed-BFS ⋮ Generalizations of matched CNF formulas ⋮ Does This Set of Clauses Overlap with at Least One MUS? ⋮ Generalized completeness for SOS resolution and its application to a new notion of relevance ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ Present and Future of Practical SAT Solving ⋮ Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. ⋮ The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas ⋮ A short note on some tractable cases of the satisfiability problem. ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ Semantic relevance ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ On functional dependencies in \(q\)-Horn theories

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving satisfiability in less than \(2^ n\) steps
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Matching theory
• Linear programming duality: an introduction to oriented matroids
• Tautologies and positive solvability of linear homogeneous systems
• 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
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Recognizing renamable generalized propositional Horn formulas is NP- complete
• Autarky pruning in propositional model elimination reduces failure redundancy
• Solving satisfiability problems using elliptic approximations -- effective branching rules
• 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
• Parallel cooperative propositional theorem proving
• On theories with a combinatorial definition of 'equivalence'
• The relative efficiency of propositional proof systems
• A Complexity Index for Satisfiability Problems
• The complexity of satisfiability problems

This page was built for publication: Investigations on autark assignments