{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:32Z","timestamp":1776333452580,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:00:00Z","timestamp":1712880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSFC Grant","award":["62122078"],"award-info":[{"award-number":["62122078"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,12]]},"DOI":"10.1145\/3597503.3639105","type":"proceedings-article","created":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T16:43:26Z","timestamp":1712940206000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5541-7194","authenticated-orcid":false,"given":"Xindi","family":"Zhang","sequence":"first","affiliation":[{"name":"Institute of Software Chinese Academy of Science, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1356-6057","authenticated-orcid":false,"given":"Bohan","family":"Li","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Science, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Science, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Gilles Audemard and Laurent Simon. 2009. Predicting learnt clauses quality in modern SAT solvers. In Twenty-first international joint conference on artificial intelligence. Citeseer."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. SMT-COMP 14","author":"Behrmann Karsten","year":"2014","unstructured":"Karsten Behrmann, Andrej Dyck, Fabian Emmes, Carsten Fuhs, J\u00fcrgen Giesl, Patrick Kabasci, Peter Schneider-Kamp, and Ren\u00e9 Thiemann. 2014. Bit-blasting for SMT-NIA with AProVE. Proc. SMT-COMP 14 (2014)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"e_1_3_2_1_7_1","first-page":"316","article-title":"Cadical, lingeling, plingeling, treengeling and yalsat entering the sat competition 2018","volume":"14","author":"Biere Armin","year":"2017","unstructured":"Armin Biere. 2017. Cadical, lingeling, plingeling, treengeling and yalsat entering the sat competition 2018. Proceedings of SAT Competition 14 (2017), 316--336.","journal-title":"Proceedings of SAT Competition"},{"key":"e_1_3_2_1_8_1","volume-title":"Workshop on the Pragmatics of SAT.","author":"Biere Armin","year":"2020","unstructured":"Armin Biere and Mathias Fleury. 2020. Chasing target phases. In Workshop on the Pragmatics of SAT."},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of Pragmatics of SAT","author":"Biere Armin","year":"2015","unstructured":"Armin Biere and Andreas Fr\u00f6hlich. 2015. Evaluating CDCL restart schemes. Proceedings of Pragmatics of SAT (2015), 1--17."},{"key":"e_1_3_2_1_10_1","volume-title":"Handbook of satisfiability","author":"Biere Armin","unstructured":"Armin Biere, Marijn Heule, and Hans van Maaren. 2009. Handbook of satisfiability. Vol. 185. IOS press."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"e_1_3_2_1_12_1","volume-title":"15th International Workshop on Termination. 18","author":"Borralleras Cristina","year":"2016","unstructured":"Cristina Borralleras, Daniel Larraz, Albert Oliveras, Jos\u00e9 Miguel Rivero, Enric Rodr\u00edguez-Carbonell, and Albert Rubio. 2016. VeryMax: tool description for termCOMP 2016. In 15th International Workshop on Termination. 18."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340923"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9196-8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763544"},{"key":"e_1_3_2_1_17_1","volume-title":"d.]. Z3++ at SMT-COMP","author":"Cai Shaowei","year":"2022","unstructured":"Shaowei Cai, Bohan Li, Jinkun Lin, Zhonghan Wang, Bohua Zhan, Xindi Zhang, and Mengyu Zhao. [n. d.]. Z3++ at SMT-COMP 2022. ([n. d.])."},{"key":"e_1_3_2_1_18_1","volume-title":"Local Search For Satisfiability Modulo Integer Arithmetic Theories. ACM Transactions on Computational Logic","author":"Cai Shaowei","year":"2022","unstructured":"Shaowei Cai, Bohan Li, and Xindi Zhang. 2022. Local Search For Satisfiability Modulo Integer Arithmetic Theories. ACM Transactions on Computational Logic (2022)."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_12"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings 24","author":"Cai Shaowei","year":"2021","unstructured":"Shaowei Cai and Xindi Zhang. 2021. Deep cooperation of cdcl and local search for sat. In Theory and Applications of Satisfiability Testing-SAT 2021: 24th International Conference, Barcelona, Spain, July 5--9, 2021, Proceedings 24. Springer, 64--81."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.13666"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_23"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2018.00016"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134029"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1973.11993265"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1248547.1248548"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_33_1","volume-title":"SAT COMPETITION 2020","author":"Fleury ABKFM","year":"2020","unstructured":"ABKFM Fleury and Maximilian Heisinger. 2020. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. SAT COMPETITION 2020 (2020), 50."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1937.10503522"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings 10","author":"Fuhs Carsten","year":"2007","unstructured":"Carsten Fuhs, J\u00fcrgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren\u00e9 Thiemann, and Harald Zankl. 2007. SAT solving for termination analysis with polynomial interpretations. In Theory and Applications of Satisfiability Testing-SAT 2007: 10th International Conference, Lisbon, Portugal, May 28--31, 2007. Proceedings 10. Springer, 340--354."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006314320276"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_43"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Pei Huang Haoze Wu Yuting Yang Ieva Daukantas Min Wu Yedi Zhang and Clark Barrett. 2023. Towards Efficient Verification of Quantized Neural Networks. arXiv:2312.12679 [cs.LG]","DOI":"10.1609\/aaai.v38i19.30108"},{"key":"e_1_3_2_1_41_1","volume-title":"Thirty-seventh Conference on Neural Information Processing Systems.","author":"Jia Fuqi","year":"2023","unstructured":"Fuqi Jia, Yuhang Dong, Minghao Liu, Pei Huang, Feifei Ma, and Jian Zhang. 2023. Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning. In Thirty-seventh Conference on Neural Information Processing Systems."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598034"},{"key":"e_1_3_2_1_43_1","volume-title":"VMCAI 2017, Paris, France, January 15--17, 2017, Proceedings 18","author":"Jovanovi\u0107 Dejan","year":"2017","unstructured":"Dejan Jovanovi\u0107. 2017. Solving nonlinear integer arithmetic with MCSAT. In Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15--17, 2017, Proceedings 18. Springer, 330--346."},{"key":"e_1_3_2_1_44_1","volume-title":"The design and implementation of the model constructing satisfiability calculus. In 2013 Formal Methods in Computer-Aided Design","author":"Jovanovic Dejan","unstructured":"Dejan Jovanovic, Clark Barrett, and Leonardo De Moura. 2013. The design and implementation of the model constructing satisfiability calculus. In 2013 Formal Methods in Computer-Aided Design. IEEE, 173--180."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429135.2429155"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45641-6_21"},{"key":"e_1_3_2_1_47_1","volume-title":"Decision procedures","author":"Kroening Daniel","unstructured":"Daniel Kroening and Ofer Strichman. 2016. Decision procedures. Springer."},{"key":"e_1_3_2_1_48_1","volume-title":"Geometric series as nontermination arguments for linear lasso programs. arXiv preprint arXiv: 1405.4413","author":"Leike Jan","year":"2014","unstructured":"Jan Leike and Matthias Heizmann. 2014. Geometric series as nontermination arguments for linear lasso programs. arXiv preprint arXiv: 1405.4413 (2014)."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"e_1_3_2_1_50_1","volume-title":"Optimally solving the mcm problem using pseudo-boolean satisfiability. arXiv preprint arXiv: 1011.2685","author":"Lopes Nuno P","year":"2010","unstructured":"Nuno P Lopes, Levent Aksoy, Vasco Manquinho, and Jos\u00e9 Monteiro. 2010. Optimally solving the mcm problem using pseudo-boolean satisfiability. arXiv preprint arXiv: 1011.2685 (2010)."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_52_1","volume-title":"Bitwuzla at the SMT-COMP","author":"Niemetz Aina","year":"2020","unstructured":"Aina Niemetz and Mathias Preiner. 2020. Bitwuzla at the SMT-COMP 2020. arXiv preprint arXiv:2006.01621 (2020)."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings 10","author":"Pipatsrisawat Knot","year":"2007","unstructured":"Knot Pipatsrisawat and Adnan Darwiche. 2007. A lightweight component caching scheme for satisfiability solvers. In Theory and Applications of Satisfiability Testing-SAT 2007: 10th International Conference, Lisbon, Portugal, May 28--31, 2007. Proceedings 10. Springer, 294--299."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"e_1_3_2_1_57_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 418--423","author":"de Le\u00f3n Hern\u00e1n","year":"2022","unstructured":"Hern\u00e1n Ponce-de Le\u00f3n, Thomas Haas, and Roland Meyer. 2022. Dartagnan: Smt-based violation witness validation (competition contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 418--423."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190034"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of SAT Competition","author":"Soos Mate","year":"2016","unstructured":"Mate Soos. 2016. The CryptoMiniSat 5 set of solvers at SAT Competition 2016. Proceedings of SAT Competition (2016), 28."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_16"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_12"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"e_1_3_2_1_65_1","volume-title":"Proceedings of SAT competition","author":"Zhang Xindi","year":"2020","unstructured":"Xindi Zhang and Shaowei Cai. 2020. Relaxed backtracking with rephasing. Proceedings of SAT competition (2020), 15--15."},{"key":"e_1_3_2_1_66_1","volume-title":"SAT COMPETITION 2021","author":"Zhang Xindi","year":"2021","unstructured":"Xindi Zhang, Shaowei Cai, and Zhihan Chen. 2021. Improving cdcl via local search. SAT COMPETITION 2021 (2021), 42."}],"event":{"name":"ICSE '24: IEEE\/ACM 46th International Conference on Software Engineering","location":"Lisbon Portugal","acronym":"ICSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS","Faculty of Engineering of University of Porto"]},"container-title":["Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597503.3639105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:11Z","timestamp":1750286951000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,12]]},"references-count":66,"alternative-id":["10.1145\/3597503.3639105","10.1145\/3597503"],"URL":"https:\/\/doi.org\/10.1145\/3597503.3639105","relation":{},"subject":[],"published":{"date-parts":[[2024,4,12]]},"assertion":[{"value":"2024-04-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}