I tried writing a SAT solver with CDCL:https://gist.github.com/rrika/1f5756e4334c0269be20b811e7e64d04 …
-
change "random.random() > 0.5" to "random.random() > 0.98"
However, I can't use it on any nontrivial DIMACS inputs because of deep recursion. Adding something like "sys.setrecursionlimit(1000000)" seems to fix it.
44 minutes. That's only 2^8 times slower than MiniSAT. I'd say that's pretty amazing! Re-running without the print statements now.. (srsy? tabs for indenting python? ;)