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 is developed by the UCLA Automated Reasoning Group.
News and Announcements
Version 2.02 beta released. This version has an interface for incremental SAT and specifying partial order of variables.
Recursive-style interface for exhaustive search is added to the source code of RSat 2.01.
the source code and executables of RSat versions 2.01 and 2.00 have been released.