Feature #546
closedCould CVC3 runtime be improved by decreasing precision?
0%
Description
I heard that some of SMT solvers (yices, for instance?) say that the formula is SAT if they can't prove otherwise after certain probe threshold or something. No wonder: proving unsat should be faster than proving sat.
In my experience, it takes an extremely large amount of time for CVC3 solver to prove satisfiability of a given SAT formula. Well, the time being not the biggest issue here, the memory consumed during processing of SAT formulæ is enormously big.
My question is, could CVC3 be tweaked, so it works in an "optimized" fashion? There are interesting options to try, such as "-resource
" and some "theoretical" tweaks, purpose of which I don't really understand.
To make an example: here are two formulæ, which differ only in one term. One is SAT, and the other is UNSAT. Processing of the SAT one takes 2Gb of memory and more runtime that of the other one. For example, Yices solver says "unknown" for the SAT formula; CVC3, on the other hand, proves that it's SAT by default.
Files