License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2021.55
URN: urn:nbn:de:0030-drops-153464
Go to the corresponding LIPIcs Volume Portal

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

Parallelizing a SAT-Based Product Configurator

LIPIcs-CP-2021-55.pdf (0.6 MB)


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.

BibTeX - Entry

  author =	{Ullmann, Nils Merlin and Balyo, Tom\'{a}\v{s} and Klein, Michael},
  title =	{{Parallelizing a SAT-Based Product Configurator}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{55:1--55:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-153464},
  doi =		{10.4230/LIPIcs.CP.2021.55},
  annote =	{Keywords: Configuration, Satisfiability, Parallel}

Keywords: Configuration, Satisfiability, Parallel
Collection: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Issue Date: 2021
Date of publication: 15.10.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI