Category: SMT
-
Checking Uniform-Like Samplers
Uniform sampling is pretty simple: there are a set of solutions to a set of equations, and I want you to give me N solutions uniformly at random. Say, I have a set of equations that only has the solutions x=1…6, and I ask you to give me solutions uniformly at random. In this case, […]
-
How Approximate Model Counting Works
Approximate model counting allows to count the number of solutions (or “models”) to propositional satisfiability problems. This problem seems trivial at first given a propositional solver that can find a single solution: find one solution, ban it, ask for another one, ban it, etc. until all solutions are counted. The issue is that sometimes, the […]
-
SMT Competition’14 and STP
The 2014 SMT competition‘s QF_BV divison is over (benchmark tarball here), and the results are (copied from here): Solver Errors Solved Not Solved CPU time (solved instances) Boolector 0 2361 127 138077.59 STP-CryptoMiniSat4 0 2283 205 190660.82 [MathSAT] 0 2199 289 262349.39 [Z3] 0 2180 308 214087.66 CVC4 0 2166 322 87954.62 4Simp 0 2121 […]