I tried writing a SAT solver with CDCL:https://gist.github.com/rrika/1f5756e4334c0269be20b811e7e64d04 …
This is so cool! 
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.pic.twitter.com/jlgPo6v9IX
-
-
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
-
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
- 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.