Finding read-once resolution refutations in systems of 2CNF clauses

DOI10.1016/J.TCS.2018.02.002MaRDI QIDQ1749535zbMATH OpenOpenAlexFDO

Authors Hans Kleine Büning, Piotr Wojciechowski, K. Subramani

Publication date 17 May 2018

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2018.02.002

zbMATH Keywords

refutationread-once resolution2CNFvariable read-once resolution

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Recommendations

• On the computational complexity of read once resolution decidability in 2CNF formulas
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
• The complexity of finding read-once NAE-resolution refutations
• scientific article; zbMATH DE number 1765669
• The complexity of read-once resolution

Cites work

• scientific article; zbMATH DE number 5539366 (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?)
• A Machine-Oriented Logic Based on the Resolution Principle
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• On the Complexity of Timetable and Multicommodity Flow Problems
• On the structure of some classes of minimal unsatisfiable formulas
• Optimal length tree-like resolution refutations for 2SAT formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• The Complexity of Propositional Proofs
• The complexity of facets resolved
• The complexity of read-once resolution
• The directed subgraph homeomorphism problem
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• Time bounded random access machines

Cited in

(16)

• Theory and Applications of Satisfiability Testing
• Proving the infeasibility of Horn formulas through read-once resolution
• Reachability in choice networks
• Copy complexity of Horn formulas with respect to unit read-once resolution
• Parameterized and exact-exponential algorithms for the read-once integer refutation problem in UTVPI constraints
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
• Analyzing the reachability problem in choice networks
• Analyzing read-once cutting plane proofs in Horn systems
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Farkas Bounds on Horn Constraint Systems
• On the computational complexity of read once resolution decidability in 2CNF formulas
• The complexity of finding read-once NAE-resolution refutations
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
• On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations

This page was built for publication: Finding read-once resolution refutations in systems of 2CNF clauses

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