Solving Huge Instances with Intel(R) SAT Solver

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.

Authors

• Alexander Nadel

Keywords

• SAT
• CDCL