Machine Learning for SAT: Restricted Heuristics and New Graph Representations

TL;DR

This paper proposes a hybrid approach combining machine learning and classical heuristics for SAT solving, improving efficiency by making initial ML-guided steps before switching to traditional methods, and introduces a modified Graph-Q-SAT for domain-specific SAT problems.

Contribution

It introduces a hybrid ML-heuristic strategy for SAT solving and a modified Graph-Q-SAT tailored for SAT problems from other domains, validated on various instances.

Findings

Hybrid approach reduces total solving steps and runtime.

Initial ML-guided steps improve cold start performance.

Modified Graph-Q-SAT effectively handles domain-specific SAT problems.

Abstract

Boolean satisfiability (SAT) is a fundamental NP-complete problem with many applications, including automated planning and scheduling. To solve large instances, SAT solvers have to rely on heuristics, e.g., choosing a branching variable in DPLL and CDCL solvers. Such heuristics can be improved with machine learning (ML) models; they can reduce the number of steps but usually hinder the running time because useful models are relatively large and slow. We suggest the strategy of making a few initial steps with a trained ML model and then releasing control to classical heuristics; this simplifies cold start for SAT solving and can decrease both the number of steps and overall runtime, but requires a separate decision of when to release control to the solver. Moreover, we introduce a modification of Graph-Q-SAT tailored to SAT problems converted from other domains, e.g., open shop scheduling problems. We validate the feasibility of our approach with random and industrial SAT problems.