Efficient Partial Order CDCL Using Assertion Level Choice Heuristics
This work addresses performance improvements in SAT solving for problems with high independence between decision levels, but it is incremental as it builds on prior PO-CDCL research.
The paper analyzes why Partial Order CDCL (PO-CDCL) is efficient for SAT solving, particularly focusing on how the partial order creates multiple assertion level candidates, and finds that a well-designed heuristic for selecting the assertion level can significantly improve performance on relevant benchmarks.
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.