{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T11:08:06Z","timestamp":1764587286995},"reference-count":40,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T00:00:00Z","timestamp":1081296000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2004,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper is concerned with techniques for identifying simple and quantified lattice points in 2SAT polytopes. 2SAT polytopes generalize the polyhedra corresponding to Boolean 2SAT formulas, Vertex\u2010Packing (Covering, Partitioning) and Network flow problems; they find wide application in the domains of Program verification (Software Engineering) and State\u2010Space search (Artificial Intelligence). Our techniques are based on the symbolic elimination strategy called the Fourier\u2010Motzkin elimination procedure and thus have the advantages of being extremely simple (from an implementational perspective) and incremental. We also provide a characterization of a 2SAT polytope in terms of its extreme points and derive some interesting hardness results for associated optimization problems. Finally, we provide a brief discussion on the maximum size of a subdeterminant of the linear system representing a 2SAT polytope; this parameter plays a vital role in deriving analytical bounds on the size of the search space for checking whether the polyhedron includes a lattice point. (\u00a9 2004 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200310099","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T15:02:53Z","timestamp":1081350173000},"page":"281-292","source":"Crossref","is-referenced-by-count":14,"title":["On deciding the non\u2010emptiness of 2SAT polytopes with respect to First Order Queries"],"prefix":"10.1002","volume":"50","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2004,4,7]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"crossref","unstructured":"K. R.Apt andE. R.Olderog Verification of Sequential and Concurrent Programs (Springer\u2010Verlag New York et. al. 1997).","DOI":"10.1007\/978-1-4757-2714-2"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90002-4"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0024-3795(80)90162-7"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"H.Kleine\u2010B\u00fcning K.Subramani andXishunZhao On Boolean models for quantified Boolean Horn formulas. In: Proceedings 6th International Conference on Theory and Applications of Satisfiability (E. Giunchiglia and A. Tachhela eds.) Lecture Notes in Computer Science2919 93\u2013104 (2003).","DOI":"10.1007\/978-3-540-24605-3_8"},{"key":"e_1_2_1_7_2","doi-asserted-by":"crossref","unstructured":"V.Chandru andJ. N.Hooker Optimization Methods for Logical Inference (John Wiley and Sons New York 1999).","DOI":"10.1002\/9781118033166"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","unstructured":"V.Chandru andM. R.Rao Linear programming. In: Algorithms and Theory of Computation Handbook (CRC Press Boca Rato 1999).","DOI":"10.1201\/9781420049503-c32"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90199-6"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539791256325"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90069-5"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01582230"},{"key":"e_1_2_1_13_2","unstructured":"T. H.Cormen C. E.Leiserson andR. L.Rivest Introduction to Algorithms 2nd edition (MIT Press and McGraw\u2010Hill Book Company Boston 1992)."},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"e_1_2_1_15_2","unstructured":"J. B. J.Fourier Reported in: Analyse de travaux de l'Academie Royale des Sciences pendant l'annee 1824 Partie Mathematique History de l'Academie Royale de Sciences de l'Institue de France7xlvii \u2013 lv (1827). (Partial English translation in: D. A. Kohler Translation of a Report by Fourier on his work on Linear Inequalities. Opsearch10 38\u201342 (1973).)"},{"key":"e_1_2_1_16_2","unstructured":"M. R.Garey andD. S.Johnson Computers and Intractability: A Guide to the Theory of NP\u2010Completeness (W. H. Freeman Company San Francisco 1979)."},{"key":"e_1_2_1_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90038-B"},{"key":"e_1_2_1_18_2","unstructured":"M.Genesereth Logical Foundations of Artificial Intelligence (Morgan Kaufmann San Francisco 1990)."},{"key":"e_1_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321936"},{"key":"e_1_2_1_20_2","unstructured":"D. S.Hochbaum(editor) Approximation Algorithms for NP\u2010Hard Problems (PWS Publishing Company Boston 1996)."},{"key":"e_1_2_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01585160"},{"key":"e_1_2_1_22_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251876"},{"key":"e_1_2_1_23_2","doi-asserted-by":"crossref","unstructured":"T.Huynh C.Lassez andJ.\u2010L.Lassez Fourier Algorithm Revisited. In: Proceedings Second International Conference on Algebraic and Logic Programming Nancy October 1990 (H. Kirchner and W. Wechler eds.) Lecture Notes in Computer Science463 117\u2013131 (1991).","DOI":"10.1007\/3-540-53162-9_34"},{"key":"e_1_2_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/322169.322179"},{"key":"e_1_2_1_25_2","first-page":"1093","article-title":"A polynomial algorithm in linear programming","volume":"224","author":"Khachian L. G.","year":"1979","journal-title":"Doklady Akad. Nauk SSSR"},{"key":"e_1_2_1_26_2","doi-asserted-by":"publisher","DOI":"10.1137\/0214016"},{"key":"e_1_2_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245296"},{"key":"e_1_2_1_28_2","doi-asserted-by":"publisher","DOI":"10.1287\/moor.8.4.538"},{"key":"e_1_2_1_29_2","unstructured":"J.Loeckx andK.Sieber The Foundations of Program Verification (John Wiley and Sons New York 1985)."},{"key":"e_1_2_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01580444"},{"key":"e_1_2_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01580222"},{"key":"e_1_2_1_32_2","unstructured":"G. L.Nemhauser andL. A.Wolsey Integer and Combinatorial Optimization (John Wiley and Sons New York 1999)."},{"key":"e_1_2_1_33_2","unstructured":"N. J.Nilsson Artificial Intelligence: A New Synthesis (Morgan Kaufmann San Francisco 1998)."},{"key":"e_1_2_1_34_2","unstructured":"C. H.Papadimitriou Computational Complexity (Addison\u2010Wesley New York 1994)."},{"key":"e_1_2_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/135226.135233"},{"key":"e_1_2_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/291889.291900"},{"key":"e_1_2_1_37_2","doi-asserted-by":"crossref","unstructured":"T. J.Schaefer The complexity of satisfiability problems. In: Proceedings of the 10th Annual ACM Symposium on Theory of Computing New York City 1978 (A. Aho ed.) pp. 216\u2013226.","DOI":"10.1145\/800133.804350"},{"key":"e_1_2_1_38_2","unstructured":"A.Schrijver Theory of Linear and Integer Programming (John Wiley and Sons New York 1987)."},{"key":"e_1_2_1_39_2","unstructured":"K.Subramani An analyis of selected quantified integer programs. Theory of Computing Systems (submitted)."},{"key":"e_1_2_1_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(76)90055-8"},{"key":"e_1_2_1_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(83)90024-0"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200310099","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200310099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T21:05:04Z","timestamp":1697663104000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200310099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,7]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,5]]}},"alternative-id":["10.1002\/malq.200310099"],"URL":"https:\/\/doi.org\/10.1002\/malq.200310099","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,7]]}}}