HaifaSAT is a new robust SAT solver.
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.
For related documentation, see: Roman Gershman, Ofer Strichman HaifaSat: a new robust SAT solver, Proc. of Haifa Verification Conference (HVC’05). LNCS vol. 3875, pages 76 – 89
Usage
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).
Download HaifaSat
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.
Click on this link to download HaifaSat1.0 including its sources
An email with the download path will be sent to you after filling a short registration form.
Contact Info
Dr. Ofer Strichman email: ofers@ie.technion.ac.il
Roman Gershman email : gershman@cs.technion.ac.il