RSat is a complete Boolean satisfiability solver with an exhaustive search interface for applications such as model counting and knowledge compilation. RSat uses a phase selection heuristic that is oriented toward reducing work repetition and a frequent restart policy. For a complete description of RSat please see the list of papers.

RSat won gold medals from the SAT'07 competition in the industrial category. The previous version of RSat also won the third place in SAT-Race 2006.

RSat is developed by the UCLA Automated Reasoning Group.

News and Announcements

November 9, 2007:

Version 2.02 beta released. This version has an interface for incremental SAT and specifying partial order of variables.

June 25, 2007:

Recursive-style interface for exhaustive search is added to the source code of RSat 2.01.


June 10, 2007:

the source code and executables of RSat versions 2.01 and 2.00 have been released.