Efficient Partial Order CDCL Using Assertion Level Choice Heuristics

TL;DR

This paper analyzes the efficiency of Partial Order CDCL in SAT solving, highlighting how heuristics for assertion level choice can significantly improve performance on complex benchmarks.

Contribution

It introduces and evaluates heuristics for assertion level selection in PO-CDCL, demonstrating their impact on solver efficiency.

Findings

Heuristics for assertion level choice greatly influence PO-CDCL performance.

Carefully designed heuristics can significantly improve solving times.

PO-CDCL outperforms traditional methods on certain benchmark problems.

Abstract

We previously designed Partial Order Conflict Driven Clause Learning (PO-CDCL), a variation of the satisfiability solving CDCL algorithm with a partial order on decision levels, and showed that it can speed up the solving on problems with a high independence between decision levels. In this paper, we more thoroughly analyze the reasons of the efficiency of PO-CDCL. Of particular importance is that the partial order introduces several candidates for the assertion level. By evaluating different heuristics for this choice, we show that the assertion level selection has an important impact on solving and that a carefully designed heuristic can significantly improve performances on relevant benchmarks.