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
Updated by Pavel Shved almost 14 years ago
For example, on my machine, limiting -resource
helps. Here's the output:
$ src/bin/cvc3 -lang smtlib <smt_query_short -resource 5 unsat $ src/bin/cvc3 -lang smtlib <smt_query_long -resource 5 unknown
It doesn't go over 1Gb of memory with this limit. So it seems to be an interesting matter to experiment with.
Updated by Mikhail Mandrykin almost 14 years ago
An option -quant-complete-inst may be used. It disables complete instantiation heuristic, i.e. instantiating every forall quantified subexpression with all possible terms. This significantly decreases the number of resulting instances and thus time and memory consumption (with this option cvc3 gives "unknown" on smt_query_long example in ~15 seconds). Also an option -quant-max-IL n (where n is maximal instantiation level allowed) may help. It puts a limit on the number of repeated instantiations with ground terms that have appeared as a result of some previous instantiations. The "depth" of such repeated instantiation is called instantiation level. There is a soft time limit option -stimeout ms (in tenth of seconds). "Currently, when the limit is reached, cvc3 tries to quickly terminate, probably with the status unknown", cvc3 documentation says.
Updated by Mikhail Mandrykin almost 14 years ago
On small regression tests cvc3 performed worse with only -quant-complete-inst option. It consumed much more time and memory and even got out of 2GB limit on some tests. Maybe some other instantiation heuristic was used... So I added -quant-new option disabling all instantiation heuristics except naive. Then test results restored.
Updated by Pavel Shved almost 14 years ago
- File cvc3config.png cvc3config.png added
- Category set to BLAST
- Status changed from New to Resolved
So we checked the following options:
(1) cvc3 -lang smtlib -quant-complete-inst -quant-new -stimeout 10 (2) cvc3 -lang smtlib # default (4) cvc3 -lang smtlib -quant-complete-inst -quant-new -quant-max-IL 1 (5) cvc3 -lang smtlib -quant-complete-inst -quant-new (7) yices
(other runs on the picture are not for consideration for various reasons)
We learned that (4) and (5) don't have precision degradations, and provide better runtime at the same time. (1) was neither faster nor as precise as the default run. It seems that CVC3 configuration (4) approached configuration of another solver, Yices, and we can consider it acceptable.
This configuration is pushed to master as commit commit:7aa6b9c3.
Updated by Alexey Khoroshilov almost 14 years ago
Should we give -quant-new option more usable name and push it to upstream?
Updated by Pavel Shved almost 14 years ago
Alexey Khoroshilov wrote:
Should we give -quant-new option more usable name and push it to upstream?
This is and option from upstream. Michael was talking about "adding" it to the list of options to launch experiments on, not about "adding it to the tool". :-)
(somehow the comment haven't got posted...)
Updated by Pavel Shved over 13 years ago
- Status changed from Resolved to Closed
- Assignee set to Mikhail Mandrykin
since we've still had no problem with this, closing.
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)