Homomorphisms of conjunctive normal forms.

DOI10.1016/S0166-218X(02)00411-0zbMath1033.68095MaRDI QIDQ1408387

Stefan Szeider

Publication date: 15 September 2003

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

zbMATH Keywords

unsatisfiable formulasunsatisfiability\(p\)-simulation

Mathematics Subject Classification ID

Computability and recursion theory (03D99)

Related Items

Disproof of the neighborhood conjecture with implications to SAT ⋮ Unnamed Item ⋮ Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable ⋮ The complexity of homomorphisms and renamings for minimal unsatisfiable formulas ⋮ The Lovász Local Lemma and Satisfiability ⋮ Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. ⋮ Formula simplification via invariance detection by algebraically indexed types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Short proofs for tricky formulas
• The intractability of resolution
• Solving satisfiability in less than \(2^ n\) steps
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• The complexity of facets resolved
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Tractability through symmetries in propositional calculus
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• 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
• The symmetry rule in propositional logic
• The relative efficiency of propositional proof systems
• The Complexity of Propositional Proofs
• Theorem-Proving for Computers: Some Results on Resolution and Renaming