{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:12Z","timestamp":1747173432102,"version":"3.40.5"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2020,10,27]],"date-time":"2020-10-27T00:00:00Z","timestamp":1603756800000},"content-version":"unspecified","delay-in-days":87,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:bold>NP-complete<\/jats:bold>. 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 <jats:bold>false<\/jats:bold>. It is well known that the problem of checking NAE-satisfiability is <jats:bold>NP-complete<\/jats:bold>. 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 <jats:bold>NP-complete<\/jats:bold>.<\/jats:p>","DOI":"10.1017\/s096012952000016x","type":"journal-article","created":{"date-parts":[[2020,10,27]],"date-time":"2020-10-27T09:39:42Z","timestamp":1603791582000},"page":"736-751","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability"],"prefix":"10.1017","volume":"30","author":[{"given":"Hans","family":"Kleine B\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,10,27]]},"reference":[{"key":"S096012952000016X_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"S096012952000016X_ref6","first-page":"66","article-title":"Propositional proof complexity: Past, present, future","volume":"65","author":"Beame","year":"1998","journal-title":"Bulletin of the EATCS"},{"key":"S096012952000016X_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2013.10.030"},{"key":"S096012952000016X_ref26","first-page":"466","volume-title":"Automation of Reasoning. Symbolic Computation (Artificial Intelligence)","author":"Tseitin","year":"1983"},{"key":"S096012952000016X_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58622-4_5"},{"key":"S096012952000016X_ref27","doi-asserted-by":"publisher","DOI":"10.2307\/421131"},{"key":"S096012952000016X_ref3","first-page":"199","volume-title":"IAS\/Park City mathematics series","volume":"10","author":"Beame","year":"2004"},{"volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","year":"1979","author":"Garey","key":"S096012952000016X_ref10"},{"key":"S096012952000016X_ref18","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199233212.001.0001"},{"key":"S096012952000016X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029974"},{"key":"S096012952000016X_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S096012952000016X_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/800133.804350"},{"key":"S096012952000016X_ref24","doi-asserted-by":"publisher","DOI":"10.1080\/00207161003631893"},{"volume-title":"Computational Complexity","year":"1994","author":"Papadimitriou","key":"S096012952000016X_ref19"},{"key":"S096012952000016X_ref1","first-page":"176","volume-title":"Mathematical Foundations of Computer Science (MFCS)","author":"Alekhnovich","year":"1998"},{"key":"S096012952000016X_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_13"},{"key":"S096012952000016X_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54069-5_6"},{"key":"S096012952000016X_ref17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016339119669"},{"key":"S096012952000016X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90002-4"},{"key":"S096012952000016X_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1996.548486"},{"key":"S096012952000016X_ref22","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.20166"},{"volume-title":"Introduction to Algorithms","year":"2009","author":"Cormen","key":"S096012952000016X_ref8"},{"key":"S096012952000016X_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430"},{"key":"S096012952000016X_ref5","unstructured":"Beame, P. and Pitassi, T. (1997). Resolution and the weak pigeonhole principle. In: CSL: 11th Workshop on Computer Science Logic, LNCS, Springer-Verlag."},{"key":"S096012952000016X_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/800119.803893"},{"key":"S096012952000016X_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.02.002"},{"key":"S096012952000016X_ref13","doi-asserted-by":"publisher","DOI":"10.1109\/SCT.1995.514725"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012952000016X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,4]],"date-time":"2020-12-04T11:48:30Z","timestamp":1607082510000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012952000016X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8]]},"references-count":27,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,8]]}},"alternative-id":["S096012952000016X"],"URL":"https:\/\/doi.org\/10.1017\/s096012952000016x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2020,8]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}