UNSAT Solver Synthesis via Monte Carlo Forest Search

Overview

• Introduces a new class of reinforcement learning (RL) algorithms called Monte Carlo Forest Search (MCFS) for learning policies in tree-structured Markov Decision Processes (tree MDPs)
• Focuses on problems where policy execution involves traversing an exponential-sized tree, such as proving unsatisfiability of a SAT formula, counting the number of solutions to a satisfiable SAT formula, or finding the optimal solution to a mixed-integer program
• Presents an instantiation of MCFS called Knuth Synthesis, which learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem with the goal of achieving good average-case performance on a given distribution of unsatisfiable instances

Plain English Explanation

The paper introduces a new approach called Monte Carlo Forest Search (MCFS) for solving complex problems that involve searching through an exponentially large tree of possible solutions. Examples of such problems include proving that a set of logical constraints (a SAT formula) has no solutions, counting the number of solutions to a satisfiable SAT formula, or finding the best solution to a mixed-integer programming problem.

The key idea behind MCFS is to view these tree-structured problems not as finding a single good path through the tree, but rather as finding a small "tree" (or set of solutions) within a larger "forest" of candidate trees. The researchers develop a specific MCFS algorithm called Knuth Synthesis, which learns how to make early decisions in the search process that can dramatically reduce the size of the overall search tree.

Knuth Synthesis does this by leveraging two key insights: First, it uses a clever statistical technique developed by Donald Knuth to estimate the size of the search tree by randomly sampling paths through it, rather than trying to fully explore the entire tree. Second, it focuses its learning on the early decisions in the search process, which have the greatest potential to reduce the overall tree size, rather than trying to learn a policy for the entire tree.

By using these techniques, Knuth Synthesis was able to match or exceed the performance of a strong baseline on several well-known SAT problem distributions, even on instances that were two orders of magnitude more challenging than those tackled in previous reinforcement learning studies.

Technical Explanation

The paper introduces a new class of reinforcement learning (RL) algorithms called Monte Carlo Forest Search (MCFS) for learning policies in tree-structured Markov Decision Processes (tree MDPs). In these problems, policy execution involves traversing an exponential-sized tree, which makes traditional RL approaches prohibitively expensive.

MCFS algorithms can be seen as an extension of Monte Carlo Tree Search (MCTS) to cases where the goal is not to find a good path (solution) within a tree, but rather to find a small tree within a forest of candidate trees. The researchers instantiate and evaluate their ideas in an algorithm called Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem.

Knuth Synthesis addresses the prohibitive costs of policy evaluations in an exponentially-sized tree using two key ideas: First, it estimates tree size by randomly sampling paths and measuring their lengths, drawing on an unbiased approximation technique due to Knuth (1975). Second, it queries a strong solver at a user-defined depth rather than learning a policy across the whole tree, focusing the policy search on early decisions that offer the greatest potential for reducing tree size.

The researchers show that Knuth Synthesis matched or exceeded the performance of a strong baseline on three well-known SAT distributions, tackling problems that were two orders of magnitude more challenging than those addressed in previous RL studies.

Critical Analysis

The paper presents a novel and promising approach to solving complex, tree-structured problems using reinforcement learning. The key insights of using statistical tree size estimation and focusing the policy search on early decisions are clever and well-justified.

However, the paper does not provide a comprehensive analysis of the limitations of the Knuth Synthesis algorithm. For example, it would be useful to understand how the performance of the algorithm scales with the size and complexity of the problem instances, or how sensitive it is to the choice of the user-defined depth at which the strong solver is queried.

Additionally, the paper does not compare Knuth Synthesis to other recent advances in RL for tree-structured problems, such as the work on proof-number based MCTS. Exploring these comparisons could provide valuable insights into the relative strengths and weaknesses of different approaches.

Overall, the paper makes a strong contribution by introducing MCFS and the Knuth Synthesis algorithm, but there is room for further research to fully understand the capabilities and limitations of this new class of RL algorithms.

Conclusion

This paper presents a novel class of reinforcement learning algorithms called Monte Carlo Forest Search (MCFS) for tackling complex, tree-structured problems. The researchers develop a specific MCFS algorithm called Knuth Synthesis, which learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem.

By leveraging statistical tree size estimation and focusing the policy search on early decisions, Knuth Synthesis was able to match or exceed the performance of a strong baseline on several well-known SAT problem distributions, even on instances that were significantly more challenging than those addressed in previous RL studies.

This work opens up new avenues for applying reinforcement learning to a broader class of problems that involve searching through exponentially large trees of possibilities, with potential applications in areas like theorem proving, program synthesis, and optimization. Further research is needed to fully understand the capabilities and limitations of MCFS algorithms, but this paper represents an important step forward in this promising direction.