RSat is a complete Boolean satisfiability solver. RSat uses the 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

June 10, 2007: RSat 2.01 source code release.
June 10, 2007: RSat 2.00 source code release.