OptiLog: a framework for SAT-based systems. (English) Zbl 07495561

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 1-10 (2021).
Summary: 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.
For the entire collection see [Zbl 1482.68030].


68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI


[1] Adenso-Diaz, B.; Laguna, M., Fine-tuning of algorithms using fractional experimental design and local search, Oper. Res., 54, 1, 99-114 (2006) · Zbl 1167.90654
[2] 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)
[3] Ansótegui, C., Malitsky, Y., Samulowitz, H., Sellmann, M., Tierney, K.: Model-based genetic algorithms for algorithm configuration. In: IJCAI, pp. 733-739 (2015)
[4] Audemard, G.; Paulevé, L.; Simon, L.; Pulina, L.; Seidl, M., SAT heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers, Theory and Applications of Satisfiability Testing - SAT 2020, 107-113 (2020), Cham: Springer, Cham · Zbl 07331015
[5] 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)
[6] Bacchus, F., Berg, J., Järvisalo, M., Martins, R.: MaxSAT evaluation 2020: solver and benchmark descriptions (2020)
[7] Balyo, T., contributors: The standard interface for incremental satisfiability solving. https://github.com/biotomas/ipasir (2014)
[8] Biere, A., PicoSAT essentials, J. Satisfiability, Boolean Model. Comput., 4, 2-4, 75-97 (2008) · Zbl 1159.68403
[9] Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. Proc. SAT Competition 2013, 1 (2013)
[10] 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)
[11] 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) · Zbl 1204.68280
[12] Chollet, F., et al.: Keras (2015). https://github.com/fchollet/keras
[13] COIN-OR Foundation: Computational infrastructure for operations research. https://www.coin-or.org/ (2016)
[14] de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg
[15] Eén, N.; Sörensson, N.; Giunchiglia, E.; Tacchella, A., An extensible SAT-solver, Theory and Applications of Satisfiability Testing, 502-518 (2004), Heidelberg: Springer, Heidelberg · Zbl 1204.68191
[16] 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 · Zbl 1116.68083
[17] Gamrath, G., et al.: The SCIP Optimization Suite 7.0. ZIB-Report 20-10, Zuse Institute Berlin, March 2020
[18] Google: Google OR-Tools. https://developers.google.com/optimization (2021)
[19] Gurobi Optimization: Gurobi. https://www.gurobi.com/ (2021)
[20] Harris, CR, Array programming with NumPy, Nature, 585, 7825, 357-362 (2020)
[21] Hutter, F.; Hoos, HH; Leyton-Brown, K.; Coello, CAC, Sequential Model-Based Optimization for General Algorithm Configuration, Learning and Intelligent Optimization, 507-523 (2011), Heidelberg: Springer, Heidelberg
[22] Hutter, F.; Hoos, H.; Leyton-Brown, K.; Stuetzle, T., ParamILS: an automatic algorithm configuration framework, JAIR, 36, 267-306 (2009) · Zbl 1192.68831
[23] IBM: IBM ILOG CPLEX. https://www.ibm.com/products/ilog-cplex-optimization-studio (2021)
[24] Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a Python toolkit for prototyping with SAT oracles. In: SAT, pp. 428-437 (2018) · Zbl 1484.68215
[25] Lauria, M.; Elffers, J.; Nordström, J.; Vinyals, M.; Gaspers, S.; Walsh, T., CNFgen: a generator of crafted benchmarks, Theory and Applications of Satisfiability Testing - SAT 2017, 464-473 (2017), Cham: Springer, Cham · Zbl 06807244
[26] Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisfiability, Boolean Model. Comput. 7(2-3), 59-64 (2010). IOS Press
[27] Logic and Optimization Group: Optilog official documentation (2021). http://ulog.udl.cat/static/doc/optilog/html/index.html
[28] Logic Optimization Group: PyPBLib: PBLib Python3 bindings. https://pypi.org/project/pypblib/ (2019)
[29] 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). doi:10.25080/Majora-92bf1922-00a
[30] 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)
[31] Pedregosa, F., Scikit-learn: machine learning in Python, J. Mach. Learn. Res., 12, 2825-2830 (2011) · Zbl 1280.68189
[32] Philipp, T.; Steinke, P.; Heule, M.; Weaver, S., PBLib – a library for encoding pseudo-Boolean constraints into CNF, Theory and Applications of Satisfiability Testing - SAT 2015, 9-16 (2015), Cham: Springer, Cham · Zbl 1471.68261
[33] Van Rossum, G., Drake, F.L.: Python 3 Reference Manual. CreateSpace, Scotts Valley, CA (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.