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

2CNFread-once resolutionrefutationvariable read-once resolution

Mathematics Subject Classification ID

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

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

• A Machine-Oriented Logic Based on the Resolution Principle
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• 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?)
• 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 facets resolved
• The Complexity of Propositional Proofs
• 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

(18)

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

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)