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.

翻译：布尔可满足性（SAT）是一个基础的NP完全问题，广泛应用于自动规划与调度等领域。为求解大规模实例，SAT求解器必须依赖启发式策略（例如DPLL和CDCL求解器中的分支变量选择）。这类启发式可通过机器学习模型进行改进，虽能减少求解步骤数，但通常因实用模型规模较大且速度较慢而影响运行时间。我们提出一种策略：先利用训练好的机器学习模型执行若干初始步骤，随后将控制权交还给经典启发式。该方法可简化SAT求解的热启动过程，并在减少步骤数的同时降低总运行时间，但需要独立决策何时将控制权释放给求解器。此外，我们引入Graph-Q-SAT的改进版本，专为从其他领域（如开放式车间调度问题）转换而来的SAT问题设计。我们通过随机SAT问题与工业SAT问题验证了该方法的可行性。