← 研踪 PaperTrailarXiv:2610.41290 · v3
SAT-ACT: Learning CDCL Branching from Outcome-Derived Action Preferences
首次提交 2026-10-30 13:52
版本更新 2026-11-03 22:07
雷达观测 2026-11-04 23:39
摘要
Learning-based approaches have increasingly been explored for SAT solving, with particular attention to improving branching decisions in conflict-driven clause learning (CDCL) solvers. These approaches derive branching guidance either from static structural properties of SAT formulas or from dynamic signals obtained through solver feedback and execution traces. However, these forms of supervision provide limited evidence about state-dependent branching effects, while different outcome measures may favor different branching choices. To address these limitations, we propose SAT-ACT, an outcome-derived learning framework for CDCL branching. We design three complementary outcome comparison criteria to extract action preferences from independent branching action rollouts initiated at the same solver state. The criteria identify preferences supported by the outcomes and leave comparisons unresolved when the evidence is insufficient or conflicting, instead of forcing an ordering using a predefined scalar metric. A state-conditioned network learns branching priorities from the extracted preferences and uses them to guide CDCL search directly without online action rollouts. We further introduce non-dominated heuristic action supervision, which retains the solver-selected action as a training target only when it remains non-dominated under these preferences. Solver-level experiments show that SAT-ACT consistently reduces CDCL search costs on three SAT families and improves PAR-2 on the SAT Competition benchmarks.
作者备注：this work is currently in progress
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-03 22:07 · 最新观测版本
SAT-ACT: Learning CDCL Branching from Outcome-Derived Action Preferences
Learning-based approaches have increasingly been explored for SAT solving, with particular attention to improving branching decisions in conflict-driven clause learning (CDCL) solvers. These approaches derive branching guidance either from static structural properties of SAT formulas or from dynamic signals obtained through solver feedback and execution traces. However, these forms of supervision provide limited evidence about state-dependent branching effects, while different outcome measures may favor different branching choices. To address these limitations, we propose SAT-ACT, an outcome-derived learning framework for CDCL branching. We design three complementary outcome comparison criteria to extract action preferences from independent branching action rollouts initiated at the same solver state. The criteria identify preferences supported by the outcomes and leave comparisons unresolved when the evidence is insufficient or conflicting, instead of forcing an ordering using a predefined scalar metric. A state-conditioned network learns branching priorities from the extracted preferences and uses them to guide CDCL search directly without online action rollouts. We further introduce non-dominated heuristic action supervision, which retains the solver-selected action as a training target only when it remains non-dominated under these preferences. Solver-level experiments show that SAT-ACT consistently reduces CDCL search costs on three SAT families and improves PAR-2 on the SAT Competition benchmarks.
查看此版本解读 →查看此版本原文 ↗