Tech stack for numerical solutions

[ramanshah]

Markus suggested a couple SAT solvers:

• SATO ("full solver" - not sure what that means) https://homepage.divms.uiowa.edu/~hzhang/sato/
• WalkSAT ("local solver" - not sure what that means) https://en.wikipedia.org/wiki/WalkSAT

Via Twitter:

https://twitter.com/MarkusTriska/status/1259130230066864134

"The Prolog code to generate SAT instances is available from: https://metalevel.at/sgp/ You can use Scryer Prolog to run it: https://github.com/mthom/scryer-prolog Once an instance is generated (in DIMACS format), any SAT solver can be used to search for a satisfiable assignment."

https://twitter.com/MarkusTriska/status/1263923809566023681

One small tip: When you apply a SAT solver with local search, remove the symmetry constraints from the model. They are good for complete solvers (which apply backtracking to traverse the search space), but they reduce the number of (symmetric) solutions, and make it hard for LS!

[ramanshah]

I've tried one run of the Prolog code on the local host. It's very slow. I'll likely need to use AWS to avoid killing/tying up my everyday computer.

[ramanshah]

One more:

https://twitter.com/MarkusTriska/status/1263928735214043137

I have had good results with SATO (a complete solver) and Walksat (based on local search). In http://satgolf.pl, you can remove the symmetry breaking constraints from DIMACS by commenting out lines 198--212 (they are marked with the comment "symmetry breaking constraints").