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

[Martin Brain]

On Thu, 2014-12-04 at 15:13 -0500, Frank Imeson wrote:
> Hey guys,
> 
> I have an open question on Stackoverflow
> <https://stackoverflow.com/questions/27298133/solving-dimacs-instances-with-an-smt-solver-seems-slow-smt2-format>
> about
> the speed of smt solvers. Thanks ahead of time If you have time to look at
> it.

Reposting the question for everyone on the list:

0 down vote favorite 

I'm converting my problem to SMT and
I have noticed that the SMT solvers
(MathSat5 and CVC4) are slow when
solving sat instances. My suspension
is that there is something in my
translation that is making it go
slow.

I'm attaching a sample cnf instance
and the smt2 translation for
reference and below I'm providing
solver times (excluding the
translation time) for a larger
instance to compare MathSat5, CVC4
and MiniSat.

Solver                Solver Time (s)
-------------------------------------
MiniSat               0.028062 s
MathSat5              2.629702 s
CVC4                  7.488870 s

So does anyone have an idea why
these times are drastically
different? PS. cvc4 says it spent
5.862 seconds in: theory uf
symmetry_breaker

Sample cnf:
-------------------------------------
p cnf 20  91 
4 -18 19 0
...
4 -16 -5 0


Sample smt2:
-------------------------------------
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)

(declare-fun v1 () Bool)
...
(declare-fun x20 () Bool)

(assert (or v4 (not x18) x19))
...
(assert (or v4 (not v16) (not v5)))
(check-sat)
(get-value ( v1 ... x20))
(exit)

Thanks




There are a number of things that could be causing this.  Firstly
SMT-LIB is a lot more verbose than DIMACS, so some of this will be
parsing overhead.  Next there is building and preprocessing the SMT-LIB
terms and then converting them to clauses to feed into the internal SAT
solver.  Finally there will be overhead in the actual solver search
algorithm.  Thus it is reasonable to expect an SMT solver to be slower
than a SAT solver, because, they do more.  For problems this simple, the
overhead is likely to dominate.  For harder problems it is (hopefully)
fairly minimal.

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.

HTH

Cheers,
 - Martin