walksat

[jwaldmann]

(no action required, this is just a note)

I built walksat from source https://gitlab.com/HenryKautz/Walksat (by one of the original authors, see https://henrykautz.com/walksat/index.html) and applied it to CNFs built by ersatz. I was quite shocked to observer that walksat often finds assignments that leave just one clause unsatisfied (if I'm reading their trace correctly). Does that mean that (given some more time) it would solve the formula completely?

No! Assume we have do xs <- replicate _ exists; assert $ some_function_of xs. This gets Tseitin-transformed. Then for any assignment to xs, auxiliary literals can be assigned correctly (computing the value of the formula). Just the very top clause (asserting that the value is True) remains unsatisfied.

To counter that, one must do all unit propagations (from the top) first. I don't think walksat does this. But cadical seems to (cadical -O10 -P10 -L10000 ... with L for local search, P for preprocessing, eliminating variables while possibly adding clauses). But it does not seem to help (kissat seems faster).

So, all is well. Except, maybe, my experiments suggest that ersatz could provide ways to

• set cmd line options for solver
• show stderr of running solver
• run several solvers in parallel

I will write separate issues.