Homomorphisms of conjunctive normal forms.

DOI10.1016/S0166-218X(02)00411-0MaRDI QIDQ1408387zbMATH OpenFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 2165693
• Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
• The complexity of homomorphisms and renamings for minimal unsatisfiable formulas
• The complexity of resolution with generalized symmetry rules
• scientific article; zbMATH DE number 1962837

Cites work

• scientific article; zbMATH DE number 1612537 (Why is no real title available?)
• scientific article; zbMATH DE number 1342212 (Why is no real title available?)
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• A perspective on certain polynomial-time solvable classes of satisfiability
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Investigations on autark assignments
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Short proofs for tricky formulas
• Solving satisfiability in less than \(2^ n\) steps
• The Complexity of Propositional Proofs
• The complexity of facets resolved
• The intractability of resolution
• The relative efficiency of propositional proof systems
• The symmetry rule in propositional logic
• Theorem-Proving for Computers: Some Results on Resolution and Renaming
• Tractability through symmetries in propositional calculus

Cited in

(8)

• Disproof of the neighborhood conjecture with implications to SAT
• Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
• The complexity of homomorphisms and renamings for minimal unsatisfiable formulas
• scientific article; zbMATH DE number 2165693 (Why is no real title available?)
• Formula simplification via invariance detection by algebraically indexed types
• Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable
• The Lovász Local Lemma and Satisfiability
• scientific article; zbMATH DE number 7350778 (Why is no real title available?)

This page was built for publication: Homomorphisms of conjunctive normal forms.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1408387)