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.SAT.2023.17
URN: urn:nbn:de:0030-drops-184790
Go to the corresponding LIPIcs Volume Portal

Nadel, Alexander

Solving Huge Instances with Intel(R) SAT Solver

LIPIcs-SAT-2023-17.pdf (0.8 MB)


We introduce a new release of our SAT solver Intelregistered SAT Solver. The new release, called IS23, is targeted to solve huge instances beyond the capacity of other solvers. IS23 can use 64-bit clause-indices and store clauses compressedly using bit-arrays, where each literal is normally allocated fewer than 32 bits. As a preliminary result, we show that only IS23 can handle a gigantic trivially satisfiable instance with over 8.5 billion clauses. Then, we demonstrate that IS23 enables a significant improvement in the capacity of our industrial tool for cell placement in physical design, since only IS23 can solve placement instances with up to 4.3 billion clauses. Finally, we show that IS23 is substantially more efficient than other solvers for finding many (10⁶) placements on instances with up to 170 million clauses. We use the latter application to demonstrate that variable succession, that is, the order in which the variables are provided to the solver, might have a significant impact on IS23’s performance, thereby providing a new dimension to SAT encoding considerations.

BibTeX - Entry

  author =	{Nadel, Alexander},
  title =	{{Solving Huge Instances with Intel(R) SAT Solver}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{17:1--17:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-184790},
  doi =		{10.4230/LIPIcs.SAT.2023.17},
  annote =	{Keywords: SAT, CDCL}

Keywords: SAT, CDCL
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023
Supplementary Material: Software (Source Code): archived at:

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