Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas

DOI10.1007/s10472-021-09762-2zbMath1485.90119OpenAlexW3175751884WikidataQ113904581 ScholiaQ113904581MaRDI QIDQ2075363

Piotr J. Wojciechowski, K. Subramani and Vahan Mkrtchyan

Publication date: 14 February 2022

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-021-09762-2

zbMATH Keywords

NP-hardexact exponential algorithmsread-once resolution2CNF

Mathematics Subject Classification ID

Combinatorial optimization (90C27) Boolean programming (90C09)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exact exponential algorithms.
• On finding short resolution refutations and small unsatisfiable subsets
• The intractability of resolution
• On the complexity of approximating the independent set problem
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• What is answer set programming to propositional satisfiability
• Finding read-once resolution refutations in systems of 2CNF clauses
• Restricted cutting plane proofs in Horn constraint systems
• Read-once resolutions in Horn formulas
• The Uniform Minimum-Ones 2SAT Problem and its Application to Haplotype Classification
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Renaming a Set of Clauses as a Horn Set
• Kernelization
• Answer Set Programming
• Minimum Witnesses for Unsatisfiable 2CNFs

This page was built for publication: Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas