2026-07-23T04:32:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16682 2024-03-06T10:58:02Z ddc:004 open_access

Introducing Intel(R) SAT Solver Nadel, Alexander SAT CDCL MaxSAT We introduce Intel(R) SAT Solver (IntelSAT) - a new open-source CDCL SAT solver, written from scratch. IntelSAT is optimized for applications which generate many mostly satisfiable incremental SAT queries. We apply the following Incremental Lazy Backtracking (ILB) principle: in-between incremental 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander Nadel 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.8 urn:nbn:de:0030-drops-166825 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.8 eng https://creativecommons.org/licenses/by/4.0/legalcode