Proving the infeasibility of Horn formulas through read-once resolution

DOI10.1016/J.DAM.2023.02.001MaRDI QIDQ6558679zbMATH OpenFDO

Authors Piotr Wojciechowski, K. Subramani

Publication date 20 June 2024

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

zbMATH Keywords

NP-completenessHorn clauseAPX-completeness2CNFread-once refutation

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Cites work

• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 1342249 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1179974 (Why is no real title available?)
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 2110413 (Why is no real title available?)
• A Brief Overview of PVS
• A Machine-Oriented Logic Based on the Resolution Principle
• A combinatorial algorithm for Horn programs
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Completeness in approximation classes beyond APX
• Copy complexity of Horn formulas with respect to unit read-once resolution
• Edmonds polytopes and a hierarchy of combinatorial problems. (Reprint)
• Finding read-once resolution refutations in systems of 2CNF clauses
• Handbook of automated reasoning. In 2 vols
• Introduction to algorithms
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
• Lower bounds for cutting planes proofs with small coefficients
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Lower bounds to the size of constant-depth propositional proofs
• On the complexity of cutting-plane proofs
• Outline of an algorithm for integer solutions to linear programs
• Read-once resolutions in Horn formulas
• Redundancy in logic. II: 2CNF and Horn propositional formulae
• The Complexity of Propositional Proofs
• The Complexity of Propositional Proofs
• The complexity of read-once resolution
• The intractability of resolution

This page was built for publication: Proving the infeasibility of Horn formulas through read-once resolution

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