Document Open Access Logo

OptiLog V2: Model, Solve, Tune and Run

Authors Josep Alòs , Carlos Ansótegui , Josep M. Salvia , Eduard Torres

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.25.pdf
  • Filesize: 0.8 MB
  • 16 pages

Document Identifiers

Author Details

Josep Alòs
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Carlos Ansótegui
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Josep M. Salvia
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Eduard Torres
  • Logic & Optimization Group (LOG), University of Lleida, Spain

Funding

Supported by Grant PID2019-109137GB-C21 funded by MCIN/AEI/10.13039/ 501100011033, PANDEMIES 2020 by Agencia de Gestio d’Ajuts Universitaris i de Recerca (AGAUR), Departament d’Empresa i Coneixement de la Generalitat de Catalunya, FONDO SUPERA COVID-19 funded by Crue-CSIC-SANTANDER, and the MICNN FPU fellowship (FPU18/02929).

Cite AsGet BibTex

Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: Model, Solve, Tune and Run. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.25

Abstract

We present an extension of the OptiLog Python framework. We fully redesign the solvers module to support the dynamic loading of incremental SAT solvers with support for external libraries. We introduce new modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for evaluating and parsing the results of applications, and we add support for constrained execution of blackbox programs and SAT-heritage integration. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Tool framework
  • Satisfiability
  • Modelling
  • Solving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Amir Aavani. Translating pseudo-boolean constraints into cnf. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011, pages 357-359, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  2. Carlos Ansótegui, Jesus Ojeda, António Pacheco, Josep Pon, Josep M. Salvia, and Eduard Torres. Optilog: A framework for sat-based systems. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 1-10. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_1.
  3. Carlos Ansótegui, Josep Pon, and Meinolf Sellmann. Boosting evolutionary algorithm configuration. Annals of Mathematics and Artificial Intelligence, 2021. URL: https://doi.org/10.1007/s10472-020-09726-y.
  4. Carlos Ansótegui, Josep Pon, Meinolf Sellmann, and Kevin Tierney. Pydgga: Distributed gga for automatic configuration. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 11-20, Cham, 2021. Springer International Publishing. Google Scholar
  5. Gilles Audemard, Loïc Paulevé, and Laurent Simon. SAT heritage: A community-driven effort for archiving, building and running more than thousand SAT solvers. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 107-113. Springer, 2020. Google Scholar
  6. Gilles Audemard, Loïc Paulevé, and Laurent Simon. Sat heritage: A community-driven effort for archiving, building and running more than thousand sat solvers. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020, pages 107-113, Cham, 2020. Springer International Publishing. Google Scholar
  7. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI'09, pages 399-404, San Francisco, CA, USA, 2009. Morgan Kaufmann Publishers Inc. Google Scholar
  8. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2021. Google Scholar
  9. Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2021. Google Scholar
  10. Armin Biere. Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2-4):75-97, 2008. Google Scholar
  11. Armin Biere. Lingeling, plingeling and treengeling entering the sat competition 2013. Proceedings of SAT competition, 2013:1, 2013. Google Scholar
  12. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  13. Francois Chollet et al. Keras, 2015. URL: https://github.com/fchollet/keras.
  14. COIN-OR Foundation. Computational infrastructure for operations research. https://www.coin-or.org/, 2016.
  15. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  16. dimacs.rutgers.edu. Dimacs cnf suggested format, 2021. URL: http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps.
  17. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, pages 502-518, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  18. Python Software Fundation. Python package index - pypi. URL: https://pypi.org/.
  19. Gerald Gamrath, Daniel Anderson, Ksenia Bestuzheva, Wei-Kun Chen, Leon Eifler, Maxime Gasse, Patrick Gemander, Ambros Gleixner, Leona Gottwald, Katrin Halbig, Gregor Hendel, Christopher Hojny, Thorsten Koch, Pierre Le Bodic, Stephen J. Maher, Frederic Matter, Matthias Miltenberger, Erik Mühmer, Benjamin Müller, Marc E. Pfetsch, Franziska Schlösser, Felipe Serrano, Yuji Shinano, Christine Tawfik, Stefan Vigerske, Fabian Wegscheider, Dieter Weninger, and Jakob Witzig. The SCIP Optimization Suite 7.0. ZIB-Report 20-10, Zuse Institute Berlin, March 2020. Google Scholar
  20. Marco Gario and Andrea Micheli. Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In SMT Workshop 2015, 2015. Google Scholar
  21. Google. Google OR-Tools. https://developers.google.com/optimization, 2021.
  22. T. Guns. Increasing modeling language convenience with a universal n-dimensional array, CPpy as python-embedded example. In The 18th workshop on Constraint Modelling and Reformulation at CP (ModRef 2019), 2019. URL: https://github.com/CPMpy/cpmpy.
  23. Gurobi Optimization. Gurobi. https://www.gurobi.com/, 2021.
  24. Charles R. Harris, K. Jarrod Millman, Stéfan J. van der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J. Smith, Robert Kern, Matti Picus, Stephan Hoyer, Marten H. van Kerkwijk, Matthew Brett, Allan Haldane, Jaime Fernández del Río, Mark Wiebe, Pearu Peterson, Pierre Gérard-Marchant, Kevin Sheppard, Tyler Reddy, Warren Weckesser, Hameer Abbasi, Christoph Gohlke, and Travis E. Oliphant. Array programming with NumPy. Nature, 585(7825):357-362, September 2020. URL: https://doi.org/10.1038/s41586-020-2649-2.
  25. IBM. IBM ILOG CPLEX. https://www.ibm.com/products/ilog-cplex-optimization-studio, 2021.
  26. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. Google Scholar
  27. Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. Cnfgen: A generator of crafted benchmarks. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 464-473. Springer, 2017. Google Scholar
  28. Marius Lindauer, Katharina Eggensperger, Matthias Feurer, André Biedenkapp, Difan Deng, Carolin Benjamins, Tim Ruhkopf, René Sass, and Frank Hutter. Smac3: A versatile bayesian optimization package for hyperparameter optimization, 2021. URL: http://arxiv.org/abs/2109.09831.
  29. Lluis Batlle i Rossell. Task spooler man page, 2021. URL: http://manpages.ubuntu.com/manpages/xenial/man1/tsp.1.html.
  30. Logic and Optimization Group. OptiLog C++ Interface for Python bindings. https://github.com/optilog/OptiLogFrameworkInterface. Accessed: 2022-02-26.
  31. Logic and Optimization Group. OptiLog official documentation, 2022. URL: http://ulog.udl.cat/static/doc/optilog/html/index.html.
  32. Logic Optimization Group. PyPBLib: PBLib Python3 bindings. https://pypi.org/project/pypblib/, 2018. Described in OptiLog [Carlos Ansótegui et al., 2021].
  33. W. Gentzsch (Sun Microsystems). Sun grid engine: Towards creating a compute power grid. In Proceedings of the 1st International Symposium on Cluster Computing and the Grid, CCGRID '01, page 35, USA, 2001. IEEE Computer Society. Google Scholar
  34. Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In In: Proc. of 13th International Conference on Principles and Practice of Constraint Programming, pages 529-543. Springer, 2007. Google Scholar
  35. Nikoli. Nikoli’s slitherlink webpage, 2021. URL: https://www.nikoli.co.jp/en/puzzles/slitherlink.html.
  36. The pandas development team. pandas-dev/pandas: Pandas, February 2020. URL: https://doi.org/10.5281/zenodo.3509134.
  37. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. dquotesingle Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32, pages 8024-8035. Curran Associates, Inc., 2019. Google Scholar
  38. F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011. Google Scholar
  39. Olivier Roussel. Controlling a solver execution: the runsolver tool. JSAT, 7:139-144, November 2011. URL: https://doi.org/10.3233/SAT190083.
  40. Guido Van Rossum and Fred L. Drake. Python 3 Reference Manual. CreateSpace, Scotts Valley, CA, 2009. Google Scholar
  41. Wes McKinney. Data Structures for Statistical Computing in Python. In Stéfan van der Walt and Jarrod Millman, editors, Proceedings of the 9th Python in Science Conference, pages 56-61, 2010. URL: https://doi.org/10.25080/Majora-92bf1922-00a.
  42. Takayuki Yato. On the np-completeness of the slither link puzzle. IPSJ SIGNotes ALgorithms, 74:25-32, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact