[SMT-LIB] Solving dimacs instances with an SMT solvers

[Morgan Deters]

Hi Martin and Frank,

On Thu, Dec 4, 2014 at 3:50 PM, Martin Brain <martin.brain at cs.ox.ac.uk>
wrote:

> For specific solvers, you're best off contacting the authors' mailing
> lists rather than the one for the standard.  In the case of CVC4, 5
> seconds on symmetry breaking does seem somewhat high and I suspect
> they'd be interested in talking to you to work out why.
>

This is a known issue with SAT instances in CVC4.  The symmetry breaker is
spending a lot of time looking for symmetries that don't exist, so it's all
wasted effort.  You can disable the symmetry breaker
(--no-symmetry-breaker), or advise CVC4 that it's actually solving a SAT
instance rather than a QF_UF instance with "(set-info :cvc4-logic QF_SAT)".

I'll add to what Martin said also by saying that we have to disable some
optimizations in Minisat because they aren't generally favorable, or sound,
for SMT purposes.

Morgan
-- 
Morgan Deters
Senior Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/