[gecode-users] unsigned 32bit representation, additions

[Jean-Noël Monette]

Hi Serg,

Kellen Dye implemented a Bit-Vector domain implementation for Gecode for 
his master thesis. You can find his thesis at

http://uu.diva-portal.org/smash/record.jsf?pid=diva2%3A761927&dswid=8488

and the source-code at

https://github.com/kellen/bitvector-masters

He did not implement the addition constraint but the paper on which he 
based his implementation gives an algorithm for the addition:

L. D. Michel and P. Van Hentenryck. *Constraint* *Satisfaction* *over* 
*Bit-Vectors*. http://link.springer.com/chapter/10.1007/978-3-642-33558-7_39

Best,

Jean-Noël


On 2015-03-11 10:17, Christian Schulte wrote:
>
> Hi Serg,
>
> For the time being there is not much that you can do about this. And 
> Gecode cannot be easily recompiled using unsigned ints (or 64 bit 
> integers for that matter). I think some people have been experimenting 
> with arbitrary precision integers as well as bit vectors but I do not 
> know how far that got. Anybody?
>
> Best
>
> Christian
>
> --
>
> Christian Schulte, www.gecode.org/~schulte
>
> Professor of Computer Science, KTH, cschulte at kth.se 
> <mailto:cschulte at kth.se>
>
> Expert Researcher, SICS, cschulte at sics.se <mailto:cschulte at sics.se>
>
> *From:*users-bounces at gecode.org [mailto:users-bounces at gecode.org] *On 
> Behalf Of *Serg Buslovsky
> *Sent:* Wednesday, March 11, 2015 6:54 AM
> *To:* users at gecode.org
> *Subject:* [gecode-users] unsigned 32bit representation, additions
>
> Hi Group,
>
> I'm thinking about the ways of implementing 32bit unsigned integer 
> representations in gecode model.
>
> So I have 32 BoolVar's per uint32 representation, which are used to 
> store corresponding bits, then I can easily define bitwise operations 
> on "integers" by posting relation constraints on the bits.
>
> The problem is with the addition.
>
> My first approach was to add an IntVar, post linear constraints with 
> powers of 2 as coefficients to reconstruct integer from bits, however 
> gecode limits IntVar into signed int bounds and it doesn't fit.
>
> The second approach was to just implement binary addition:
>
> bool lsb = true;
>
> for (int i=(INT_BITS-1); i>=0; i--) {
>
> BoolVarArgs bits;
>
> bits << bools[i] << x->bools[i];
>
> if (!lsb) {
>
> bits << result->bools[INT_BITS+i+1];
>
> }
>
> rel(*model, BOT_XOR, bits, result->bools[i]);
>
> if (lsb) {
>
> rel(*model, BOT_AND, bits, result->bools[INT_BITS+i]);
>
> lsb = false;
>
> } else {
>
> linear(*model, bits, IRT_GQ, 2, result->bools[INT_BITS+i]);
>
> }
>
> }
>
> (bools[i] - bits of the first "integer", x->bools[i] - bits of the 
> second "integer", result->bools[i] - bits of the resulting "integer", 
> result->bools[INT_BITS+i] - carry bits)
>
> That works but it turned out to be very inefficient in practice, 
> complexity of the model is growing exponentially with this approach.
>
> Any thoughts? Maybe there's a way to recompile gecode to use unsigned 
> int internally? Maybe there are ideas on better implementation of 
> addition? Maybe just some suggestion on another tool which uses 
> unsigned ints internally?
>
> Thanks,
>
> Serg
>
>
>
> _______________________________________________
> Gecode users mailing list
> users at gecode.org
> https://www.gecode.org/mailman/listinfo/gecode-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gecode.org/pipermail/users/attachments/20150311/ce33d46c/attachment.html>