[SMT-LIB] Suggestion for addition in the BitVec theory

[Andre Suelflow]

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
>