Scholarlink

Modern SAT solvers are based on a paradigm which adopts Conjunctive Normal Form (CNF) format and based on the conflict driven clause learning (CDCL) approach. This paradigm has dominated SAT solving for two decades and is very mature. We believe that for the future of SAT solving, it is beneficial to explore more paradigms that might lead to further improvements in certain aspects. This paper reviews three recent works that represent paradigm shifts to CNF-based CDCL. Specifically, we introduce circuit-based SAT solver, FPGA-based solver, and SAT solver that evolves via Large Language Models. The experiments show very promising results which indicate that such paradigm shifts to the mainstream method deserve more attention.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

More Paradigms of SAT Solvers: Circuit-SAT, FPGA-Based SAT, LLM-Based SAT

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Shaowei Cai

摘要

Modern SAT solvers are based on a paradigm which adopts Conjunctive Normal Form (CNF) format and based on the conflict driven clause learning (CDCL) approach. This paradigm has dominated SAT solving for two decades and is very mature. We believe that for the future of SAT solving, it is beneficial to explore more paradigms that might lead to further improvements in certain aspects. This paper reviews three recent works that represent paradigm shifts to CNF-based CDCL. Specifically, we introduce circuit-based SAT solver, FPGA-based solver, and SAT solver that evolves via Large Language Models. The experiments show very promising results which indicate that such paradigm shifts to the mainstream method deserve more attention.