Skip to main content

2017 | OriginalPaper | Buchkapitel

On Optimization Modulo Theories, MaxSMT and Sorting Networks

verfasst von : Roberto Sebastiani, Patrick Trentin

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Optimization Modulo Theories (\(\text {OMT}\)) is an extension of SMT which allows for finding models that optimize given objectives. (Partial weighted) MaxSMT–or equivalently \(\text {OMT}\) with Pseudo-Boolean objective functions, \(\text {OMT+PB}\) – is a very-relevant strict subcase of \(\text {OMT}\). We classify existing approaches for MaxSMT or \(\text {OMT+PB}\) in two groups: MaxSAT-based approaches exploit the efficiency of state-of-the-art MaxSAT solvers, but they are specific-purpose and not always applicable; OMT-based approaches are general-purpose, but they suffer from intrinsic inefficiencies on MaxSMT/\(\text {OMT+PB}\) problems.
We identify a major source of such inefficiencies, and we address it by enhancing \(\text {OMT}\) by means of bidirectional sorting networks. We implemented this idea on top of the OptiMathSAT \(\text {OMT}\) solver. We run an extensive empirical evaluation on a variety of problems, comparing MaxSAT-based and \(\text {OMT}\)-based techniques, with and without sorting networks, implemented on top of OptiMathSAT and https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_14/447563_1_En_14_IEq10_HTML.gif . The results support the effectiveness of this idea, and provide interesting insights about the different approaches.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
Hereafter, when speaking of MaxSAT or MaxSMT, we keep “partial weighted” implicit.
 
2
For example, \(\frac{1799972218749879}{2251799813685248}\) is a sample weight value from problems in [34].
 
3
One could run a MaxSAT-based search separately on each objective, but doing this he/she would loose the benefits of boxed optimization, see [8, 15, 31].
 
4
The fact that such call is actually performed depends on the early-pruning strategy implemented in the OMT solver; alternatively, a possibly-expensive \(\mathcal {T}\)-propagation step on the previous \(\mathcal {LRA}\)-\(\mathsf {Solver}\) call has a similar effect. (See e.g. [5, 27].)
 
5
Here (14)–(18) are written as implications to emphasize the directionality of the encodings.
 
6
Notice that, unlike OptiMathSAT, https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_14/447563_1_En_14_IEq287_HTML.gif selects automatically its presumably-best configuration for a given input problem. In particular, when MaxSMT-encodable problems are fed to https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_14/447563_1_En_14_IEq288_HTML.gif –like, e.g., those in Sect. 5.1 https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_14/447563_1_En_14_IEq289_HTML.gif forces automatically the choice of the MaxSAT-based configuration, allowing the user only the choice of the MaxSAT algorithm. Thus we could not test https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_14/447563_1_En_14_IEq290_HTML.gif also with \(\text {OMT}\)-based configuration for the problems in Sect. 5.1. Alternatively, we should have disguised the input problem, with the risk of affecting the significance or the result.
 
