An SMT solver stayed alive for 111 hours without running out of memory?
-
-
-
For hard CircuitSAT-type ABV problems the solver memory usage usually doesn't increase that much after the first couple of minutes. (Maybe max double after the first hour, then double again for the remainder of the solver time.)
End of conversation
New conversation -
-
-
Is it possible to run this kind of solver in multiple threads or is that an unsolvable problem? (I have no clue how this works under the hood at all)
-
Some solvers support multithreading, but scaling isn't linear. Often multithreading is simply achieved via portfolio methods. To scale well with parallelism a problem must be in NC. SAT is usually used for NP problems. So naturally it tends to be a hard to parallelize problem.
End of conversation
New conversation -
-
-
Better than: (111 hours) Status: FAILED
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Fighting against solver... "prove that I'm wrong motherf*...."pic.twitter.com/XvvuWQPHhS
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Which brings up the main issue I have with formal method. How can you rely on such a verification method when you can't predict how long your runs are going to take? For all you know, this could have ended after 1100 hours, not 110. Do you have any progress indication of hints?
-
For example, you can run it with different shorter bounds, fit a low-order polynomial to the curve, and extrapolate to obtain a (usually pretty good) estimate for how long it will take.
- 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.