{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:36Z","timestamp":1747173456426,"version":"3.40.5"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T00:00:00Z","timestamp":1694390400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we analyze two types of refutations for Unit Two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint is a linear inequality of the form: <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline1.png\"\/><jats:tex-math>\n$a_{i}\\cdot x_{i}+a_{j} \\cdot x_{j} \\le b_{k}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, where <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline2.png\"\/><jats:tex-math>\n$a_{i},a_{j}\\in \\{0,1,-1\\}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline3.png\"\/><jats:tex-math>\n$b_{k} \\in \\mathbb{Z}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. A conjunction of such constraints is called a UTVPI constraint system (UCS) and can be represented in matrix form as: <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline4.png\"\/><jats:tex-math>\n${\\bf A \\cdot x \\le b}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. UTVPI constraints are used in many domains including operations research and program verification. We focus on two variants of read-once refutation (ROR). An ROR is a refutation in which each constraint is used at most once. A literal-once refutation (LOR), a more restrictive form of ROR, is a refutation in which each literal (<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline5.png\"\/><jats:tex-math>\n$x_i$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> or <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000300_inline6.png\"\/><jats:tex-math>\n$-x_i$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) is used at most once. First, we examine the constraint-required read-once refutation (CROR) problem and the constraint-required literal-once refutation (CLOR) problem. In both of these problems, we are given a set of constraints that must be used in the refutation. RORs and LORs are incomplete since not every system of linear constraints is guaranteed to have such a refutation. This is still true even when we restrict ourselves to UCSs. In this paper, we provide <jats:bold>NC<\/jats:bold> reductions between the CROR and CLOR problems in UCSs and the minimum weight perfect matching problem. The reductions used in this paper assume a CREW PRAM model of parallel computation. As a result, the reductions establish that, from the perspective of parallel algorithms, the CROR and CLOR problems in UCSs are equivalent to matching. In particular, if an <jats:bold>NC<\/jats:bold> algorithm exists for either of these problems, then there is an <jats:bold>NC<\/jats:bold> algorithm for matching.<\/jats:p>","DOI":"10.1017\/s0960129523000300","type":"journal-article","created":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T09:05:55Z","timestamp":1694423155000},"page":"227-243","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Constrained read-once refutations in UTVPI constraint systems: A parallel perspective"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,9,11]]},"reference":[{"key":"S0960129523000300_ref15","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251876"},{"key":"S0960129523000300_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/321941.321942"},{"key":"S0960129523000300_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S0960129523000300_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.02.002"},{"key":"S0960129523000300_ref3","unstructured":"Anari, N. and Vazirani, V. V. (2020). Matching is as easy as the decision problem, in the NC model. In: 11th Innovations in Theoretical Computer Science Conference, ITCS 2020, January 12\u201314, 2020, Seattle, Washington, USA, LIPIcs, vol. 151, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 54:1\u201354:25."},{"key":"S0960129523000300_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3155301"},{"key":"S0960129523000300_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_13"},{"volume-title":"Computational Complexity","year":"1994","author":"Papadimitriou","key":"S0960129523000300_ref26"},{"key":"S0960129523000300_ref14","unstructured":"Harvey, W. and Stuckey, P. J. (1997). A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian Computer Science Conference, 102\u2013111."},{"key":"S0960129523000300_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-017-0176-3"},{"volume-title":"Algorithms of Informatics","year":"2013","author":"Khan","key":"S0960129523000300_ref18"},{"volume-title":"Combinatorial Optimization","year":"1998","author":"Cook","key":"S0960129523000300_ref5"},{"key":"S0960129523000300_ref21","volume-title":"Combinatorial Optimization","volume":"21","author":"Korte","year":"2010"},{"key":"S0960129523000300_ref2","doi-asserted-by":"crossref","unstructured":"Anari, N. and Vazirani, V. V. (2017). Planar graph perfect matching is in NC. In: 2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS), 650\u2013661.","DOI":"10.1109\/FOCS.2018.00068"},{"key":"S0960129523000300_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"S0960129523000300_ref10","first-page":"1","article-title":"\u00dcber die Theorie der Einfachen Ungleichungen","volume":"124","author":"Farkas","year":"1902","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"S0960129523000300_ref17","doi-asserted-by":"publisher","DOI":"10.1109\/SCT.1995.514725"},{"volume-title":"Introduction to Parallel Algorithms and Architectures","year":"1992","author":"Leighton","key":"S0960129523000300_ref23"},{"volume-title":"Introduction to Algorithms","year":"2001","author":"Cormen","key":"S0960129523000300_ref6"},{"key":"S0960129523000300_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/12.372041"},{"key":"S0960129523000300_ref4","doi-asserted-by":"crossref","unstructured":"Blum, M. , Luby, M. and Rubinfeld, R. (1990). Program result checking against adaptive programs and in cryptographic settings (extended abstract). In: DIMACS Workshop on Distributed Computing and Crypthography, American Mathematical Society, 107\u2013118.","DOI":"10.1090\/dimacs\/002\/06"},{"key":"S0960129523000300_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_9"},{"key":"S0960129523000300_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029974"},{"key":"S0960129523000300_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-019-00554-z"},{"key":"S0960129523000300_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-016-0131-1"},{"key":"S0960129523000300_ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016339119669"},{"key":"S0960129523000300_ref28","unstructured":"Sankowski, P. (2018). NC algorithms for weighted planar perfect matching and related problems. In: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 107, Dagstuhl, Germany, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 97:1\u201397:16."},{"key":"S0960129523000300_ref9","unstructured":"Edmonds, J. (1967). An introduction to matching. Mimeographed notes. Engineering Summer Conference, University of Michigan, Ann Arbor, MI."},{"volume-title":"Integer and Combinatorial Optimization","year":"1999","author":"Nemhauser","key":"S0960129523000300_ref25"},{"key":"S0960129523000300_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"S0960129523000300_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055766"},{"key":"S0960129523000300_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"volume-title":"Theory of Linear and Integer Programming","year":"1987","author":"Schrijver","key":"S0960129523000300_ref29"},{"key":"S0960129523000300_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_18"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T11:02:05Z","timestamp":1717412525000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000300\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,11]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["S0960129523000300"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000300","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2023,9,11]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}