UNSAT Solver Synthesis via Monte Carlo Forest Search

• URL: http://arxiv.org/abs/2211.12581v3
• Date: Sat, 13 Jul 2024 02:55:33 GMT
• Title: UNSAT Solver Synthesis via Monte Carlo Forest Search
• Authors: Chris Cameron, Jason Hartford, Taylor Lundy, Tuan Truong, Alan Milligan, Rex Chen, Kevin Leyton-Brown,
• Abstract summary: We introduce Monte Carlo Forest Search (MCFS), a class of reinforcement learning (RL) algorithms for learning policies in tree MDPs Examples of such problems include proving unsatisfiability of a SAT formula; counting the number of solutions of a satisfiable SAT formula. We dub Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies for solving the satisfiability (SAT) problem.
• Score: 10.754275929551593
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce Monte Carlo Forest Search (MCFS), a class of reinforcement learning (RL) algorithms for learning policies in {tree MDPs}, for which policy execution involves traversing an exponential-sized tree. Examples of such problems include proving unsatisfiability of a SAT formula; counting the number of solutions of a satisfiable SAT formula; and finding the optimal solution to a mixed-integer program. MCFS algorithms can be seen as extensions of Monte Carlo Tree Search (MCTS) to cases where, rather than finding a good path (solution) within a tree, the problem is to find a small tree within a forest of candidate trees. We instantiate and evaluate our ideas in an algorithm that we dub Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem, with the objective of achieving good average-case performance on a given distribution of unsatisfiable problem instances. Knuth Synthesis is the first RL approach to avoid the prohibitive costs of policy evaluations in an exponentially-sized tree, leveraging two key ideas: first, we estimate tree size by randomly sampling paths and measuring their lengths, drawing on an unbiased approximation due to Knuth (1975); second, we query a strong solver at a user-defined depth rather than learning a policy across the whole tree, to focus our policy search on early decisions that offer the greatest potential for reducing tree size. We matched or exceeded the performance of a strong baseline on three well-known SAT distributions, facing problems that were two orders of magnitude more challenging than those addressed in previous RL studies.

Related papers

• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• LiteSearch: Efficacious Tree Search for LLM [70.29796112457662]
  This study introduces a novel guided tree search algorithm with dynamic node selection and node-level exploration budget. Experiments conducted on the GSM8K and TabMWP datasets demonstrate that our approach enjoys significantly lower computational costs compared to baseline methods.
  arXiv  Detail & Related papers  (2024-06-29T05:14:04Z)
• Autonomous Tree-search Ability of Large Language Models [58.68735916408101]
  Large Language Models have excelled in remarkable reasoning capabilities with advanced prompting techniques. Recent works propose to utilize external programs to define search logic, such that LLMs can perform passive tree search to solve more challenging reasoning tasks. We propose a new concept called autonomous tree-search ability of LLM, which can automatically generate a response containing search trajectories for the correct answer.
  arXiv  Detail & Related papers  (2023-10-14T14:14:38Z)
• Structure-Unified M-Tree Coding Solver for MathWord Problem [57.825176412485504]
  In previous work, models designed by taking into account the properties of the binary tree structure of mathematical expressions at the output side have achieved better performance. In this paper, we propose the Structure-Unified M-Tree Coding Coding (S-UMCr), which applies a tree with any M branches (M-tree) to unify the output structures. Experimental results on the widely used MAWPS and Math23K datasets have demonstrated that SUMC-r not only outperforms several state-of-the-art models but also performs much better under low-resource conditions.
  arXiv  Detail & Related papers  (2022-10-22T12:20:36Z)
• Unbiased and Efficient Sampling of Dependency Trees [0.0]
  Most treebanks require that every valid dependency tree has a single edge coming out of the ROOT node. Zmigrod et al. have recently proposed algorithms for sampling with and without replacement from the single-root dependency tree distribution. We show that their fastest algorithm for sampling with replacement, Wilson-RC, is in fact biased.
  arXiv  Detail & Related papers  (2022-05-25T09:57:28Z)
• CITS: Coherent Ising Tree Search Algorithm Towards Solving Combinatorial Optimization Problems [0.0]
  This paper proposes a search algorithm by expanding search space from a Markov chain to a depth limited tree based on SA. At each iteration, the algorithm will select the best near-optimal solution within the feasible search space by exploring along the tree in the sense of look ahead' Our results show that above the primals SA and CIM, our high-level tree search strategy is able to provide solutions within fewer epochs for Ising formulated NP-optimization problems.
  arXiv  Detail & Related papers  (2022-03-09T10:07:26Z)
• What's Wrong with Deep Learning in Tree Search for Combinatorial Optimization [8.879790406465556]
  We present an open-source benchmark suite for the NP-hard Maximum Independent Set problem, in both its weighted and unweighted variants. We also conduct an in-depth analysis of the popular guided tree search algorithm by Li et al. [NeurIPS 2018], testing various configurations on small and large synthetic and real-world graphs. We show that the graph convolution network used in the tree search does not learn a meaningful representation of the solution structure, and can in fact be replaced by random values.
  arXiv  Detail & Related papers  (2022-01-25T17:37:34Z)
• Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
  This paper investigates the classical integer least-squares problem which estimates signals integer from linear models. The problem is NP-hard and often arises in diverse applications such as signal processing, bioinformatics, communications and machine learning. We propose a general hyper-accelerated tree search (HATS) algorithm by employing a deep neural network to estimate the optimal estimation for the underlying simplified memory-bounded A* algorithm.
  arXiv  Detail & Related papers  (2021-01-07T08:00:02Z)
• Exploring search space trees using an adapted version of Monte Carlo tree search for combinatorial optimization problems [0.6882042556551609]
  This approach makes use of a algorithm to explore the search space tree of a problem instance. The algorithm is based on Monte Carlo tree search, a popular algorithm in game playing that is used to explore game trees.
  arXiv  Detail & Related papers  (2020-10-22T08:33:58Z)
• Parameterizing Branch-and-Bound Search Trees to Learn Branching Policies [76.83991682238666]
  Branch and Bound (B&B) is the exact tree search method typically used to solve Mixed-Integer Linear Programming problems (MILPs) We propose a novel imitation learning framework, and introduce new input features and architectures to represent branching.
  arXiv  Detail & Related papers  (2020-02-12T17:43:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.