Applying UCT to Boolean Satisfiability

Abstract In this paper we perform a preliminary investigation into the application of sampling-based search algorithms to satisfiability testing of propositional formulas in Conjunctive Normal Form (CNF). In particular, we adapt the Upper Confidence bounds applied to Trees (UCT) algorithm [5] which has been successfully used in many game playing programs including MoGo, one of the strongest computer Go players [3].

Authors

• Alessandro Previti
• Raghuram Ramanujan
• Marco Schaerf
• Bart Selman

Keywords

No keywords are indexed for this paper.