About HyperSAT

HyperSAT is a research SAT solver written to experiment with B-cubing search space pruning (see Publications for more details). In spite of being experimental, it won 3rd place at the 2005 Satisfiability Testing competition in the satisfiable-crafted instances category.

Key Ideas

The key idea behind B-cubing is that one can learn much more from failures (i.e., conflicts) during the search than the current techniques learn. However, the problem is how to efficiently store and use such a large amount of information. Further, B-cubing works in a completely different way that is difficult to integrate with the modern DPLL solvers. B-cubes are similar to decision trees and compactly encode learned cubes, which are then used to prune search space in the future. My work barely scratches the surface of what I think could be done with B-cubing. For instance, I expect it could be effective for solving Quantified Boolean Formulas (QBF), and there is more work to be done on the SAT front as well.

Availability

HyperSAT is not actively developed. Due to low-level bit hacks it is limited to 32-bit machines. The solver has been extensively tested. However, unless you are interested in the guts of B-cubing or HyperSAT performs particularly well on your instances, I’d recommend that you use the Spear, which inherits some features from HyperSAT and is incomparably faster.

Download

Release 1.7 source (Mar 2005) [tar.bz2].