HaifaSat is a Chaff-like SAT solver featuring a novel
decision heuristic (CMTF), a new resolution-based score system (RBS), an
advanced resolution scheme, clause minimization and effective preprocessing
using a Hyper-Resolution rule. For more details, refer to this short description.
HaifaSat was developed in Haifa/Technion by Roman Gershman under the supervision of Dr. Ofer Strichman.
We decided to call our solver HaifaSat following the tradition of authors of both BerkMin and JeruSat calling their solvers by the name of the cities where the authors live.
Run HaifaSat without parameters in order to see usage options. The most important parameters are –p (preprocessing level) and timeout.
HaifaSat uses preprocessing extensively. However, sometimes it takes much longer to solve the instance with preprocessing than without. Often it depends on the kind of problem it attempts to solve. We strongly advise to try the different levels of preprocessing with “-p preprocess_level” (preprocess level can be 0,1,2) in order to achieve maximal performance. It is also advisable to give a time-limit for the run-time so that HaifaSat can share its time resource wisely (for example, it won’t spend more than 10% of the time during the preprocessing even with the ‘–p 2’ switch).
HaifaSat is available for non-commercial and research use only. For any other use please contact us. If you are affiliated with a company, we will let you download HaifaSat for evaluation purposes for free, but only after contacting us directly.
HaifaSat1.0 including its sources can be downloaded from here.
An email with the download path will be sent to you after filling a short registration form.