{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:07Z","timestamp":1747593607460,"version":"3.40.5"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Optimization Modulo Theories (OMT) has emerged as an important extension of the highly successful Satisfiability Modulo Theories (SMT) paradigm. The OMT problem requires solving an SMT problem with the restriction that the solution must be optimal with respect to a given objective function. We introduce a generalization of the OMT problem where, in particular, objective functions can range over partially ordered sets. We provide a formalization of and an abstract calculus for the Generalized OMT problem and prove their key correctness properties. Generalized OMT extends previous work on OMT in several ways. First, in contrast to many current OMT solvers, our calculus is theory-agnostic, enabling the optimization of queries over any theories or combinations thereof. Second, our formalization unifies both single- and multi-objective optimization problems, allowing us to study them both in a single framework and facilitating the use of objective functions that are not supported by existing OMT approaches. Finally, our calculus is sufficiently general to fully capture a wide variety of current OMT approaches (each of which can be realized as a specific strategy for rule application in the calculus) and to support the exploration of new search strategies. Much like the original abstract DPLL(T) calculus for SMT, our Generalized OMT calculus is designed to establish a theoretical foundation for understanding and research and to serve as a framework for studying variations of and extensions to existing OMT methodologies.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_27","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"458-479","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Generalized Optimization Modulo Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4729-9770","authenticated-orcid":false,"given":"Nestan","family":"Tsiskaridze","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"27_CR1","unstructured":"Akinlana, D.M.: New Developments in Statistical Optimal Designs for Physical and Computer Experiments. Ph.D. thesis, University of South Florida (2022)"},{"key":"27_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"27_CR3","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.185, pp. 825\u2013885. IOS Press (2009)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Bertolissi, C., dos Santos, D.R., Ranise, S.: Solving multi-objective workflow satisfiability problems with optimization modulo theories techniques. In: Bertino, E., Lin, D., Lobo, J. (eds.) Proceedings of the 23nd ACM on Symposium on Access Control Models and Technologies, SACMAT 2018, Indianapolis, IN, USA, June 13-15, 2018, pp. 117\u2013128. ACM (2018)","DOI":"10.1145\/3205977.3205982"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-66167-4_9","volume-title":"Frontiers of Combining Systems","author":"Z Bian","year":"2017","unstructured":"Bian, Z., Chudak, F., Macready, W., Roy, A., Sebastiani, R., Varotti, S.: Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 153\u2013171. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_9"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-030-86205-3_12","volume-title":"Frontiers of Combining Systems","author":"F Bigarella","year":"2021","unstructured":"Bigarella, F., et al.: Optimization modulo non-linear arithmetic via incremental linearization. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 213\u2013231. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_12"},{"key":"27_CR7","unstructured":"Bit-Monnot, A., Leofante, F., Pulina, L., \u00c1brah\u00e1m, E., Tacchella, A.: SMarTplan: a task planner for smart factories (2018). arXiv preprint arXiv:1806.07135"},{"key":"27_CR8","unstructured":"Bj\u00f8rner, N.S., Phan, A.D.: $$\\nu $$z - maximal satisfaction with z3. In: International Symposium on Symbolic Computation in Software Science (2014)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$\\nu $$Z - An optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14"},{"key":"27_CR10","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-319-40970-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2016","author":"L Candeago","year":"2016","unstructured":"Candeago, L., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Speeding up the constraint-based method in difference logic. In: Creignou, N., Le Berre, D. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016, pp. 284\u2013301. Springer International Publishing, Cham (2016)"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 99\u2013113. Springer, Berlin Heidelberg, Berlin, Heidelberg (2010)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-39071-5_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150\u2013165. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_12"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Craciunas, S.S., Oliver, R.S., Chmel\u00edk, M., Steiner, W.: Scheduling real-time communication in IEEE 802.1qbv time sensitive networks. In: Proceedings of the 24th International Conference on Real-Time Networks and Systems, p. 183-192. RTNS 2016, Association for Computing Machinery, New York, NY, USA (2016)","DOI":"10.1145\/2997465.2997470"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Demarchi, S., Menapace, M., Tacchella, A.: Automating elevator design with satisfiability modulo theories. In: 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI), pp. 26\u201333 (2019)","DOI":"10.1109\/ICTAI.2019.00013"},{"key":"27_CR15","unstructured":"Demarchi, S., Tacchella, A., Menapace, M.: Automated design of complex systems with constraint programming techniques. In: Proceedings of the Cyber-Physical Systems Ph.D Workshop 2019, CPS Summer School \u201cDesigning Cyber-Physical Systems - From concepts to implementation\u201d, Alghero, Italy, pp. 51\u201359 (2019)"},{"key":"27_CR16","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical Report, SRI International (2006)"},{"key":"27_CR17","unstructured":"Era\u015fcu, M., Micota, F., Zaharie, D.: Applying optimization modulo theory, mathematical programming and symmetry breaking for automatic deployment in the cloud of component-based applications extended abstract. In: 4th Women in Logic Workshop, p.\u00a06 (2020)"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Erata, F., Piskac, R., Mateu, V., Szefer, J.: Towards automated detection of single-trace side-channel vulnerabilities in constant-time cryptographic code (2023). arXiv preprint arXiv:2304.02102","DOI":"10.1109\/EuroSP57164.2023.00047"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-94205-6_10","volume-title":"Automated Reasoning","author":"K Fazekas","year":"2018","unstructured":"Fazekas, K., Bacchus, F., Biere, A.: Implicit hitting set algorithms for maximum satisfiability modulo theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 134\u2013151. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_10"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Feng, J., Zhang, T., Yi, C.: Reliability-aware comprehensive routing and scheduling in time-sensitive networking. In: Wireless Algorithms, Systems, and Applications: 17th International Conference, WASA 2022, Dalian, China, November 24\u201326, 2022, Proceedings, Part II, pp. 243\u2013254. Springer (2022)","DOI":"10.1007\/978-3-031-19214-2_20"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Gavran, I., Darulova, E., Majumdar, R.: Interactive synthesis of temporal specifications from examples and natural language. In: Proceedings of the ACM on Programming Languages, vol. 4(OOPSLA), pp. 1\u201326 (2020)","DOI":"10.1145\/3428269"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Gretsch, R., Song, P., Madhavan, A., Lau, J., Sherwood, T.: Energy efficient convolutions with temporal arithmetic. In: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, vol. 2, pp. 354\u2013368. ASPLOS 2024, Association for Computing Machinery, New York, NY, USA (2024)","DOI":"10.1145\/3620665.3640395"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Henry, J., Asavoae, M., Monniaux, D., Ma\u00efza, C.: How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In: Proceedings of the 2014 SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, Edinburgh, United Kingdom, pp. 43\u201352. Association for Computing Machinery, New York, NY, USA (2014)","DOI":"10.1145\/2597809.2597817"},{"key":"27_CR24","unstructured":"Jackson, D., Estler, H.C., Rayside, D.: The Guided Improvement Algorithm for Exact, General-Purpose, Many-Objective Combinatorial Optimization. Technical Report 2009-033, MIT-CSAIL (2009)"},{"key":"27_CR25","doi-asserted-by":"publisher","unstructured":"Jiang, J., Chen, L., Wu, X., Wang, J.: Block-wise abstract interpretation by combining abstract domains with SMT. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10145, pp. 310\u2013329. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_17","DOI":"10.1007\/978-3-319-52234-0_17"},{"issue":"2","key":"27_CR26","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1109\/JAS.2021.1003844","volume":"8","author":"X Jin","year":"2021","unstructured":"Jin, X., Xia, C., Guan, N., Zeng, P.: Joint algorithm of message fragmentation and no-wait scheduling for time-sensitive networks. IEEE\/CAA J. Automatica Sin. 8(2), 478\u2013490 (2021)","journal-title":"IEEE\/CAA J. Automatica Sin."},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"27_CR28","unstructured":"Karpenkov, G.E.: Finding inductive invariants using satisfiability modulo theories and convex optimization, Ph.D Thesis. Universit\u00e9 Grenoble Alpes (2017). https:\/\/tel.archives-ouvertes.fr\/tel-01681555\/file\/KARPENKOV_2017_diffusion.pdf"},{"key":"27_CR29","unstructured":"Kn\u00fcsel, M.: Optimizing Declarative Power Sequencing. Master thesis, ETH Zurich, Zurich (2021-09)"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Kov\u00e1sznai, G., Bir\u00f3, C., Erd\u00e9lyi, B.: Puli - a problem-specific OMT solver. EasyChair Preprints (2018)","DOI":"10.29007\/96p4"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS (LNAI), vol. 4720, pp. 1\u201327. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74621-8_1"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Lai, L., Fiaschi, L., Cococcioni, M., Deb, K.: Pure and mixed lexicographic-paretian many-objective optimization: state of the art. Nat. Comput. Int. J. 22(2), 227-242 (2022)","DOI":"10.1007\/s11047-022-09911-4"},{"key":"27_CR33","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-09284-3_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2014","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing - SAT 2014, pp. 333\u2013350. Springer International Publishing, Cham (2014)"},{"issue":"10","key":"27_CR34","doi-asserted-by":"publisher","first-page":"2142","DOI":"10.1109\/TCAD.2020.3037885","volume":"40","author":"D Lee","year":"2020","unstructured":"Lee, D., et al.: SP &R: SMT-based simultaneous place-and-route for standard cell synthesis of advanced nodes. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40(10), 2142\u20132155 (2020)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Leofante, F., Giunchiglia, E., \u00c1brah\u00e1m, E., Tacchella, A.: Optimal planning modulo theories. In: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, pp. 4128\u20134134 (2021)","DOI":"10.24963\/ijcai.2020\/571"},{"key":"27_CR36","doi-asserted-by":"publisher","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, USA, pp. 607\u2013618 (2014). https:\/\/doi.org\/10.1145\/2535838.2535857","DOI":"10.1145\/2535838.2535857"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-69483-2_9","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"T Liu","year":"2017","unstructured":"Liu, T., Tyszberowicz, S., Beckert, B., Taghdiri, M.: Computing exact loop bounds for bounded program verification. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 147\u2013163. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_9"},{"issue":"2","key":"27_CR38","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1109\/TII.2020.3002816","volume":"17","author":"G Marchetto","year":"2021","unstructured":"Marchetto, G., Sisto, R., Valenza, F., Yusupov, J., Ksentini, A.: A formal approach to verify connectivity and optimize VNF placement in industrial networks. IEEE Trans. Industr. Inf. 17(2), 1515\u20131525 (2021)","journal-title":"IEEE Trans. Industr. Inf."},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Model-based theory combination. In: Krstic, S., Oliveras, A. (eds.) Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, SMT@CAV 2007, Berlin, Germany, July 1-2, 2007. Electronic Notes in Theoretical Computer Science, vol.\u00a0198, pp. 37\u201349. Elsevier (2007)","DOI":"10.1016\/j.entcs.2008.04.079"},{"key":"27_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1007\/978-3-662-49674-9_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Nadel","year":"2016","unstructured":"Nadel, A., Ryvchin, V.: Bit-vector optimization. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 851\u2013867. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_53"},{"key":"27_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-319-46397-1_42","volume-title":"Conceptual Modeling","author":"CM Nguyen","year":"2016","unstructured":"Nguyen, C.M., Sebastiani, R., Giorgini, P., Mylopoulos, J.: Requirements evolution and evolution requirements with constrained goal models. In: Comyn-Wattiau, I., Tanaka, K., Song, I.-Y., Yamamoto, S., Saeki, M. (eds.) ER 2016. LNCS, vol. 9974, pp. 544\u2013552. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46397-1_42"},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Nguyen, C.M., Sebastiani, R., Giorgini, P., Mylopoulos, J.: Modeling and reasoning on requirements evolution with constrained goal models. In: Cimatti, A., Sirjani, M. (eds.) Software Engineering and Formal Methods - 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10469, pp. 70\u201386. Springer (2017)","DOI":"10.1007\/978-3-319-66197-1_5"},{"issue":"2","key":"27_CR43","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s00766-016-0263-5","volume":"23","author":"CM Nguyen","year":"2016","unstructured":"Nguyen, C.M., Sebastiani, R., Giorgini, P., Mylopoulos, J.: Multi-objective reasoning with constrained goal models. Requirements Eng. 23(2), 189\u2013225 (2016). https:\/\/doi.org\/10.1007\/s00766-016-0263-5","journal-title":"Requirements Eng."},{"key":"27_CR44","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing - SAT 2006, pp. 156\u2013169. Springer, Berlin Heidelberg, Berlin, Heidelberg (2006)"},{"issue":"6","key":"27_CR45","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"27_CR46","doi-asserted-by":"crossref","unstructured":"Paoletti, N., et al.: Synthesizing stealthy reprogramming attacks on cardiac devices. In: Proceedings of the 10th ACM\/IEEE International Conference on Cyber-Physical Systems, ICCPS 2019, pp. 13\u201322. Association for Computing Machinery, New York, NY, USA (2019)","DOI":"10.1145\/3302509.3311044"},{"key":"27_CR47","doi-asserted-by":"crossref","unstructured":"Park, D., Lee, D., Kang, I., Gao, S., Lin, B., Cheng, C.K.: SP &R: simultaneous placement and routing framework for standard cell synthesis in sub-7nm. In: 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 345\u2013350 (2020)","DOI":"10.1109\/ASP-DAC47756.2020.9045729"},{"key":"27_CR48","doi-asserted-by":"crossref","unstructured":"Patti, G., Bello, L.L., Leonardi, L.: Deadline-aware online scheduling of tsn flows for automotive applications. IEEE Trans. Ind. Inform. 19(4), 5774\u20135784 (2022)","DOI":"10.1109\/TII.2022.3184069"},{"key":"27_CR49","doi-asserted-by":"crossref","unstructured":"Ratschan, S.: Simulation based computation of certificates for safety of dynamical systems (2017). arXiv preprint arXiv:1707.00879","DOI":"10.1007\/978-3-319-65765-3_17"},{"key":"27_CR50","unstructured":"Roc, O.V.: Optimization Modulo Theories. Master\u2019s thesis, Polytechnic University of Catalonia. https:\/\/upcommons.upc.edu\/handle\/2099.1\/14204 (2011)"},{"key":"27_CR51","doi-asserted-by":"crossref","unstructured":"Rybalchenko, A., Vuppalapati, C.: Supercharging plant configurations using z3. In: Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 18th International Conference, CPAIOR 2021, Vienna, Austria, July 5\u20138, 2021, Proceedings. vol. 12735, p.\u00a01. Springer Nature (2021)","DOI":"10.1007\/978-3-030-78230-6_1"},{"key":"27_CR52","doi-asserted-by":"crossref","unstructured":"Schmitt, T., Hoffmann, M., Rodemann, T., Adamy, J.: Incorporating human preferences in decision making for dynamic multi-objective optimization in model predictive control. Inventions 7(3), 46 (2022)","DOI":"10.3390\/inventions7030046"},{"key":"27_CR53","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-662-46681-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 335\u2013349. Springer, Berlin Heidelberg, Berlin, Heidelberg (2015)"},{"key":"27_CR54","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with $$\\cal{LA} $$($$\\mathbb{Q} $$) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning, pp. 484\u2013498. Springer, Berlin Heidelberg, Berlin, Heidelberg (2012)"},{"key":"27_CR55","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logic 16(2), 1\u201343 (2015)","DOI":"10.1145\/2699915"},{"issue":"3","key":"27_CR56","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-09508-6","volume":"64","author":"R Sebastiani","year":"2018","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. J. Autom. Reasoning 64(3), 423\u2013460 (2018). https:\/\/doi.org\/10.1007\/s10817-018-09508-6","journal-title":"J. Autom. Reasoning"},{"key":"27_CR57","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-54580-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Sebastiani","year":"2017","unstructured":"Sebastiani, R., Trentin, P.: On optimization modulo theories, maxSMT and sorting networks. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 231\u2013248. Springer, Berlin Heidelberg, Berlin, Heidelberg (2017)"},{"key":"27_CR58","doi-asserted-by":"crossref","unstructured":"Shen, D., Zhang, T., Wang, J., Deng, Q., Han, S., Hu, X.S.: QoS guaranteed resource allocation for coexisting eMBB and URLLC traffic in 5G industrial networks. In: 2022 IEEE 28th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), pp. 81\u201390. IEEE (2022)","DOI":"10.1109\/RTCSA55878.2022.00015"},{"key":"27_CR59","first-page":"11936","volume":"33","author":"A Sivaraman","year":"2020","unstructured":"Sivaraman, A., Farnadi, G., Millstein, T., Van den Broeck, G.: Counterexample-guided learning of monotonic neural networks. Adv. Neural. Inf. Process. Syst. 33, 11936\u201311948 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"27_CR60","doi-asserted-by":"crossref","unstructured":"Subramanian, S., Berzish, M., Tripp, O., Ganesh, V.: A solver for a theory of strings and bit-vectors. In: 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C), pp. 124\u2013126 (2017)","DOI":"10.1109\/ICSE-C.2017.73"},{"key":"27_CR61","unstructured":"Tarrach, T., Ebrahimi, M., K\u00f6nig, S., Schmittner, C., Bloem, R., Nickovic, D.: Thorsten Tarrach and Masoud Ebrahimi and Sandra K\u00f6nig and Christoph Schmittner and Roderick Bloem and Dejan Nickovic, WorkingPaper (2022)"},{"key":"27_CR62","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1016\/j.artint.2015.04.002","volume":"244","author":"S Teso","year":"2017","unstructured":"Teso, S., Sebastiani, R., Passerini, A.: Structured learning modulo theories. Artif. Intell. 244, 166\u2013187 (2017)","journal-title":"Artif. Intell."},{"key":"27_CR63","doi-asserted-by":"crossref","unstructured":"Tierno, A., Turri, G., Cimatti, A., Passerone, R.: Symbolic encoding of reliability for the design of redundant architectures. In: 2022 IEEE 5th International Conference on Industrial Cyber-Physical Systems (ICPS), pp. 01\u201306 (2022)","DOI":"10.1109\/ICPS51978.2022.9816888"},{"key":"27_CR64","unstructured":"Trentin, P.: Optimization Modulo Theories with OptiMathSAT. Ph.D. thesis, University of Trento (2019)"},{"key":"27_CR65","doi-asserted-by":"crossref","unstructured":"Trentin, P., Sebastiani, R.: Optimization modulo the theories of signed bit-vectors and floating-point numbers. J. Autom. Reason. 65(7), 1071-1096 (2021)","DOI":"10.1007\/s10817-021-09600-4"},{"issue":"7","key":"27_CR66","doi-asserted-by":"publisher","first-page":"1071","DOI":"10.1007\/s10817-021-09600-4","volume":"65","author":"P Trentin","year":"2021","unstructured":"Trentin, P., Sebastiani, R.: Optimization modulo the theories of signed bit-vectors and floating-point numbers. J. Autom. Reason. 65(7), 1071\u20131096 (2021)","journal-title":"J. Autom. Reason."},{"key":"27_CR67","doi-asserted-by":"crossref","unstructured":"Tsiskaridze, N., Barrett, C., Tinelli, C.: Generalized optimization modulo theories (2024). arXiv preprint arXiv:2404.16122","DOI":"10.1007\/978-3-031-63498-7_27"},{"key":"27_CR68","unstructured":"Tsiskaridze, N., et al.: Automating system configuration. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021, pp. 102\u2013111. IEEE (2021)"},{"key":"27_CR69","doi-asserted-by":"crossref","unstructured":"Yao, P., Shi, Q., Huang, H., Zhang, C.: Program analysis via efficient symbolic abstraction. In: Proceedings of the ACM on Programming Languages, vol. 5(OOPSLA), pp. 1\u201332 (2021)","DOI":"10.1145\/3485495"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:42Z","timestamp":1747592262000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}