{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:39:05Z","timestamp":1773808745725,"version":"3.50.1"},"reference-count":64,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2021,12,22]],"date-time":"2021-12-22T00:00:00Z","timestamp":1640131200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air-Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-19-1-0177"],"award-info":[{"award-number":["FA9550-19-1-0177"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Air-Force Research Laboratory, Rome","award":["FA8750-17-S-7007"],"award-info":[{"award-number":["FA8750-17-S-7007"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,6,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In this paper, we discuss exact and parameterized algorithms for the problem of finding a read-once refutation (ROR) in an unsatisfiable Horn constraint system (HCS). Recall that a linear constraint system $\\mathbf {A \\cdot x \\ge b}$ is said to be an HCS if each entry in $\\textbf {A}$ belongs to the set $\\{0,1,-1\\}$ and at most one entry in each row of $\\textbf {A}$ is positive. In this paper, we examine the importance of constraints in which more variables have negative coefficients than positive coefficients. In particular, we study the impact of the proportion of these \u2018net-negative\u2019 constraints has on the difficulty of finding RORs. There exist several algorithms for checking whether an HCS is feasible. To the best of our knowledge, these algorithms are not certifying, i.e. they do not provide a certificate of infeasibility. Our work is concerned with providing a specialized class of certificates called \u2018read-once refutations\u2019. In an ROR, each constraint defining the HCS may be used at most once in the derivation of a refutation. The problem of checking if an HCS has an ROR has been shown to be NP-hard. We analyse the HCS ROR problem from three different algorithmic perspectives, viz., parameterized algorithms, exact exponential algorithms and approximation algorithms. In particular, we show that the HCS ROR problem is fixed-parameter tractable (FPT) with respect to the number of constraints in the system that have more variables with negative coefficient than variables with positive coefficient. Additionally, we show that the HCS ROR problem becomes easy when this parameter is both small and large. We also derive an algorithm that runs in time $O(1.66^{m})$, where $m$ is the number of constraints in the HCS. On the lower-bound side, we derive a lower bound on the algorithmic resources needed for this problem using the Exponential Time Hypothesis. We also establish that the HCS ROR problem does not have a polynomial kernel when the number of constraints with three or more variables in a refutation is used as a parameter. Finally, we show that the problem of approximating the length of the shortest ROR in an HCS is NPO PB-complete1.<\/jats:p>","DOI":"10.1093\/logcom\/exab072","type":"journal-article","created":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T20:17:49Z","timestamp":1636489069000},"page":"667-696","source":"Crossref","is-referenced-by-count":1,"title":["Read-once refutations in Horn constraint systems: an algorithmic approach"],"prefix":"10.1093","volume":"32","author":[{"given":"K","family":"Subramani","sequence":"first","affiliation":[{"name":"LDCSEE, West Virginia University , Morgantown, WV 26506, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[{"name":"LDCSEE, West Virginia University , Morgantown, WV 26506, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ying","family":"Sheng","sequence":"additional","affiliation":[{"name":"Department of Computer Science , Stanford University, Stanford, CA 94305, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2021,12,22]]},"reference":[{"key":"2022060307541429500_ref1","first-page":"176","article-title":"Minimum propositional proof length is NP-hard to linearly approximate","volume-title":"Mathematical Foundations of Computer Science (MFCS)","author":"Alekhnovich","year":"1998"},{"key":"2022060307541429500_ref2","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/BF02614366","article-title":"A new strongly polynomial dual network simplex algorithm","volume":"78","author":"Armstrong","year":"1997","journal-title":"Mathematical Programming"},{"key":"2022060307541429500_ref3","first-page":"23","article-title":"Combining forward and backward abstract interpretation of Horn clauses","volume-title":"Static Analysis, 24th International Symposium, SAS 2017","author":"Bakhirkin","year":"2017"},{"key":"2022060307541429500_ref4","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/BF00252179","article-title":"Linear and unit-resulting refutations for Horn theories","volume":"16","author":"Baumgartner","year":"1996","journal-title":"Journal of Automated Reasoning"},{"key":"2022060307541429500_ref5","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0890-5401(92)90056-L","article-title":"On the complexity of approximating the independent set problem","volume":"96","author":"Berman","year":"1992","journal-title":"Information and Computation"},{"key":"2022060307541429500_ref6","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","article-title":"Horn clause solvers for program verification","volume-title":"Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday","author":"Bj\u00f8rner","year":"2015"},{"key":"2022060307541429500_ref7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.entcs.2008.12.095","article-title":"Visualizing proof search for theorem prover development","volume":"226","author":"Byrnes","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2022060307541429500_ref8","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1016\/j.dam.2003.12.011","article-title":"Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing","volume":"149","author":"Cepek","year":"2005","journal-title":"Discrete Applied Mathematics"},{"key":"2022060307541429500_ref9","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.disopt.2012.11.001","article-title":"A combinatorial algorithm for Horn programs","volume":"10","author":"Chandrasekaran","year":"2013","journal-title":"Discrete Optimization"},{"key":"2022060307541429500_ref10","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1145\/102782.102789","article-title":"Extended Horn sets in propositional logic","volume":"38","author":"Chandru","year":"1991","journal-title":"Journal of ACM"},{"key":"2022060307541429500_ref11","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321607.321618","article-title":"The unit proof and the input proof in theorem proving","volume":"17","author":"Chang","year":"1970","journal-title":"Journal of ACM"},{"key":"2022060307541429500_ref12","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-540-25984-8_14","article-title":"The ICS decision procedures for embedded deduction","volume-title":"Automated Reasoning - Second International Joint Conference","author":"de Moura","year":"2004"},{"key":"2022060307541429500_ref13","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-54233-7_140","article-title":"Canonical sets of Horn clauses","volume-title":"Automata, Languages and Programming","author":"Dershowitz","year":"1991"},{"key":"2022060307541429500_ref14","first-page":"118","article-title":"Ordering-based strategies for Horn clauses","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence","author":"Dershowitz","year":"1991"},{"key":"2022060307541429500_ref15","article-title":"Proofs without words and beyond","volume":"11","author":"Doyle","year":"2014","journal-title":"Convergence"},{"key":"2022060307541429500_ref16","article-title":"The YICES SMT solver","volume-title":"Technical Report","author":"Duterre","year":"2006"},{"key":"2022060307541429500_ref17","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":"2022060307541429500_ref18","article-title":"An Introduction to Probability Theory and its Applications","author":"Feller","year":"1970"},{"key":"2022060307541429500_ref19","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1016\/j.tcs.2005.10.005","article-title":"On finding short resolution refutations and small unsatisfiable subsets","volume":"351","author":"Fellows","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"2022060307541429500_ref20","article-title":"Kernelization: Theory of Parameterized Preprocessing","author":"Fomin","year":"2019"},{"key":"2022060307541429500_ref21","first-page":"347","article-title":"Formal verification of a combination decision procedure","author":"Ford","year":"2002","journal-title":"18th International Conference on Automated Deduction"},{"key":"2022060307541429500_ref22","first-page":"345","article-title":"Efficient generation of correctness certificates for the abstract domain of polyhedra","volume-title":"Static Analysis, 20th International Symposium, SAS 2013","author":"Fouilh\u00e9","year":"2013"},{"key":"2022060307541429500_ref23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8047-2","article-title":"Discrete Mathematics","author":"Gallier","year":"2011"},{"key":"2022060307541429500_ref24","article-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey","year":"1979"},{"key":"2022060307541429500_ref25","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"2022060307541429500_ref26","doi-asserted-by":"crossref","first-page":"816","DOI":"10.1109\/TC.1976.1674700","article-title":"Semantic resolution for Horn sets","volume":"25","author":"Henschen","year":"1976","journal-title":"IEEE Transactions on Computers"},{"key":"2022060307541429500_ref27","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","article-title":"Unit refutations and Horn sets","volume":"21","author":"Henschen","year":"1974","journal-title":"Journal of ACM"},{"key":"2022060307541429500_ref28","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1287\/ijoc.1.3.137","article-title":"Input proofs and rank one cutting planes","volume":"1","author":"Hooker","year":"1989","journal-title":"INFORMS Journal on Computing"},{"key":"2022060307541429500_ref29","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1006\/jcss.2001.1774","article-title":"Which problems have strongly exponential complexity?","volume":"63","author":"Impagliazzo","year":"2001","journal-title":"Journal of Computer and System Sciences"},{"key":"2022060307541429500_ref30","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/SCT.1995.514725","article-title":"Intractability of read-once resolution","volume-title":"Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC 95)","author":"Iwama","year":"1995"},{"key":"2022060307541429500_ref31","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF01273369","article-title":"Visual theorems","volume":"24","author":"Davis","year":"1993","journal-title":"Educational Studies in Mathematics"},{"key":"2022060307541429500_ref32","article-title":"Constraint logic programming: a survey","volume":"19\u201320","author":"Jaffar","year":"1994","journal-title":"The Journal of Logic Programming"},{"key":"2022060307541429500_ref33","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1609\/aimag.v37i3.2671","article-title":"The answer set programming paradigm","volume":"37","author":"Janhunen","year":"2016","journal-title":"AI Magazine"},{"key":"2022060307541429500_ref34","first-page":"317","article-title":"Polynomially bounded minimization problems that are hard to approximate","volume":"1","author":"Kann","year":"1994","journal-title":"Nordic Journal of Computing"},{"key":"2022060307541429500_ref35","first-page":"149","article-title":"Restricted cutting plane proofs in horn constraint systems","volume-title":"Frontiers of Combining Systems, 12th International Symposium, FroCoS 2019, London, UK, 4\u20136 September 2019, volume 11715 of Lecture Notes in Computer Science","author":"B\u00fcning","year":"2019"},{"key":"2022060307541429500_ref36","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1016\/j.tcs.2018.02.002","article-title":"Finding read-once resolution refutations in systems of 2CNF clauses","volume":"729","author":"B\u00fcning","year":"2018","journal-title":"Theoretical Computer Science"},{"key":"2022060307541429500_ref37","first-page":"43:1","article-title":"New results on cutting plane proofs for Horn constraint systems","volume-title":"39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, 11\u201313 December 2019, Bombay, India","author":"B\u00fcning","year":"2019"},{"key":"2022060307541429500_ref38","first-page":"100","article-title":"Read-once resolutions in Horn formulas","volume-title":"Frontiers in Algorithmics, 13th International Workshop, FAW 2019, Sanya, China, 29 April\u20133 May 2019","author":"B\u00fcning","year":"2019"},{"key":"2022060307541429500_ref39","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1023\/A:1016339119669","article-title":"The complexity of read-once resolution","volume":"36","author":"B\u00fcning","year":"2002","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2022060307541429500_ref40","first-page":"356","article-title":"Read-once unit resolution","volume-title":"Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, 5\u20138 May 2003. Selected Revised Papers","author":"B\u00fcning","year":"2003"},{"key":"2022060307541429500_ref41","first-page":"89","article-title":"Compositional verification of procedural programs using Horn clauses over integers and arrays","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, TX, USA, 27\u201330 September 2015","author":"Komuravelli","year":"2015"},{"key":"2022060307541429500_ref42","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1080\/10556788.2014.895828","article-title":"Minimum-cost flow algorithms: an experimental evaluation","volume":"30","author":"Kov\u00e1cs","year":"2015","journal-title":"Optimization Methods and Software"},{"key":"2022060307541429500_ref43","first-page":"168","article-title":"An Efficient Decision Procedure for UTVPI Constraints","volume-title":"Proceedings of the 5th International Workshop on the Frontiers of Combining Systems, September 19\u201321, Vienna, Austria","author":"Lahiri","year":"2005"},{"key":"2022060307541429500_ref44","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-25951-0_1","article-title":"Specifying compositional units for correct program development in computational logic","volume-title":"Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development","author":"Lau","year":"2004"},{"key":"2022060307541429500_ref45","article-title":"Subextremal functions and lattice programming","volume":"10","author":"LiCalzi","year":"2005","journal-title":"SSRN Electronic Journal"},{"key":"2022060307541429500_ref46","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-24658-7","volume-title":"Answer Set Programming","author":"Lifschitz","year":"2019"},{"key":"2022060307541429500_ref47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","article-title":"LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation","volume":"29","author":"Minoux","year":"1988","journal-title":"Information Processing Letters"},{"key":"2022060307541429500_ref48","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(90)90043-5","article-title":"Refutation search for Horn sets by a subgoal-extraction method","volume":"9","author":"Neiman","year":"1990","journal-title":"Journal of Logic Programming"},{"key":"2022060307541429500_ref49","first-page":"93","article-title":"Linear and input resolution","author":"Nienhuys-Cheng","year":"1997"},{"key":"2022060307541429500_ref50","article-title":"On approximation preserving reductions: complete problems and robust measures. Technical Report","volume-title":"Department of Computer Science","author":"Orponen","year":"1987"},{"key":"2022060307541429500_ref51","doi-asserted-by":"crossref","first-page":"897","DOI":"10.1080\/00029890.2001.11919824","article-title":"Visible structures in number theory","volume":"108","author":"Borwein","year":"2001","journal-title":"American Mathematics Monthly"},{"key":"2022060307541429500_ref52","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s13218-018-0550-z","article-title":"Answer set programming unleashed!","volume":"32","author":"Schaub","year":"2018","journal-title":"K\u00fcnstliche Intell."},{"key":"2022060307541429500_ref53","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","article-title":"Swaminathan. On finding solutions for extended Horn formulas","volume":"54","author":"Schlipf","year":"1995","journal-title":"Information Processing Letters"},{"key":"2022060307541429500_ref54","article-title":"Theory of Linear and Integer Programming","author":"Schrijver","year":"1987"},{"key":"2022060307541429500_ref55","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s10817-009-9139-4","article-title":"Optimal length resolution refutations of difference constraint systems","volume":"43","author":"Subramani","year":"2009","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"2022060307541429500_ref56","doi-asserted-by":"crossref","first-page":"2765","DOI":"10.1007\/s00453-019-00554-z","article-title":"A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints","volume":"81","author":"Subramani","year":"2019","journal-title":"Algorithmica"},{"key":"2022060307541429500_ref57","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-93100-1_21","article-title":"Exact and parameterized algorithms for read-once refutations in Horn constraint systems","author":"Subramani","year":"2022"},{"key":"2022060307541429500_ref58","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2014.12.016","article-title":"Feasibility checking in Horn constraint systems through a reduction based approach","volume":"576","author":"Subramani","year":"2015","journal-title":"Theoretical Computer Science"},{"key":"2022060307541429500_ref59","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0166-218X(95)80005-O","article-title":"The arborescence-realization problem","volume":"59","author":"Swaminathan","year":"1995","journal-title":"Discrete Applied Mathematics"},{"key":"2022060307541429500_ref60","first-page":"168","article-title":"NP-completeness of refutability by literal-once resolution","volume-title":"Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, 18\u201323 June 2001","author":"Szeider","year":"2001"},{"key":"2022060307541429500_ref61","author":"Truemper","year":"2003"},{"key":"2022060307541429500_ref62","author":"Wasilewska","year":"2019"},{"key":"2022060307541429500_ref63","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(83)90020-8","article-title":"Some consequences of non-uniform conditions on uniform classes","volume":"26","author":"Yap","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"2022060307541429500_ref64","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1093\/teamat\/23.3.108","article-title":"From visualizing to proving","volume":"23","author":"Zarzycki","year":"09 2004","journal-title":"Teaching Mathematics and Its Applications"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/4\/667\/43933791\/exab072.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/32\/4\/667\/43933791\/exab072.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,3]],"date-time":"2022-06-03T07:55:48Z","timestamp":1654242948000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/32\/4\/667\/6470743"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,22]]},"references-count":64,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2021,12,22]]},"published-print":{"date-parts":[[2022,6,1]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab072","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,6]]},"published":{"date-parts":[[2021,12,22]]}}}