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

DOI10.1007/978-3-319-55911-7_26zbMATH Open1485.68110arXiv1610.04523OpenAlexW2533102354MaRDI QIDQ2988835FDOQ2988835

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)

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.

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

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

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)

Cites Work

• The complexity of facets resolved
• The directed subgraph homeomorphism problem
• Resolution theorem proving
• On the Complexity of Timetable and Multicommodity Flow Problems
• A Machine-Oriented Logic Based on the Resolution Principle
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• On the structure of some classes of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• The Complexity of Propositional Proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of read-once resolution

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)