Feature #546: Could CVC3 runtime be improved by decreasing precision? - BLAST - Open-Source Projects

Actions

Copy link

Feature #546

closed

Could CVC3 runtime be improved by decreasing precision?

Added by Pavel Shved about 14 years ago. Updated about 13 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Mikhail Mandrykin

Category:

Target version:

2.6

Start date:

11/14/2010

Due date:

% Done:

Estimated time:

Published in build:

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

Download all files

smt_query_short (89.5 KB) smt_query_short	UNSAT smtlib formula	Pavel Shved, 11/14/2010 02:16 PM
smt_query_long (89.5 KB) smt_query_long	SAT smtlib formula	Pavel Shved, 11/14/2010 02:16 PM
cvc3config.png (48.3 KB) cvc3config.png	screenshot for comparison of CVC3 configurations	Pavel Shved, 12/03/2010 08:13 PM

Related issues 1 (0 open — 1 closed)

Actions

Copy link

Updated by Pavel Shved about 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.

Actions

Copy link

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.

Actions

Copy link

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.

Actions

Copy link

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.

Actions

Copy link

Updated by Alexey Khoroshilov almost 14 years ago

Should we give -quant-new option more usable name and push it to upstream?

Actions

Copy link

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...)

Actions

Copy link