What is current best practice for highest performance on incremental QF_BV?

[Geoff Langdale]

I've recently ported a project I'm working on to use Boolector as a alternate back-end. I'd like to know how to achieve the best performance for my workload.

At the moment the vast majority of my processing is done on quantifier free bit vectors only (QF_BV) and I generally need incremental use (doing a program synthesis problem with the usual "get one or more counter examples, add it/them to the model" flow - "CEGIS").

I tried two setups with Boolector - one was grabbing the SMTCOMP19 branch, and the other was default "master" branch. 

The SMTCOMP19 branch was sensationally faster than master (about 11x faster on my problem), but is still somewhat slower than Yices.

Is the SMTCOMP19 branch the best starting point if I want to work on tuning my system with Boolector? Is there a planned release schedule?

Geoff.

[Mathias Preiner]

Hi Geoff,

The smtcomp19 branch is a good starting point. We are currently in the
process of cleaning up the branch and merge it back to master for a new
release, which will hopefully happen until end of November.

It would be great if you could share the benchmarks where Boolector
performs worse than Yices. What you can try is to enable option
BTOR_OPT_NONDESTR_SUBST on the smtcomp19 branch. Let me know if it makes
any difference.

Cheers,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Geoff Langdale]

HI Mathias,

Thanks for the quick response! Good to hear there is a new release coming. 

I tried the BTOR_OPT_NONDESTR_SUBST option and it provided a small improvement (5-10%, it seems).

I need to do some work to make it possible to generate SMTLIB2 examples from my code. At the moment I have rolled my own layer in front of some native APIs (Yices, Z3 and now Boolector). I had thought this would be good for performance as I have tons of not very long-running solves to do (typically averaging around 1ms). In retrospect this is feeling like a dumb decision - it has 'premature optimization' written all over it as I can admit I didn't bother to measure how long SMTLIB2 takes to parse. 

I'm not at a point where I can/should share the source code itself, but if I built SMTLIB2 export it would make a lot of sense.

Regards,

Geoff.

> an email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.

[Mathias Preiner]

Hi Geoff,

What SAT solver do you use with Boolector? I would recommend using
CaDiCaL if you are not already using it.

Cheers,
Mathias

> > an email to bool...@googlegroups.com <javascript:>
> > <mailto:bool...@googlegroups.com <javascript:>>.

> > To view this discussion on the web visit
> >
> https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com>
>
> >

> <https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/boolector/a7bc597b-5207-4527-9807-366cbe5f4c1d%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send

> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/boolector/38e27574-4054-4ad6-9323-0bacc5586d90%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/38e27574-4054-4ad6-9323-0bacc5586d90%40googlegroups.com?utm_medium=email&utm_source=footer>.