danielschemmel / drsat Goto Github PK

Clauses w/ exactly two literals can be stored and applied more efficiently than is currently done (both literals are watched) by adding specific data structures for them.

The Learning Rate Branching (LRB) heuristic, which did rather well in the 2017 SATCOMP has been implemented in the branch lrb. It is initialized with the same static heuristic, as is done on the master branch with the CHB heuristic.

Two major faults remain with the implementation:

• Instead of considering the whole conflict side, only the literals in the final (!) learned clause are given a boost.
• The original paper already mentions that the locality decay ("multiply with 0.95 when unused") can be batched, which is currently simply done brute force. This is not that much of a problem with the current test sets, as their number of variables is comparatively small.

Additionally, no fancy data structure is used to find the unassigned variable with the highest score. This must be kept this way for the moment to retain comparability with the CHB heuristic. Improvements can be implemented on master and then applied to the lrb branch when this should be of interest.

Performance

It would seem that for drsat the CHB heuristic results in better performance for SAT benchmarks, but that LRB wins for UNSAT benchmarks. Generally CHB seems to be a stronger choice at the moment.