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

DOI10.1016/j.tcs.2018.02.002zbMath1435.03086OpenAlexW2789909559MaRDI QIDQ1749535

Hans Kleine Büning, K. Subramani and Vahan Mkrtchyan, Piotr J. Wojciechowski

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)

Related Items

Analyzing the reachability problem in choice networks ⋮ A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints ⋮ Analyzing read-once cutting plane proofs in Horn systems ⋮ Reachability in choice networks ⋮ Integer feasibility and refutations in UTVPI constraints using bit-scaling ⋮ Copy complexity of Horn formulas with respect to unit read-once resolution ⋮ On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems ⋮ NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability ⋮ 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

Cites Work

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