On the computational complexity of read once resolution decidability in 2CNF formulas

DOI10.1007/978-3-319-55911-7_26MaRDI QIDQ2988835zbMATH OpenOpenAlexFDO

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

Publication date 19 May 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.04523

zbMATH Keywords

resolution2SATread-once

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Computational aspects of satisfiability (68R07)

Abstract: In this paper, we analyze 2CNF formulas from the perspectives of Read-Once resolution (ROR) refutation schemes. We focus on two types of ROR refutations, viz., variable-once refutation and clause-once refutation. In the former, each variable may be used at most once in the derivation of a refutation, while in the latter, each clause may be used at most once. We show that the problem of checking whether a given 2CNF formula has an ROR refutation under both schemes is NP-complete. This is surprising in light of the fact that there exist polynomial refutation schemes (tree-resolution and DAG-resolution) for 2CNF formulas. On the positive side, we show that 2CNF formulas have copy-complexity 2, which means that any unsatisfiable 2CNF formula has a refutation in which any clause needs to be used at most twice.

Recommendations

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

Cites work

• 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
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Resolution theorem proving
• The Complexity of Propositional Proofs
• The complexity of facets resolved
• The complexity of read-once resolution
• The directed subgraph homeomorphism problem

Cited in

(5)

• The complexity of read-once resolution
• Copy complexity of Horn formulas with respect to unit read-once resolution
• Finding read-once resolution refutations in systems of 2CNF clauses
• The complexity of finding read-once NAE-resolution refutations
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas

This page was built for publication: On the computational complexity of read once resolution decidability in 2CNF formulas

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