Title: Finding the smallest tree in the forest: Monte Carlo Forest Search for UNSAT solving. Abstract: Monte Carlo Tree Search (MCTS) is an effective approach for finding low-cost paths through any large combinatorial space that can naturally be structured as a search tree. However, some combinatorial problems do not have a natural interpretation as searches for a good path. For example, solving a CSP can be represented as a path (assign variables sequentially and check the solution); however, proving that no solution exists (via existing methods) requires enumerating multiple paths to build out a “proof tree” demonstrating that every possible variable assignment leads to a conflict. Rather than finding a good path (solution) within a tree, the search problem becomes searching for a small proof tree within a forest of candidate trees. In this paper we develop Monte Carlo Forest Search (MCFS), an algorithm for finding small search trees. Our method leverages the benefits of the best MCTS approaches and further introduces two key ideas. First, we estimate tree size via the linear (i.e., path-based) and unbiased approximation from Knuth (1975). Second, we query a strong solver at a user-defined depth rather than learning a policy across the whole tree, in order to (1) reduce the variance of our tree-size estimates and (2) focus our policy search on early decisions, which offer the greatest potential for reducing tree size. We evaluated our approach on the Boolean satisfiability (SAT) problem, and found that it matched or improved performance over a strong baseline on two well-known distributions (\texttt{sgen}, \texttt{random}). Notably, we improved walltime by 9\% on \texttt{sgen} over the \texttt{kcnfs} solver and even further over the strongest UNSAT solver from the 2021 SAT competition.