Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

So, here's a thing. Years ago I remember Matti presenting a graph of an experiment he did. Each time the solver pruned the clause database, he recorded it and tracked how many were repeated. Turns out after a while 80-90% of learnt clauses were duplicates.

Every proof of completeness for CDCL variants I have seen has been hand-wavy as anything. So... 1. I am not sure that "will eventually return an answer" is true. 2. Once you take learnt clause pruning into account, I think CDCL may be more than exponential.

As long as the number of conflicts between restarts grows unbounded, you don't need to keep learned clauses at all to get completeness. Not sure what's currently used but with luby restarts that takes care of 1. Still growing way too slow to really help with 2 though.

Nevermind the part about 2, I think it grows fast enough to still give you an exponential worst case bound, but I haven't checked that carefully. In any case no issue with completeness though.

No offense meant but this is what I mean about handwaving. Yes, one can construct a theoretical solver that doesn't repeat itself and is exponential worst-case but that is not what actual solvers do.

This applies to my SAT solver and I think it also applies to minisat

Also not sure if you saw this, as I screwed up the threading:https://twitter.com/jix_/status/1256931027211165696 …

The point is, that without restarts or with unbounded time between restarts, the trail + asserting clauses is enough state to ensure progress. AFAICT that applies to all modern SAT solvers unless they have a fixed upper bound on time between restarts (which I don't know).