References & Citations
Computer Science > Artificial Intelligence
Title: Improving SAT Solving with Graph Neural Networks
(Submitted on 26 Oct 2021 (this version), latest version 8 May 2024 (v7))
Abstract: Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Despite the remarkable success of modern SAT solvers, scalability still remains a challenge. Main stream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers by improving its variable branching heuristics through predictions generated by Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or has required frequent online accesses to substantial GPU resources. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroComb, which builds on two insights: (1) predictions of important variables and clauses can be combined with dynamic branching into a more effective hybrid branching strategy, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Implemented as an enhancement to the classic MiniSat solver, NeuroComb allowed it to solve 18.5% more problems on the recent SATCOMP-2020 competition problem set. NeuroComb is therefore a practical approach to improving SAT solving through modern machine learning.
Submission history
From: Wenxi Wang [view email][v1] Tue, 26 Oct 2021 22:08:22 GMT (111kb,D)
[v2] Thu, 28 Oct 2021 02:57:28 GMT (111kb,D)
[v3] Thu, 9 Jun 2022 19:13:56 GMT (119kb,D)
[v4] Wed, 4 Oct 2023 01:31:48 GMT (128kb,D)
[v5] Fri, 27 Oct 2023 16:30:44 GMT (128kb,D)
[v6] Tue, 28 Nov 2023 21:05:18 GMT (168kb,D)
[v7] Wed, 8 May 2024 18:23:10 GMT (176kb,D)
Link back to: arXiv, form interface, contact.