I tried writing a SAT solver with CDCL:https://gist.github.com/rrika/1f5756e4334c0269be20b811e7e64d04 …
-
oh god, I didn't expect anyone would actually try to run it. it prints the entire assignment every line, so stdout gets quite crowded for any non-tiny instance
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.
Solving the uum8.smt2-stp212.cnf instance from SATCOMP2016 right now (should be unsat, MiniSAT can solve it in 11 seconds). If sat.py can solve it in less than one hour I would say that's a huge success. ;)pic.twitter.com/Yt9G2dalzP
-
-
with a few tweaks it terminates in ~50 minutes
-
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..
- Show replies
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.