Document Open Access Logo

Parallelizing a SAT-Based Product Configurator

Authors Nils Merlin Ullmann, Tomáš Balyo, Michael Klein

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.55.pdf
  • Filesize: 0.62 MB
  • 18 pages

Document Identifiers

Author Details

Nils Merlin Ullmann
  • CAS Software AG, Karlsruhe, Germany
Tomáš Balyo
  • CAS Software AG, Karlsruhe, Germany
Michael Klein
  • CAS Software AG, Karlsruhe, Germany

Cite AsGet BibTex

Nils Merlin Ullmann, Tomáš Balyo, and Michael Klein. Parallelizing a SAT-Based Product Configurator. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 55:1-55:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.55

Abstract

This paper presents how state-of-the-art parallel algorithms designed to solve the Satisfiability (SAT) problem can be applied in the domain of product configuration. During an interactive configuration process, a user selects features step-by-step to find a suitable configuration that fulfills his desires and the set of product constraints. A configuration system can be used to guide the user through the process by validating the selections and providing feedback. Each validation of a user selection is formulated as a SAT problem. Furthermore, an optimization problem is identified to find solutions with the minimum amount of changes compared to the previous configuration. Another additional constraint is deterministic computation, which is not trivial to achieve in well performing parallel SAT solvers. In the paper we propose five new deterministic parallel algorithms and experimentally compare them. Experiments show that reasonable speedups are achieved by using multiple threads over the sequential counterpart.

Subject Classification

ACM Subject Classification
  • Applied computing → E-commerce infrastructure
Keywords
  • Configuration
  • Satisfiability
  • Parallel

Metrics

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

Related Versions

