# General Method for Solving Four Types of SAT Problems

arXiv: https://arxiv.org/abs/2312.16423 · HTML: https://mlsanity.com/paper/2312.16423/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 41 references that are in the map.
- First posted on arXiv 27 Dec 2023.

## Builds on (most cited first, 8 of 8)

- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [A Game-Theoretic Approach for Improving Generalization Ability of TSP Solvers](https://mlsanity.com/paper/2110.15105/) (2021)
- [DeepSAT: An EDA-Driven Learning Framework for SAT](https://mlsanity.com/paper/2205.13745/) (2022)
- [Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?](https://mlsanity.com/paper/1909.11830/) (2019)
- [Learning Branching Heuristics for Propositional Model Counting](https://mlsanity.com/paper/2007.03204/) (2020)
- [Further Improvements for SAT in Terms of Formula Length](https://mlsanity.com/paper/2105.06131/) (2021)
- [NeuroPrim: An Attention-based Model for Solving NP-hard Spanning Tree Problems](https://mlsanity.com/paper/2210.12453/) (2022)

## Built on by (most cited first, 4 of 4)

- [Accessing GPT-4 level Mathematical Olympiad Solutions via Monte Carlo Tree Self-refine with LLaMa-3 8B](https://mlsanity.com/paper/2406.07394/) (2024)
- [MC-NEST: Enhancing Mathematical Reasoning in Large Language Models leveraging a Monte Carlo Self-Refine Tree](https://mlsanity.com/paper/2411.15645/) (2024)
- [MCTSr-Zero: Self-Reflective Psychological Counseling Dialogues Generation via Principles and Adaptive Exploration](https://mlsanity.com/paper/2505.23229/) (2025)
- [MCTS-SQL: Light-Weight LLMs can Master the Text-to-SQL through Monte Carlo Tree Search](https://mlsanity.com/paper/2501.16607/) (2025)

## Abstract (arXiv)

Existing methods provide varying algorithms for different types of Boolean satisfiability problems (SAT), lacking a general solution framework. Accordingly, this study proposes a unified framework DCSAT based on integer programming and reinforcement learning (RL) algorithm to solve different types of SAT problems such as MaxSAT, Weighted MaxSAT, PMS, WPMS. Specifically, we first construct a consolidated integer programming representation for four types of SAT problems by adjusting objective function coefficients. Secondly, we construct an appropriate reinforcement learning models based on the 0-1 integer programming for SAT problems. Based on the binary tree search structure, we apply the Monte Carlo tree search (MCTS) method on SAT problems. Finally, we prove that this method can find all optimal Boolean assignments based on Wiener-khinchin law of large Numbers. We experimentally verify that this paradigm can prune the unnecessary search space to find the optimal Boolean assignments for the problem. Furthermore, the proposed method can provide diverse labels for supervised learning methods for SAT problems.