Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-24T15:01:42.573Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  27 October 2020

Hans Kleine Büning ,
P. Wojciechowski  and
K. Subramani Open the ORCID record for K. Subramani [Opens in a new window]
Hans Kleine Büning
Affiliation:
Universität Paderborn, Paderborn, Germany
P. Wojciechowski
Affiliation:
West Virginia University, Morgantown, WV26506, USA
K. Subramani*
Affiliation:
West Virginia University, Morgantown, WV26506, USA
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

Keywords

Read-onceNAE-SATrefutationoptimal length refutation
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 7 , August 2020 , pp. 736 - 751
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alekhnovich, M., Buss, S., Moran, S. and Pitassi, T. (1998). Minimum propositional proof length is NP-hard to linearly approximate. In: Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, Springer-Verlag, 176–184.Google Scholar
Aspvall, B., Plass, M. F. and Tarjan, R. (1979). A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters 8 (3) 121–123.CrossRefGoogle Scholar
Beame, P. (2004). Proof complexity. In: Rudich, S. and Wigderson, A. (eds.) Computational Complexity Theory , IAS/Park City mathematics series, vol. 10, American Mathematical Society, 199–246.Google Scholar
Beame, P. and Pitassi, T. (1996). Simplified and improved resolution lower bounds. In: 37th Annual Symposium on Foundations of Computer Science, Burlington, Vermont, 14–16 October 1996, IEEE, 274–282.CrossRefGoogle Scholar
Beame, P. and Pitassi, T. (1997). Resolution and the weak pigeonhole principle. In: CSL: 11th Workshop on Computer Science Logic, LNCS, Springer-Verlag.Google Scholar
Beame, P. and Pitassi, T. (1998). Propositional proof complexity: Past, present, future. Bulletin of the EATCS 65 66–89.Google Scholar
Buss, S. R. (1999). Propositional Proof Complexity: An Introduction. In: Berger, U. and Schwichtenberg, H. (eds.) Computational Logic, Berlin, Springer-Verlag, 127–178.CrossRefGoogle Scholar
Cormen, T. H., Leiserson, C. E., Rivest, R. L. and Stein, C. (2009). Introduction to Algorithms, 3rd edn., Cambridge, MA, The MIT Press.Google Scholar
Cook, S. A. and Reckhow, R. A. (1974). On the lengths of proofs in the propositional calculus (preliminary version). In: Proceedings of the 6th Annual ACM Symposium on Theory of Computing, 30 April–2 May, 1974, Seattle, Washington, USA, 135–148.CrossRefGoogle Scholar
Garey, M. R. and Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness, San Francisco, W. H. Freeman Company.Google Scholar
Haken, A. (1985). The intractability of resolution. Theoretical Computer Science 39 (2–3) 297–308.CrossRefGoogle Scholar
Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning, 1st edn., Cambridge University Press.CrossRefGoogle Scholar
Iwama, K. and Miyano, E. (1995). Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC’95), Los Alamitos, CA, USA, June 1995, IEEE Computer Society Press, 29–36.CrossRefGoogle Scholar
Iwama, K. (1997). Complexity of finding short resolution proofs. Lecture Notes in Computer Science 1295 309–319.CrossRefGoogle Scholar
Kleine Büning, H., Wojciechowski, P. J. and Subramani, K. (2017). The complexity of finding read-once nae-resolution refutations. In: Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, 5–7 January, 2017, Proceedings, 64–76.CrossRefGoogle Scholar
Kleine Büning, H., Wojciechowski, P. J. and Subramani, K. (2018). Finding read-once resolution refutations in systems of 2CNF clauses. Theoretical Computer Science 729 42–56.CrossRefGoogle Scholar
Kleine Büning, H. and Zhao, X. (2002). The complexity of read-once resolution. Annals of Mathematics and Artificial Intelligence 36 (4) 419–435.CrossRefGoogle Scholar
Moore, C. and Mertens, S. (2011). The Nature of Computation, 1st edn., Oxford University Press.CrossRefGoogle Scholar
Papadimitriou, C. H. (1994). Computational Complexity, New York, Addison-Wesley.Google Scholar
Porschen, S., Schmidt, T., Speckenmeyer, E. and Wotzlaw, A. (2014). XSAT and NAE-SAT of linear CNF classes. Discrete Applied Mathematics 167 1–14.CrossRefGoogle Scholar
Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM 12 (1) 23–41.CrossRefGoogle Scholar
Rödl, V. and Siggers, M. H. (2006). Color critical hypergraphs with many edges. Journal of Graph Theory 53 (1) 56–74.CrossRefGoogle Scholar
Schaefer, T. J. (1978). The complexity of satisfiability problems. In: Aho, A. (eds.) Proceedings of the 10th Annual ACM Symposium on Theory of Computing, New York City, NY, ACM Press, 216–226.CrossRefGoogle Scholar
Subramani, K. and Gu, X. (2011). Absorbing random walks and the NAE2SAT problem. International Journal of Computer Mathematics 88 (3) 452–467.CrossRefGoogle Scholar
Szeider, S. (2001). NP-completeness of refutability by literal-once resolution. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, 18–23 June, 2001, Proceedings, 168–181.CrossRefGoogle Scholar
Tseitin, G.S. (1983). On the Complexity of Derivation in Propositional Calculus. In: Siekmann J.H., Wrightson G. (eds.) Automation of Reasoning. Symbolic Computation (Artificial Intelligence), Berlin, Heidelberg, Springer, 466–483.Google Scholar
Urquhart, A. (1995). The complexity of propositional proofs. The Bulletin of Symbolic Logic 1 (4) 425–467.CrossRefGoogle Scholar