RLSAT: Satisfiability using Reinforcement Learning

Introduction

RLSAT is a DPLL solver for the satisfiability (SAT) problem enhanced with machine learning capabilities. In particular, RLSAT uses experience from previous executions to learn how to select appropriate branching heuristics from a library of predefined heuristics with the goal of minimizing the total size of the search tree, and therefore the total execution time. RLSAT also applies to the #SAT problem where the goal is to count the number of satisfying assignments instead of just finding one of them.

Authors

Michail G. Lagoudakis
Ph.D. Candidate, Department of Computer Science, Duke University
mgl @ cs . duke . edu

Michael L. Littman
Assistant Professor, Department of Computer Science, Rutgers University
mlittman @ cs . rutgers . edu

Papers

Here is a paper that describes RLSAT:

Learning to Select Branching Rules in the DPLL Procedure for Satisfiability
Michail G. Lagoudakis and Michael L. Littman
Electronic Notes in Discrete Mathematics (ENDM), Vol. 9, Elsevier
LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001)
Boston, MA, June 14-15, 2001 (ENDM Volume 9 online)


RLSAT Code Distribution

RLSAT is written in C and accepts standard CNF inputs.
Distribution and use of this code is subject to the following agreement:
This Program is provided by Duke University and the authors as a service to the research community. It is provided without cost or restrictions, except for the User's acknowledgement that the Program is provided on an "As Is" basis and User understands that Duke University and the authors make no express or implied warranty of any kind.  Duke University and the authors specifically disclaim any implied warranty or merchantability or fitness for a particular purpose, and make no representations or warranties that the Program will not infringe the intellectual property rights of others. The User agrees to indemnify and hold harmless Duke University and the authors from and against any and all liability arising out of User's use of the Program.

Download Directory (Please read the instructions.README file)

Email Michail at  mgl @ cs . duke . edu  if you encounter any problems.