Project

General

Profile

Actions

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
Category:
-
Target version:
Start date:
11/14/2010
Due date:
% Done:

0%

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

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 open1 closed)

Blocks BLAST - Bug #544: CVC3 is too slow and greedy in memory consumptionClosedPavel Shved11/14/2010

Actions
Actions

Also available in: Atom PDF