Literatur
1.
Zurück zum Zitat Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A parametric approach for smaller and better encodings of cardinality constraints. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 80–96. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40627-0_9 CrossRef Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A parametric approach for smaller and better encodings of cardinality constraints. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 80–96. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40627-0_​9 CrossRef
2.
Zurück zum Zitat Alviano, M., Dodaro, C., Ricca, F.: A maxsat algorithm using cardinality constraints of bounded size. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 2677–2683. AAAI Press (2015) Alviano, M., Dodaro, C., Ricca, F.: A maxsat algorithm using cardinality constraints of bounded size. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 2677–2683. AAAI Press (2015)
3.
Zurück zum Zitat Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M., Theories, S.M.: An efficient approach for the resource-constrained project scheduling problem. In: SARA (2011) Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M., Theories, S.M.: An efficient approach for the resource-constrained project scheduling problem. In: SARA (2011)
4.
Zurück zum Zitat Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)MathSciNetCrossRefMATH Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)MathSciNetCrossRefMATH
5.
Zurück zum Zitat Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories, Chap. 26, vol. 185, pp. 825–885, Biere et al. [6], February 2009 Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories, Chap. 26, vol. 185, pp. 825–885, Biere et al. [6], February 2009
6.
Zurück zum Zitat Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, vol. 185. IOS Press, February 2009 Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, vol. 185. IOS Press, February 2009
7.
Zurück zum Zitat Bjorner, N.: Personal communication, 02 (2016) Bjorner, N.: Personal communication, 02 (2016)
9.
Zurück zum Zitat Bjørner, 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–199. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_14 Bjørner, 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–199. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​14
11.
Zurück zum Zitat Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99–113. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_8 CrossRef Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99–113. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-12002-2_​8 CrossRef
12.
Zurück zum Zitat Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150–165. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_12 CrossRef Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150–165. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39071-5_​12 CrossRef
13.
Zurück zum Zitat Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)MATH Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)MATH
14.
Zurück zum Zitat Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333–350. Springer, Heidelberg (2014). doi:10.1007/978-3-319-09284-3_25 Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333–350. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-09284-3_​25
15.
Zurück zum Zitat Li, Y., Albarghouthi, A., Kincad, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL (2014) Li, Y., Albarghouthi, A., Kincad, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL (2014)
16.
Zurück zum Zitat Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers, Chap. 4, vol. 185, pp. 131–153, Biere et al. [6], February 2009 Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers, Chap. 4, vol. 185, pp. 131–153, Biere et al. [6], February 2009
18.
Zurück zum Zitat Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided maxsat resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 27–31 July, Québec City, Québec, Canada, pp. 2717–2723. AAAI Press (2014) Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided maxsat resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 27–31 July, Québec City, Québec, Canada, pp. 2717–2723. AAAI Press (2014)
20.
Zurück zum Zitat 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–552. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46397-1_42 CrossRef 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–552. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-46397-1_​42 CrossRef
21.
Zurück zum Zitat Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006). doi:10.1007/11814948_18 CrossRef Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006). doi:10.​1007/​11814948_​18 CrossRef
25.
Zurück zum Zitat Roussel, O., Manquinho, V.: Pseudo-boolean and cardinality constraints, Chap. 22, vol. 185, pp. 695–733 Biere et al. [6], February 2009 Roussel, O., Manquinho, V.: Pseudo-boolean and cardinality constraints, Chap. 22, vol. 185, pp. 695–733 Biere et al. [6], February 2009
26.
Zurück zum Zitat Sawaya, N.W., Grossmann, I.E.: A cutting plane method for solving linear generalized disjunctive programming problems. Comput. Chem. Eng. 29(9), 1891–1913 (2005)CrossRef Sawaya, N.W., Grossmann, I.E.: A cutting plane method for solving linear generalized disjunctive programming problems. Comput. Chem. Eng. 29(9), 1891–1913 (2005)CrossRef
27.
Zurück zum Zitat Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. JSAT 3(3–4), 141–224 (2007)MathSciNetMATH Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. JSAT 3(3–4), 141–224 (2007)MathSciNetMATH
28.
Zurück zum Zitat Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484–498. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_38 CrossRef Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484–498. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31365-3_​38 CrossRef
29.
Zurück zum Zitat Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12 (2015)MathSciNetCrossRefMATH Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12 (2015)MathSciNetCrossRefMATH
30.
Zurück zum Zitat Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447–454. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_27 CrossRef Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447–454. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-21690-4_​27 CrossRef
31.
Zurück zum Zitat Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 335–349. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_27 Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 335–349. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​27
32.
Zurück zum Zitat Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005). doi:10.1007/11564751_73 CrossRef Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005). doi:10.​1007/​11564751_​73 CrossRef
Metadaten
Titel
On Optimization Modulo Theories, MaxSMT and Sorting Networks
verfasst von
Roberto Sebastiani
Patrick Trentin
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-54580-5_14