Boolean Satisfiability (SAT)
Table of Contents
Boolean Satisfiability (SAT) #
Boolean Satisfiability is a fundamental problem in computer science with applications to formal verification and automated reasoning. Machine learning approaches are increasingly being applied to improve SAT solver heuristics.
Recent Literature #
Graph neural networks and boolean satisfiability. Arxiv, 2017. paper
Bünz, Benedikt, and Matthew Lamm.
Learning a SAT solver from single-bit supervision. Arxiv, 2018. paper, code
Selsam, Daniel, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill.
Machine learning-based restart policy for CDCL SAT solvers. SAT, 2018. paper
Liang, Jia Hui, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, and Vijay Ganesh.
Learning to solve circuit-SAT: An unsupervised differentiable approach. ICLR, 2019. paper, code
Amizadeh, Saeed, Sergiy Matusevych, and Markus Weimer.
Learning Local Search Heuristics for Boolean Satisfiability. NeurIPS, 2019. paper, code
Yolcu, Emre and Poczos, Barnabas
Improving SAT solver heuristics with graph networks and reinforcement learning. Arxiv, 2019. paper
Kurin, Vitaly, Saad Godil, Shimon Whiteson, and Bryan Catanzaro.
Graph neural reasoning may fail in certifying boolean unsatisfiability. Arxiv, 2019. paper
Chen, Ziliang, and Zhanfu Yang.
Guiding high-performance SAT solvers with unsat-core predictions. SAT, 2019. paper
Selsam, Daniel, and Nikolaj Bjørner.
G2SAT: Learning to Generate SAT Formulas. NeurIPS, 2019. paper, code
You, Jiaxuan, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec.
Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning. Arxiv, 2019. paper, code
Lederman, Gil, Markus N. Rabe, Edward A. Lee, and Sanjit A. Seshia.
Enhancing SAT solvers with glue variable predictions. Arxiv, 2020. paper
Han, Jesse Michael.
Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? NeurIPS, 2020. paper
Whiteson, Shimon.
Online Bayesian Moment Matching based SAT Solver Heuristics. ICML, 2020. paper, code
Duan, Haonan, Saeed Nejati, George Trimponias, Pascal Poupart, and Vijay Ganesh.
Learning Clause Deletion Heuristics with Reinforcement Learning. AITP, 2020. paper
Vaezipoor, Pashootan, Gil Lederman, Yuhuai Wu, Roger Grosse, and Fahiem Bacchus.
Classification of SAT problem instances by machine learning methods. CEUR, 2020. paper
Danisovszky, Márk, Zijian Győző Yang, and Gábor Kusper.
Predicting Propositional Satisfiability via End-to-End Learning. AAAI, 2020. paper
Cameron, Chris, Rex Chen, Jason Hartford, and Kevin Leyton-Brown.
Neural heuristics for SAT solving. Arxiv, 2020. paper
Jaszczur, Sebastian, Michał Łuszczyk, and Henryk Michalewski.
NLocalSAT: Boosting Local Search with Solution Prediction. Arxiv, 2020. paper, code
Zhang, Wenjie, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang.
Optimistic tree search strategies for black-box combinatorial optimization NeurIPS, 2022. paper
Malherbe, Cedric and Grosnit, Antoine and Tutunov, Rasul and Ammar, Haitham Bou and Wang, Jun
Goal-Aware Neural SAT Solver. IJCNN, 2022. paper
Ozolins, Emils, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics.
NeuroComb: Improving SAT Solving with Graph Neural Networks. Arxiv, 2022. paper
Wang, Wenxi, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikkulainen.
On the Performance of Deep Generative Models of Realistic SAT Instances. SAT, 2022. paper
Garzón, Iván, Pablo Mesejo, and Jesús Giráldez-Cru.
DeepSAT: An EDA-Driven Learning Framework for SAT. Arxiv, 2022. paper
Li, Min, Zhengyuan Shi, Qiuxia Lai, Sadaf Khan, and Qiang Xu.
SATformer: Transformers for SAT Solving. Arxiv, 2022. paper
Shi, Zhengyuan, Min Li, Sadaf Khan, Hui-Ling Zhen, Mingxuan Yuan, and Qiang Xu.
Augment with Care: Contrastive Learning for Combinatorial Problems. ICML, 2022. paper, code
Duan, Haonan, Pashootan Vaezipoor, Max B. Paulus, Yangjun Ruan and Chris J. Maddison
NSNet: A General Neural Probabilistic Framework for Satisfiability Problems NeurIPS, 2022. paper
Zhaoyu Li, Xujie Si
Neural Set Function Extensions: Learning with Discrete Functions in High Dimensions NeurIPS, 2022. paper
Nikolaos Karalias, Joshua Robinson, Andreas Loukas, Stefanie Jegelka
Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness ICLR, 2022. paper
Simon Geisler, Johanna Sommer, Jan Schuchardt, Aleksandar Bojchevski and Stephan Günnemann
Let the Flows Tell: Solving Graph Combinatorial Optimization Problems with GFlowNets NeurIPS, 2023. paper, code
Dinghuai Zhang, Hanjun Dai, Nikolay Malkin, Aaron Courville, Yoshua Bengio, Ling Pan
⭐HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline KDD, 2023. paper, code
Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Wanqian Luo, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Junchi Yan
Distributed Constrained Combinatorial Optimization leveraging Hypergraph Neural Networks Nature Machine Intelligence, 2024. paper, code
Nasimeh Heydaribeni, Xinrui Zhan, Ruisi Zhang, Tina Eliassi-Rad, Farinaz Koushanfar
Efficient Combinatorial Optimization via Heat Diffusion NeurIPS, 2024. paper
Hengyuan Ma, Wenlian Lu, Jianfeng Feng
⭐UniCO: On Unified Combinatorial Optimization via Problem Reduction to Matrix-Encoded General TSP ICLR, 2025. paper, code
Wenzheng Pan, Hao Xiong, Jiale Ma, Wentao Zhao, Yang Li, Junchi Yan