Alexander Nadel: Introducing Intel® SAT solver

Tuesday February 28, 2023 Introducing Intel® SAT solver (Alexander Nadel, Intel & Technion) We introduce Intel® SAT Solver (IntelSAT) — an open-source CDCL SAT solver, recently written from scratch and released at SAT 2022 conference. IntelSAT is optimized for applications which generate many mostly satisfiable incremental SAT queries. The first part of our talk will include a brief self-contained introduction into CDCL SAT solving, required to understand the algorithms in IntelSAT, followed by a high-level review of these algorithms and experimental results. In the second part of our talk, we will discuss more gory details along the following lines. IntelSAT applies the following Incremental Lazy Backtracking (ILB) principle: in-between incremental SAT queries, backtrack only when necessary and to the highest possible decision level. ILB is enabled by a novel reimplication procedure, which can reimply an assigned literal at a lower level without backtracking. Reimplication also helped us to restore the following two properties, lost in the modern solvers with the introduction of chronological backtracking: no assigned literal can be implied at a lower level, conflict analysis always starts with a clause falsified at the lowest possible level. In addition, we apply some new heuristics. Integrating IntelSAT into the MaxSAT solver TT-Open-WBO-Inc resulted in a significant performance boost on incomplete unweighted MaxSAT Evaluation benchmarks and improved the state-of-the-art in anytime unweighted MaxSAT solving. For more information about the MIAO seminars, please visit http://www.jakobnordstrom.se/miao-seminars/.