NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability

DOI10.1017/S096012952000016XzbMath1492.68064OpenAlexW3097893064MaRDI QIDQ3386749

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

Publication date: 7 January 2021

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s096012952000016x

zbMATH Keywords

refutationread-onceNAE-SAToptimal-length refutation

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• The complexity of read-once resolution
• Finding read-once resolution refutations in systems of 2CNF clauses
• An exponential separation between the parity principle and the pigeonhole principle
• XSAT and NAE-SAT of linear CNF classes
• The Complexity of Propositional Proofs
• The Complexity of Finding Read-Once NAE-Resolution Refutations
• Absorbing random walks and the NAE2SAT problem
• The complexity of satisfiability problems
• Color critical hypergraphs with many edges
• A Machine-Oriented Logic Based on the Resolution Principle