[SMT-LIB] Suggestion for addition in the BitVec theory
Rémi Delmas
Remi.Delmas at onera.fr
Wed Apr 21 03:40:21 EDT 2010
Hi Andre,
Your paper reports that picosat is faster on cardinality constraints
expressed as an arithmetic sum of base 2 bitvectors, which from other
sources should be the less efficient encoding wrt unit propagation.
Yet, a while back I observed as well that picosat was much more
efficient than, say minisat, on problems obtained by bitblasting integer
arithmetic problems.
An examination of picosat's code led me to believe this performance was
due to the way the decision heuristic was initialised by default,
assigning weights to the variables in ascending order wrt their integer
ID in the CNF. This meant that variables with consecutive IDs were more
likely to be split on not to far apart in sequence by the decision
heuristic.
Often, when bitblasting an instance, consecutive bits of a same
bitvector will end up having consecutive integer IDs, and being perhaps
more strongly related in the instance. This could be why it could make
sense to split on them in sequence.
It would be nice to analyse conflicts / propagation statistics from the
solvers, and to tweak the decision heuritsic initialisation to see if my
assumption holds for other solvers.
/Rémi
Andre Suelflow wrote:
> Hi Duraid, Clark, Rémi,
>
> just a side note: We did some experimental studies on cardinality
> constraints using the bit-vector theory. From our experiments, we can
> confirm the strong dependency of the performance of SMT solvers on the
> chosen encoding of the cardinality constraint. We have observed
> performance differences of up-to a factor of 2500 in run-time (or even
> memory outs) just by replacing the cardinality constraint. (for details
> see
> http://www.informatik.uni-bremen.de/agra/doc/konf/2009-ismvl-smtcardinalityconstraints.pdf)
>
> Thus, having a built-in cardinality constraint would help to reduce this
> dependency. The generation of benchmarks would not be a big deal for us
> (debugging instances, SMT-LIB 1.2).
>
>
> Andre
>
>
> On 03/26/10 10:39, Rémi Delmas wrote:
>> Hi everyone!
>>
>> I'm glad to have some feedback on this proposal.
>>
>> I've done bibliographic research on the topic and found these papers to
>> be quite interesting. The authors propose an arc coherent and polynomial
>> size encoding of pseudo boolean constraints (cardinality is just a
>> special case of this).
>>
>> http://boolvar.net/static/pagespro/pdf/obybor-sat-2009.pdf
>>
>> http://boolvar.net/static/pagespro/pdf/jsat-2006.pdf
>>
>> I've done some experiments on my own, trying different encodings of
>> cardinality constraints, and my observations match the authors claims,
>> i.e. the proposed encoding is the one that lends itself best to unit
>> propagation with MathSat, Z3, yices, etc.
>>
>> Unfortunately, I will not be able to provide the community with
>> benchmarks right now, as I manually bitblasted my examples to
>> propositional logic, but I can work on it for later.
>>
>> /Rémi
>>
>> Duraid Madina wrote:
>>
>>> Hi Clark, Remi:
>>>
>>> I could certainly provide a few such benchmarks, up to now I have
>>> been getting away with hacks like (in CVC3):
>>>
>>> B0, B1, B2, B3 : BITVECTOR(16);
>>> ASSERT(B0 = 0hex5555);
>>> ASSERT(B1 = 0hex3333);
>>> ASSERT(B2 = 0hex0f0f);
>>> ASSERT(B3 = 0hex00ff);
>>> popcount : BITVECTOR(16) -> BITVECTOR(16) =
>>> LET C1 = LAMBDA(x: BITVECTOR(16)): BVPLUS(16, (x>> 1)&B0[15:0],
>>> x&B0[15:0]) IN
>>> LET C2 = LAMBDA(C1: BITVECTOR(16)): BVPLUS(16, (C1>> 2)&B1[15:0],
>>> C1&B1[15:0]) IN
>>> LET C3 = LAMBDA(C2: BITVECTOR(16)): BVPLUS(16, (C2>> 4)&B2[15:0],
>>> C2&B2[15:0]) IN
>>> LET C4 = LAMBDA(C3: BITVECTOR(16)): BVPLUS(16, (C3>> 8)&B3[15:0],
>>> C3&B3[15:0]) IN
>>> LAMBDA(x: BITVECTOR(16)) : C4(C3(C2(C1(x))));
>>>
>>> I would be thrilled if a tool did something more intelligent than
>>> just blast away bitcount predicates doing something similar to the above, so
>>> I agree with Remi that it might be a good idea to add such predicates. There
>>> are a number of different ways of formulating the Hamming weight and I have
>>> seen tools perform differently on benchmarks depending on the formulation
>>> used. So if bitcount gets added to the SMT-LIB format, at the very least one
>>> would hope that implementers would treat it in a way appropriate for their
>>> particular tools.
>>>
>>> Duraid
>>>
>>>
>>> On Thu, Mar 25, 2010 at 10:13:31PM -0400, Clark Barrett wrote:
>>>
>>>> Remi,
>>>>
>>>> I'm not sure if anyone ever responded to you about this.
>>>>
>>>> Our usual policy is that if someone can provide benchmarks using an
>>>> additional operator like the one you mention, then we will strongly consider
>>>> adding it to the standard.
>>>>
>>>> Would you be able to produce such benchmarks?
>>>>
>>>> -Clark
>>>>
>>>>
>>>> On Mon, Feb 15, 2010 at 11:10 AM, R?mi Delmas<Remi.Delmas at onera.fr> wrote:
>>>>
>>>>
>>>>> Hello,
>>>>>
>>>>> it would be very handy if the BitVec theory offered bitcount predicates
>>>>> that would allow to express cardinality constraints on the number of
>>>>> true bits in a bitvector.
>>>>>
>>>>> (bvbitcounteq Int BitVec[m] Bool) :
>>>>>
>>>>> true iff the number of true bits in the second argument is equal to the
>>>>> first argument
>>>>>
>>>>>
>>>>> (bvbitcountlt Int BitVec[m] Bool) :
>>>>>
>>>>> true iff the number of true bits in the second argument is strictly less
>>>>> than the first argument
>>>>>
>>>>>
>>>>> we could have polymorphic variants of them for ease of use :
>>>>>
>>>>> (bvbitcounteq BitVec[n] BitVec[m] BitVec[1]) :
>>>>>
>>>>> true iff the number of true bits in the second argument is equal to the
>>>>> first argument (seen as an integer in 2's complement).
>>>>>
>>>>> (bvbitcountlt BitVec[n] BitVec[m] BitVec[1]) :
>>>>>
>>>>> true iff the number of true bits in the second argument is strictly less
>>>>> than the first argument (seen as an integer in 2's complement).
>>>>>
>>>>> More proposed variants :
>>>>> (bvbitcounteq[i] BitVec[m] BitVec[1])
>>>>> (bvbitcountlt[i] BitVec[m] BitVec[1])
>>>>> (bvbitcounteq[i] BitVec[m] Bool)
>>>>> (bvbitcountlt[i] BitVec[m] Bool)
>>>>>
>>>>>
>>>>>
>>>>> Best regards,
>>>>>
>>>>> R?mi Delmas
>>>>> _______________________________________________
>>>>> SMT-LIB mailing list
>>>>> SMT-LIB at cs.nyu.edu
>>>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>>>>
>>>>>
>>>>>
>>>> _______________________________________________
>>>> SMT-LIB mailing list
>>>> SMT-LIB at cs.nyu.edu
>>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>>>
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
More information about the SMT-LIB
mailing list