I tried writing a SAT solver with CDCL:https://gist.github.com/rrika/1f5756e4334c0269be20b811e7e64d04 …
-
with a few tweaks it terminates in ~50 minutes
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.
Can you update the gist with your changes? I'm curious to see what those tweaks are. The old version is now running for almost 4 hours here..
-
-
change "random.random() > 0.5" to "random.random() > 0.98"
-
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? ;)
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.