Prioritized Unit Propagation with Periodic Resetting is (Almost) All You Need for Random SAT Solving

TL;DR

This paper introduces a simple yet effective SAT solving algorithm based on prioritized unit propagation with periodic resetting, demonstrating competitive performance on hard random SAT instances in major competitions.

Contribution

It presents a novel, straightforward algorithm that significantly improves solving random SAT problems, challenging more complex methods and providing insights into problem hardness.

Findings

Ranks second in 2017 and 2018 SAT competitions

Outperforms many existing methods on hard random instances

Suggests simplicity can be highly effective in SAT solving

Abstract

We propose prioritized unit propagation with periodic resetting, which is a simple but surprisingly effective algorithm for solving random SAT instances that are meant to be hard. In particular, an evaluation on the Random Track of the 2017 and 2018 SAT competitions shows that a basic prototype of this simple idea already ranks at second place in both years. We share this observation in the hope that it helps the SAT community better understand the hardness of random instances used in competitions and inspire other interesting ideas on SAT solving.