{"ID":2863923,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.25411","arxiv_id":"2509.25411","title":"Boolean Satisfiability via Imitation Learning","abstract":"We propose ImitSAT, a branching policy for conflict-driven clause learning (CDCL) solvers based on imitation learning for the Boolean satisfiability problem (SAT). Unlike previous methods that predict instance-level signals to improve CDCL branching indirectly, or rely on reinforcement learning and insufficient CDCL information to enhance branching, ImitSAT learns from expert KeyTrace that collapses a full run into the sequence of surviving decisions. Replaying a KeyTrace on the same instance is nearly conflict-free, providing dense decision-level supervision and directly reducing propagations -- the dominant contributor to wall-clock time. This prefix-conditioned supervision enables ImitSAT to reproduce high-quality branches without exploration, yielding faster convergence, stable training, and seamless integration into CDCL. Extensive experiments demonstrate that ImitSAT reduces propagation counts and runtime, outperforming state-of-the-art learned approaches. We released the source code and trained model at https://github.com/zewei-Zhang/ImitSAT","short_abstract":"We propose ImitSAT, a branching policy for conflict-driven clause learning (CDCL) solvers based on imitation learning for the Boolean satisfiability problem (SAT). Unlike previous methods that predict instance-level signals to improve CDCL branching indirectly, or rely on reinforcement learning and insufficient CDCL in...","url_abs":"https://arxiv.org/abs/2509.25411","url_pdf":"https://arxiv.org/pdf/2509.25411v2","authors":"[\"Zewei Zhang\",\"Huan Liu\",\"Yuanhao Yu\",\"Jun Chen\",\"Xiangyu Xu\"]","published":"2025-09-29T19:09:37Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.LG\"]","methods":"[\"Reinforcement Learning\",\"LoRA\"]","has_code":false,"code_links":[{"ID":609084,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_id":2863923,"paper_url":"https://arxiv.org/abs/2509.25411","paper_title":"Boolean Satisfiability via Imitation Learning","repo_url":"https://github.com/zewei-Zhang/ImitSAT","is_official":false,"mentioned_in_paper":false,"mentioned_in_github":true,"github_stars":0}]}