References

  1. Henrik Reif Andersen, Tarik Hadzic, and David Pisinger. Interactive cost configuration over decision diagrams. Journal of Artificial Intelligence Research, 37:99-139, 2010. Google Scholar
  2. Tomáš Balyo, Peter Sanders, and Carsten Sinz. Hordesat: A massively parallel portfolio sat solver. In International Conference on Theory and Applications of Satisfiability Testing, pages 156-172, 2015. Google Scholar
  3. Don Batory. Feature models, grammars, and propositional formulas. In International Conference on Software Product Lines, pages 7-20, 2005. Google Scholar
  4. Armin Biere. Lingeling, plingeling and treengeling entering the sat competition 2013. Proceedings of SAT competition, 2013:1, 2013. Google Scholar
  5. Csaba Biro, Gergely Kovasznai, Armin Biere, Gábor Kusper, and Gábor Geda. Cube-and-conquer approach for sat solving on grids. In Annales Mathematicae et Informaticae, pages 9-21, 2013. Google Scholar
  6. CAS Software AG. Cas configurator merlin, 2020. URL: https://www.cas.de/en/products/configurator/cas-configurator-merlin.html.
  7. Wahid Chrabakh and Richard Wolski. Gridsat: A chaff-based distributed sat solver for the grid. In SC'03: Proceedings of the 2003 ACM/IEEE conference on Supercomputing, page 37, 2003. Google Scholar
  8. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962. Google Scholar
  9. Edsger W. Dijkstra. A note on two problems in connexion with graphs. Numerische mathematik, 1(1):269-271, 1959. Google Scholar
  10. Matthew Evett, James Hendler, Ambuj Mahanti, and Dana Nau. Pra*: Massively parallel heuristic search. Journal of Parallel and Distributed Computing, 25(2):133-143, 1995. Google Scholar
  11. Andreas Falkner, Alexander Felfernig, and Albert Haag. Recommendation technologies for configurable products. Ai Magazine, 32(3):99-108, 2011. Google Scholar
  12. Alexander Felfernig, Lothar Hotz, Claire Bagley, and Juha Tiihonen. Knowledge-based configuration: From research to business cases. Newnes, 2014. Google Scholar
  13. Eugene C. Freuder, Chavalit Likitvivatanavong, and Richard J. Wallace. Explanation and implication for configuration problems. In IJCAI 2001 workshop on configuration, pages 31-37, 2001. Google Scholar
  14. Zhaohui Fu and Sharad Malik. Solving the minimum-cost satisfiability problem using sat based branch-and-bound search. In Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, pages 852-859, 2006. Google Scholar
  15. Begum Genc, Mohamed Siala, Barry O'Sullivan, and Gilles Simonin. Finding robust solutions to stable marriage. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 631-637. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/88.
  16. Tarik Hadzic, Sathiamoorthy Subbarayan, Rune M. Jensen, Henrik R. Andersen, Jesper Møller, and Henrik Hulgaard. Fast backtrack-free product configuration using a precompiled solution space representation. small, 10(1):3, 2004. Google Scholar
  17. Youssef Hamadi, Said Jabbour, Cédric Piette, and Lakhdar Sais. Deterministic parallel dpll. Journal on Satisfiability, Boolean Modeling and Computation, 7(4):127-132, 2011. Google Scholar
  18. Youssef Hamadi, Said Jabbour, and Lakhdar Sais. Manysat: A parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation, 6(4):245-262, 2010. Google Scholar
  19. Peter E. Hart, Nils J. Nilsson, and Bertram Raphael. A formal basis for the heuristic determination of minimum cost paths. IEEE Transactions on Systems Science and Cybernetics, 4(2):100-107, 1968. Google Scholar
  20. Emmanuel Hebrard, Brahim Hnich, and Toby Walsh. Robust solutions for constraint satisfaction and optimization. In Ramón López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pages 186-190. IOS Press, 2004. Google Scholar
  21. Emmanuel Hebrard, Brahim Hnich, and Toby Walsh. Super solutions in constraint programming. In Jean-Charles Régin and Michel Rueher, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, First International Conference, CPAIOR 2004, Nice, France, April 20-22, 2004, Proceedings, volume 3011 of Lecture Notes in Computer Science, pages 157-172. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24664-0_11.
  22. Marijn Heule and Hans van Maaren. Look-ahead based sat solvers. Handbook of satisfiability, 185:155-184, 2009. Google Scholar
  23. Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding cdcl sat solvers by lookaheads. In Haifa Verification Conference, pages 50-65, 2011. Google Scholar
  24. KEKIB IRANI and YI-FON SHIH. Parallel a* and ao* algorithms: An optimality criterion and performance evaluation. In 1986 International Conference on Parallel Processing, University Park, PA, pages 274-277, 1986. Google Scholar
  25. Mikolas Janota. Do sat solvers make good configurators? In SPLC (2), pages 191-195, 2008. Google Scholar
  26. Mikoláš Janota. SAT solving in interactive configuration. PhD thesis, Citeseer, 2010. Google Scholar
  27. Mikoláš Janota, Goetz Botterweck, Radu Grigore, and Joao Marques-Silva. How to complete an interactive configuration process? In International Conference on Current Trends in Theory and Practice of Computer Science, pages 528-539, 2010. Google Scholar
  28. Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence, 1(1-4):167-187, 1990. Google Scholar
  29. Yuu Jinnai and Alex Fukunaga. Abstract zobrist hashing: An efficient work distribution method for parallel best-first search. In Thirtieth AAAI Conference on Artificial Intelligence, 2016. Google Scholar
  30. Bernard Jurkowiak, Chu Min Li, and Gil Utard. A parallelization scheme based on work stealing for a class of sat solvers. Journal of Automated Reasoning, 34(1):73-101, 2005. Google Scholar
  31. Yoshikazu Kobayashi, Akihiro Kishimoto, and Osamu Watanabe. Evaluations of hash distributed a* in optimal sequence alignment. In Twenty-Second International Joint Conference on Artificial Intelligence, 2011. Google Scholar
  32. Richard E. Korf. Depth-first iterative-deepening: An optimal admissible tree search. Artificial intelligence, 27(1):97-109, 1985. Google Scholar
  33. Vipin Kumar, K. Ramesh, and V. Nageshwara Rao. Parallel best-first search of state-space graphs: A summary of results. In AAAI, volume 88, pages 122-127, 1988. Google Scholar
  34. Matthew Lewis, Tobias Schubert, and Bernd Becker. Multithreaded sat solving. In Asia and South Pacific Design Automation Conference, 2007, pages 926-931, Piscataway, NJ, 2007. IEEE Operations Center. URL: https://doi.org/10.1109/ASPDAC.2007.358108.
  35. Chu Min Li and Felip Manya. Maxsat, hard and soft constraints. Handbook of satisfiability, 185:613-631, 2009. Google Scholar
  36. Xiao Yu Li. Optimization algorithms for the minimum-cost satisfiability problem. PhD thesis, North Carolina State University, 2004. URL: https://repository.lib.ncsu.edu/handle/1840.16/4594.
  37. Inês Lynce, Vasco M. Manquinho, and Ruben Martins. Parallel maximum satisfiability. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 61-99. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_3.
  38. Joao P. Marques-Silva and Karem A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. Google Scholar
  39. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530-535, 2001. Google Scholar
  40. Hidetomo Nabeshima and Katsumi Inoue. Reproducible efficient parallel sat solving. In International Conference on Theory and Applications of Satisfiability Testing, pages 123-138. Springer, 2020. Google Scholar
  41. Mike Phillips, Maxim Likhachev, and Sven Koenig. Pa* se: Parallel a* for slow expansions. In Twenty-Fourth International Conference on Automated Planning and Scheduling, 2014. Google Scholar
  42. Ted K. Ralphs, Yuji Shinano, Timo Berthold, and Thorsten Koch. Parallel solvers for mixed integer linear optimization. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 283-336. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_8.
  43. Daniel Sabin and Rainer Weigel. Product configuration frameworks-a survey. IEEE Intelligent Systems and their applications, 13(4):42-49, 1998. Google Scholar
  44. Tobias Schubert, Matthew Lewis, and Bernd Becker. Pamiraxt: Parallel sat solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation, 6(4):203-222, 2010. Google Scholar
  45. Carsten Sinz, Wolfgang Blochinger, and Wolfgang Küchlin. Pasat - parallel sat-checking with lemma exchange: Implementation and applications. Electronic Notes in Discrete Mathematics, 9:205-216, 2001. Google Scholar
  46. Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Detection of inconsistencies in complex product configuration data using extended propositional sat-checking. In FLAIRS conference, pages 645-649, 2001. Google Scholar
  47. Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Formal methods for the validation of automotive product configuration data. Ai Edam, 17(1):75-97, 2003. Google Scholar
  48. Nils Merlin Ullmann. Parallel sat-solving for product configuration. Master’s thesis, KIT, Karslruhe, Germany, 2021. URL: https://doi.org/10.5281/zenodo.5154040.
  49. Hantao Zhang, Maria Paola Bonacina, and Jieh Hsiang. Psato: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation, 21(4-6):543-560, 1996. 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