{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T12:45:55Z","timestamp":1759063555244,"version":"3.41.2"},"reference-count":40,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,12,19]],"date-time":"2005-12-19T00:00:00Z","timestamp":1134950400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Given a formula in quantifier-free Presburger arithmetic, if it has a satisfying solution, there is one whose size, measured in bits, is polynomially bounded in the size of the formula. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are difference (separation) constraints, and the non-difference constraints are sparse. This class has been observed to commonly occur in software verification. We derive a new solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of non-difference constraints, in addition to traditional measures of formula size. In particular, we show that the number of bits needed per integer variable is linear in the number of non-difference constraints and logarithmic in the number and size of non-zero coefficients in them, but is otherwise independent of the total number of linear constraints in the formula. The derived bound can be used in a decision procedure based on instantiating integer variables over a finite domain and translating the input quantifier-free Presburger formula to an equi-satisfiable Boolean formula, which is then checked using a Boolean satisfiability solver. In addition to our main theoretical result, we discuss several optimizations for deriving tighter bounds in practice. Empirical evidence indicates that our decision procedure can greatly outperform other decision procedures.<\/jats:p>","DOI":"10.2168\/lmcs-1(2:6)2005","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:24:58Z","timestamp":1164273898000},"source":"Crossref","is-referenced-by-count":4,"title":["Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds"],"prefix":"10.46298","volume":"Volume 1, Issue 2","author":[{"given":"Sanjit A.","family":"Seshia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,12,19]]},"reference":[{"key":"10.2168\/LMCS-1(2:6)2005_ackermann-54","unstructured":"W. Ackermann.Solvable Cases of the Decision Problem. North-Holland, Amsterdam, 1954."},{"key":"10.2168\/LMCS-1(2:6)2005_brenner-amm72","doi-asserted-by":"publisher","DOI":"10.2307\/2317092"},{"key":"10.2168\/LMCS-1(2:6)2005_brinkmann-vlsi02","doi-asserted-by":"crossref","unstructured":"R. Brinkmann and R. Drechsler. RTL-datapath verification using integer linear programming. InProceedings of the IEEE VLSI Design Conference, pages 741-746, 2002.","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"10.2168\/LMCS-1(2:6)2005_barrett-cav02","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. L. Dill, and A. Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In E. Brinksma and K. G. Larsen, editors,Proc. 14th Intl. Conference on Computer-Aided Verification (CAV'02), LNCS 2404, pages 236-249. Springer-Verlag, July 2002.","DOI":"10.1007\/3-540-45657-0_18"},{"key":"10.2168\/LMCS-1(2:6)2005_borosh-pams89","doi-asserted-by":"publisher","DOI":"10.2307\/2047041"},{"key":"10.2168\/LMCS-1(2:6)2005_borosh-dismath86","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(86)90138-X"},{"key":"10.2168\/LMCS-1(2:6)2005_ganesh-tacas03","doi-asserted-by":"crossref","unstructured":"S. Berezin, V. Ganesh, and D. L. Dill. An online proof-producing decision procedure for mixed-integer linear arithmetic. InProc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), LNCS 2619, pages 521-536, April 2003.","DOI":"10.1007\/3-540-36577-X_38"},{"key":"10.2168\/LMCS-1(2:6)2005_bryant-cav02","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_7"},{"key":"10.2168\/LMCS-1(2:6)2005_borosh-pams76","doi-asserted-by":"publisher","DOI":"10.2307\/2041711"},{"key":"10.2168\/LMCS-1(2:6)2005_borosh-siam-mtx92","doi-asserted-by":"publisher","DOI":"10.1137\/0613029"},{"key":"10.2168\/LMCS-1(2:6)2005_chaki-icse03","doi-asserted-by":"crossref","unstructured":"Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, and Helmut Veith. Modular verification of software components in C. InProc. 25th International Conference on Software Engineering (ICSE), pages 385-395, 2003.","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"10.2168\/LMCS-1(2:6)2005_chandru-compjnl93","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.5.463"},{"key":"10.2168\/LMCS-1(2:6)2005_cplex-www","unstructured":"CPLEX Optimization Tool. Available from ILOG. {\\tt http:\/\/www.ilog.com\/products\/cplex\/}. {CVC-Lite: Cooperating Validity Checker}. Available at {\\tt http:\/\/verify.stanford.edu\/CVCL\/}."},{"key":"10.2168\/LMCS-1(2:6)2005_demoura-cade02","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura, Harald Rue\\ss, and Maria Sorea. Lazy theorem proving for bounded model checking over infinite domains. InProc. 18th International Conference on Automated Deduction (CADE), pages 438-455, 2002.","DOI":"10.1007\/3-540-45620-1_35"},{"key":"10.2168\/LMCS-1(2:6)2005_detlefs-tr03","unstructured":"David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories Palo Alto, 2003."},{"key":"10.2168\/LMCS-1(2:6)2005_fischer-siam74","first-page":"27","volume":"7","author":"M. J. Fischer and M. O. Rabin","year":"1974","journal-title":"Proceedings of SIAM-AMS"},{"key":"10.2168\/LMCS-1(2:6)2005_ganesh-fmcad02","doi-asserted-by":"crossref","unstructured":"V. Ganesh, S. Berezin, and D. L. Dill. Deciding Presburger arithmetic by model checking and comparisons with other methods. InFormal Methods in Computer-Aided Design (FMCAD '02), LNCS 2517, pages 171-186. Springer-Verlag, November 2002.","DOI":"10.1007\/3-540-36126-X_11"},{"key":"10.2168\/LMCS-1(2:6)2005_goldberg-date02","doi-asserted-by":"crossref","unstructured":"E. Goldberg and Y. Novikov. BerkMin: A fast and robust SAT solver. InDesign Automation and Test in Europe (DATE) 2002, pages 142-149, 2002.","DOI":"10.1109\/DATE.2002.998262"},{"key":"10.2168\/LMCS-1(2:6)2005_henzinger-popl02","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy abstraction. InProc. 29th ACM Symposium on Principles of Programming Languages, pages 58-70, 2002.","DOI":"10.1145\/565816.503279"},{"key":"10.2168\/LMCS-1(2:6)2005_ics-www","doi-asserted-by":"crossref","unstructured":"{ICS: Integrated Canonizer and Solver}. Available at {\\tt http:\/\/www.icansolve.com}. R. Kannan and C. L. Monma. On the computational complexity of integer programming problems. InOptimisation and Operations Research, volume 157 ofLecture Notes in Economics and Mathematical Systems, pages 161-172. Springer-Verlag, 1978.","DOI":"10.1007\/978-3-642-95322-4_17"},{"key":"10.2168\/LMCS-1(2:6)2005_kroening-cav04","doi-asserted-by":"crossref","unstructured":"Daniel Kroening, Jo\u00ebl Ouaknine, Sanjit A. Seshia, and Ofer Strichman. Abstraction-based satisfiability solving of Presburger arithmetic. InProc. 16th International Conference on Computer-Aided Verification (CAV), pages 308-320, July 2004.","DOI":"10.1007\/978-3-540-27813-9_24"},{"key":"10.2168\/LMCS-1(2:6)2005_lash-www","doi-asserted-by":"crossref","unstructured":"{LASH Toolset}. Available at {\\tt http:\/\/www. montefiore.ulg.ac.be\/ {boigelot\/research\/lash}}. Stephen McCamant and Michael D. Ernst. Predicting problems caused by component upgrades. InProceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE), pages 287-296, 2003.","DOI":"10.1145\/949952.940110"},{"key":"10.2168\/LMCS-1(2:6)2005_moskewicz-dac01","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In38th Design Automation Conference (DAC '01), pages 530-535, June 2001.","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"10.2168\/LMCS-1(2:6)2005_moscow-ml-www","first-page":"245","volume":"1","author":"Moscow ML","year":"1979","journal-title":"Simplification by cooperating decision procedures. \\newblock ACM Transactions on Programming Languages and Systems 1(2):245-257, 1979"},{"key":"10.2168\/LMCS-1(2:6)2005_papadim-jacm81","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"10.2168\/LMCS-1(2:6)2005_pratt-77","unstructured":"Vaughan Pratt. Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, 1977. Cambridge, MA."},{"key":"10.2168\/LMCS-1(2:6)2005_presburger-27","first-page":"92","volume":"395","author":"M. Pre\\ssburger","year":"1929","journal-title":"{\\em Comptes-rendus du Premier Congr\u00e8s des Math\u00e9maticiens des Pays Slaves}, 395:92-101, 1929"},{"key":"10.2168\/LMCS-1(2:6)2005_pnueli-cav99","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small-domain instantiations. In N. Halbwachs and D. Peled, editors,Computer-Aided Verification, volume 1633 ofLecture Notes in Computer Science, pages 455-469. Springer-Verlag, July 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"10.2168\/LMCS-1(2:6)2005_papadim-steiglitz-82ch13","unstructured":"Christos H. Papadimitriou and Kenneth Steiglitz.Combinatorial Optimization: Algorithms and Complexity, chapter 13. Prentice-Hall, 1982."},{"key":"10.2168\/LMCS-1(2:6)2005_pugh-sc91","doi-asserted-by":"crossref","unstructured":"William Pugh. The omega test: A fast and practical integer programming algorithm for dependence analysis. InSupercomputing, pages 4-13, 1991.","DOI":"10.1145\/125826.125848"},{"key":"10.2168\/LMCS-1(2:6)2005_schrijver-86","unstructured":"Alexander Schrijver.Theory of Linear and Integer Programming. John Wiley and Sons, 1986."},{"key":"10.2168\/LMCS-1(2:6)2005_seshia-thesis05","unstructured":"Sanjit A. Seshia.Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. PhD thesis, Carnegie Mellon University, 2005."},{"key":"10.2168\/LMCS-1(2:6)2005_shostak-jacm84","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"10.2168\/LMCS-1(2:6)2005_shankar-rta02","doi-asserted-by":"crossref","unstructured":"Natarajan Shankar and Harald Rue\\ss. Combining Shostak theories. In Sophie Tison, editor,Proc. Rewriting Techniques and Applications, LNCS 2378, pages 1-18. Springer-Verlag, July 2002.","DOI":"10.1007\/3-540-45610-4_1"},{"key":"10.2168\/LMCS-1(2:6)2005_strichman-cav02","doi-asserted-by":"crossref","unstructured":"O. Strichman, S. A. Seshia, and R. E. Bryant. Deciding separation formulas with SAT. In E. Brinksma and K. G. Larsen, editors,Proc. 14th Intl. Conference on Computer-Aided Verification (CAV'02), LNCS 2404, pages 209-222. Springer-Verlag, July 2002.","DOI":"10.1007\/3-540-45657-0_16"},{"key":"10.2168\/LMCS-1(2:6)2005_seshia-tr04","doi-asserted-by":"crossref","unstructured":"Sanjit A. Seshia, K. Subramani, and Randal E. Bryant. On solving Boolean combinations of generalized 2SAT constraints. Technical Report CMU-CS-04-179, Carnegie Mellon University, 2004.","DOI":"10.21236\/ADA460032"},{"key":"10.2168\/LMCS-1(2:6)2005_strichman-fmcad02","doi-asserted-by":"crossref","unstructured":"O. Strichman. On solving Presburger and linear arithmetic with SAT. InFormal Methods in Computer-Aided Design (FMCAD '02), LNCS 2517, pages 160-170. Springer-Verlag, November 2002.","DOI":"10.1007\/3-540-36126-X_10"},{"issue":"1","key":"10.2168\/LMCS-1(2:6)2005_uclid-www","first-page":"155","volume":"72","author":"{UCLID Verification System.","year":"1978","journal-title":"A bound on solutions of linear integer equalities and inequalities. \\newblock Proceedings of the American Mathematical Society 72(1):155-158, October 1978"},{"key":"10.2168\/LMCS-1(2:6)2005_wolper-sas95","doi-asserted-by":"crossref","unstructured":"Pierre Wolper and Bernard Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. InProc. Static Analysis Symposium, LNCS 983, pages 21-32, September 1995.","DOI":"10.1007\/3-540-60360-3_30"},{"key":"10.2168\/LMCS-1(2:6)2005_wisa-www","unstructured":"{Wisconsin Safety Analyzer Project}. \\tt {http:\/\/www.cs.wisc.edu\/wisa}. Steven A. Wolfman and Daniel S. Weld. The LPSAT engine and its application to resource planning. InProceedings of the International Joint Conference in Artificial Intelligence (IJCAI), pages 310-317, 1999."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2270\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2270\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T02:18:06Z","timestamp":1736648286000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12,19]]},"references-count":40,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(2:6)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0508044","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0508044","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-540-27813-9_40","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,12,19]]},"article-number":"2270"}}