I've made some changes to my twitter profile and my twitter avatar. You are smart, you'll figure it out. ;-) 
-
Congratulations and thanks for sharing! Happy to hear your SAT solver for identity has returned a solution. Like others, I'm also curious about the naming now. Will it still be yosys or is it yosis now?
Yeah, you know how SAT solvers are. They always return a solution. But sometimes it may take 20+ years. :D
-
-
So, here's a thing. Years ago I remember Matti presenting a graph of an experiment he did. Each time the solver pruned the clause database, he recorded it and tracked how many were repeated. Turns out after a while 80-90% of learnt clauses were duplicates.
-
Every proof of completeness for CDCL variants I have seen has been hand-wavy as anything. So... 1. I am not sure that "will eventually return an answer" is true. 2. Once you take learnt clause pruning into account, I think CDCL may be more than exponential.
- 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.