{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:30:53Z","timestamp":1767339053393,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T00:00:00Z","timestamp":1560470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF-AF","award":["CCF-1524246"],"award-info":[{"award-number":["CCF-1524246"]}]},{"name":"NSF-SHF","award":["CCF-1714593"],"award-info":[{"award-number":["CCF-1714593"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2019,6,30]]},"abstract":"<jats:p>\n            We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>O<\/jats:italic>\n              (1)\n            <\/jats:sup>\n            size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>O<\/jats:italic>\n              (log\n              <jats:italic>n<\/jats:italic>\n              )\n            <\/jats:sup>\n            size proofs for these identities on Wallace tree multipliers.\n          <\/jats:p>","DOI":"10.1145\/3319396","type":"journal-article","created":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T12:56:40Z","timestamp":1560776200000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Toward Verifying Nonlinear Integer Arithmetic"],"prefix":"10.1145","volume":"66","author":[{"given":"Paul","family":"Beame","sequence":"first","affiliation":[{"name":"University of Washington, Seattle, Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Liew","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,6,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645413.652190"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/513918.514101"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2007.4295319"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622487.1622497"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682926"},{"key":"e_1_2_1_6_1","volume-title":"BIRS Workshop on Theory and Applications of Applied SAT Solving. http:\/\/www.birs.ca\/events\/2014\/5-day-workshops\/14w5101\/videos\/watch\/201401201634-Biere.html.","author":"Biere Armin","year":"2014","unstructured":"Armin Biere . 2014 b. Where does SAT not work? In BIRS Workshop on Theory and Applications of Applied SAT Solving. http:\/\/www.birs.ca\/events\/2014\/5-day-workshops\/14w5101\/videos\/watch\/201401201634-Biere.html. Armin Biere. 2014b. Where does SAT not work? In BIRS Workshop on Theory and Applications of Applied SAT Solving. http:\/\/www.birs.ca\/events\/2014\/5-day-workshops\/14w5101\/videos\/watch\/201401201634-Biere.html."},{"key":"e_1_2_1_7_1","volume-title":"Collection of combinational arithmetic miters submitted to the SAT competition","author":"Biere Armin","year":"2016","unstructured":"Armin Biere . 2016a. Collection of combinational arithmetic miters submitted to the SAT competition 2016 . In Proceedings of SAT Competition 2016 -- Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.), Vol. B-2016- 1 . University of Helsinki , 65--66. Armin Biere. 2016a. Collection of combinational arithmetic miters submitted to the SAT competition 2016. In Proceedings of SAT Competition 2016 -- Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.), Vol. B-2016-1. University of Helsinki, 65--66."},{"key":"e_1_2_1_8_1","volume-title":"Fields Institute Workshop on Theoretical Foundations of SAT Solving. http:\/\/www.fields.utoronto.ca\/talks\/weaknesses-cdcl-solvers.","author":"Biere Armin","year":"2016","unstructured":"Armin Biere . 2016 b. Weaknesses of CDCL solvers . In Fields Institute Workshop on Theoretical Foundations of SAT Solving. http:\/\/www.fields.utoronto.ca\/talks\/weaknesses-cdcl-solvers. Armin Biere. 2016b. Weaknesses of CDCL solvers. In Fields Institute Workshop on Theoretical Foundations of SAT Solving. http:\/\/www.fields.utoronto.ca\/talks\/weaknesses-cdcl-solvers."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.007"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380835"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/832284.835389"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770423"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"e_1_2_1_18_1","series-title":"Lecture Notes in Computer Science","volume-title":"Buss and Maria Luisa Bonet","author":"Samuel","year":"2012","unstructured":"Samuel R. Buss and Maria Luisa Bonet . 2012 . An improved separation of regular resolution from pool resolution and clause learning. In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT\u2019 12), Lecture Notes in Computer Science , Vol. 7313 , 244--57. Samuel R. Buss and Maria Luisa Bonet. 2012. An improved separation of regular resolution from pool resolution and clause learning. In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201912), Lecture Notes in Computer Science, Vol. 7313, 244--57."},{"key":"e_1_2_1_19_1","volume-title":"Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Log. Meth. Comput. Sci. 4, 4","author":"Buss Samuel R.","year":"2008","unstructured":"Samuel R. Buss , Jan Hoffmann , and Jan Johannsen . 2008. Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Log. Meth. Comput. Sci. 4, 4 ( 2008 ). Samuel R. Buss, Jan Hoffmann, and Jan Johannsen. 2008. Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Log. Meth. Comput. Sci. 4, 4 (2008)."},{"key":"e_1_2_1_20_1","volume-title":"Buss and Leszek Kolodziejczyk","author":"Samuel","year":"2014","unstructured":"Samuel R. Buss and Leszek Kolodziejczyk . 2014 . Small stone in pool. Log. Meth. Comput. Sci . 10, 2 (2014). Samuel R. Buss and Leszek Kolodziejczyk. 2014. Small stone in pool. Log. Meth. Comput. Sci. 10, 2 (2014)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_23_1","volume-title":"System Description: Yices 0.1. Technical Report. Computer Science Laboratory, SRI International.","author":"de Moura Leonardo Mendon\u00e7a","year":"2005","unstructured":"Leonardo Mendon\u00e7a de Moura . 2005 . System Description: Yices 0.1. Technical Report. Computer Science Laboratory, SRI International. Leonardo Mendon\u00e7a de Moura. 2005. System Description: Yices 0.1. Technical Report. Computer Science Laboratory, SRI International."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 12th Annual Conference on Uncertainty in Artificial Intelligence (UAI\u201996)","author":"Dechter Rina","year":"1996","unstructured":"Rina Dechter . 1996 . Bucket elimination: A unifying framework for probabilistic inference . In Proceedings of the 12th Annual Conference on Uncertainty in Artificial Intelligence (UAI\u201996) , Eric Horvitz and Finn Verner Jensen (Eds.). Morgan Kaufmann, 211--219. https:\/\/dslpitt.org\/uai\/displayArticleDetails.jsp?mmnu&equals;18smnu&equals;28article_id&equals;3708proceeding_id&equals;12. Rina Dechter. 1996. Bucket elimination: A unifying framework for probabilistic inference. In Proceedings of the 12th Annual Conference on Uncertainty in Artificial Intelligence (UAI\u201996), Eric Horvitz and Finn Verner Jensen (Eds.). Morgan Kaufmann, 211--219. https:\/\/dslpitt.org\/uai\/displayArticleDetails.jsp?mmnu&equals;18smnu&equals;28article_id&equals;3708proceeding_id&equals;12."},{"volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907)","author":"Ganesh Vijay","key":"e_1_2_1_26_1","unstructured":"Vijay Ganesh and David L. Dill . 2007. A decision procedure for bit-vectors and arrays . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907) , 519--531. Vijay Ganesh and David L. Dill. 2007. A decision procedure for bit-vectors and arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907), 519--531."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2893529.2893531"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-015-9653-1"},{"volume-title":"Propositional Logic and Complexity Theory","author":"Kraj\u00ed\u010dek Jan","key":"e_1_2_1_30_1","unstructured":"Jan Kraj\u00ed\u010dek . 1996. Bounded Arithmetic , Propositional Logic and Complexity Theory . Cambridge University Press . Jan Kraj\u00ed\u010dek. 1996. Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1391237"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895480192233867"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/244522.244560"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_35_1","unstructured":"Openssl.org. 2016. OpenSSL Bug CVE-2016-7055. Retrieved from https:\/\/www.openssl.org\/news\/secadv\/20161110.txt.  Openssl.org. 2016. OpenSSL Bug CVE-2016-7055. Retrieved from https:\/\/www.openssl.org\/news\/secadv\/20161110.txt."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996628"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225098"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/367072.367113"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168463"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/780542.780571"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2971808.2972053"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319396","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319396","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:21Z","timestamp":1750199901000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319396"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,14]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6,30]]}},"alternative-id":["10.1145\/3319396"],"URL":"https:\/\/doi.org\/10.1145\/3319396","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2019,6,14]]},"assertion":[{"value":"2018-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}