Abstract
We present OptiLog, a new Python framework for rapid prototyping of SAT-based systems. OptiLog allows to use and integrate SAT solvers currently developed in C/C++ just by implementing the iSAT C++ interface. It also provides a Python binding to the PBLib C++ toolkit for encoding Pseudo Boolean and Cardinality constraints. Finally, it leverages the power of automatic configurators by allowing to easily create configuration scenarios including multiple solvers and encoders.
Supported by MINECO-FEDER TASSAT3 (TIN2016-76573-C2-2-P), MICINNs PROOFS (PID2019-109137GB-C21) and FPU fellowship (FPU18/02929).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Opti stands for Optimization and LOG stands for Logic Optimization Group at UdL (http://ulog.udl.cat/).
- 2.
We will add in short a normalization step for general PB constraints.
- 3.
A SAT solver developer can make his solver configurable providing a json describing all the parameters with their domain and default value. More details can be consulted in the online documentation [27].
References
Adenso-Diaz, B., Laguna, M.: Fine-tuning of algorithms using fractional experimental design and local search. Oper. Res. 54(1), 99–114 (2006)
Ansotegui, C., Sellmann, M., Tierney, K.: A gender-based genetic algorithm for the automatic configuration of algorithms. In: Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming, pp. 142–157 (2009)
Ansótegui, C., Malitsky, Y., Samulowitz, H., Sellmann, M., Tierney, K.: Model-based genetic algorithms for algorithm configuration. In: IJCAI, pp. 733–739 (2015)
Audemard, G., Paulevé, L., Simon, L.: SAT heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 107–113. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51825-7_8
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: Proceedings of the 21st International Joint Conference on Artifical Intelligence, pp. 399–404. IJCAI 2009. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2009)
Bacchus, F., Berg, J., Järvisalo, M., Martins, R.: MaxSAT evaluation 2020: solver and benchmark descriptions (2020)
Balyo, T., contributors: The standard interface for incremental satisfiability solving. https://github.com/biotomas/ipasir (2014)
Biere, A.: PicoSAT essentials. J. Satisfiability, Boolean Model. Comput. 4(2–4), 75–97 (2008)
Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. Proc. SAT Competition 2013, 1 (2013)
Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51–53. University of Helsinki (2020)
Birattari, M., Yuan, Z., Balaprakash, P., Stützle, T.: F-Race and iterated F-Race: an overview. In: Empirical Methods for the Analysis of Optimization Algorithms, pp. 311–336 (2010)
Chollet, F., et al.: Keras (2015). https://github.com/fchollet/keras
COIN-OR Foundation: Computational infrastructure for operations research. https://www.coin-or.org/ (2016)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. J. Satisfiability, Boolean Model. Comput. 2(1–4), 1–26 (2006). IOS Press
Gamrath, G., et al.: The SCIP Optimization Suite 7.0. ZIB-Report 20–10, Zuse Institute Berlin, March 2020
Google: Google OR-Tools. https://developers.google.com/optimization (2021)
Gurobi Optimization: Gurobi. https://www.gurobi.com/ (2021)
Harris, C.R., et al.: Array programming with NumPy. Nature 585(7825), 357–362 (2020). https://doi.org/10.1038/s41586-020-2649-2
Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential Model-Based Optimization for General Algorithm Configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507–523. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25566-3_40
Hutter, F., Hoos, H., Leyton-Brown, K., Stuetzle, T.: ParamILS: an automatic algorithm configuration framework. JAIR 36, 267–306 (2009)
IBM: IBM ILOG CPLEX. https://www.ibm.com/products/ilog-cplex-optimization-studio (2021)
Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a Python toolkit for prototyping with SAT oracles. In: SAT, pp. 428–437 (2018)
Lauria, M., Elffers, J., Nordström, J., Vinyals, M.: CNFgen: a generator of crafted benchmarks. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 464–473. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_30
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisfiability, Boolean Model. Comput. 7(2–3), 59–64 (2010). IOS Press
Logic and Optimization Group: Optilog official documentation (2021). http://ulog.udl.cat/static/doc/optilog/html/index.html
Logic Optimization Group: PyPBLib: PBLib Python3 bindings. https://pypi.org/project/pypblib/ (2019)
McKinney, W.: Data Structures for Statistical Computing in Python. In: van der Walt, S., Millman, J. (eds.) In: Proceedings of the 9th Python in Science Conference, pp. 56–61 (2010). https://doi.org/10.25080/Majora-92bf1922-00a
Paszke, A., et al.: Pytorch: an imperative style, high-performance deep learning library. In: Wallach, H., Larochelle, H., Beygelzimer, A., d’ Alché-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32, pp. 8024–8035. Curran Associates, Inc. (2019)
Pedregosa, F., et al.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011)
Philipp, T., Steinke, P.: PBLib – a library for encoding pseudo-Boolean constraints into CNF. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 9–16. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_2
Van Rossum, G., Drake, F.L.: Python 3 Reference Manual. CreateSpace, Scotts Valley, CA (2009)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Ansótegui, C., Ojeda, J., Pacheco, A., Pon, J., Salvia, J.M., Torres, E. (2021). OptiLog: A Framework for SAT-based Systems. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-80223-3_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-80222-6
Online ISBN: 978-3-030-80223-3
eBook Packages: Computer ScienceComputer Science (R0)