How to encode sum of boolean variables by SAT?
252 views
Skip to first unread message
Weichen
Oct 14, 2008, 8:52:34 AM10/14/08
to MiniSat
a, b, c, d, e are boolean variables. How to encode constraint a+b+c=d
+e with SAT? To list all possible variable assignments with DNF and
transform to CNF? Is there an easy way to do that? Thanks.
+e with SAT? To list all possible variable assignments with DNF and
transform to CNF? Is there an easy way to do that? Thanks.
Weichen
Oct 14, 2008, 9:01:16 AM10/14/08
to MiniSat
Here, I mean if a=0, b=1, c=1, then a+b+c=0+1+1=2
jw
Oct 14, 2008, 1:16:52 PM10/14/08
to MiniSat
> To list all possible variable assignments with DNF and
> transform to CNF?
but its computation should be a hard problem (in general).
In your case, it looks like you need 15 clauses
with total 50 literals:
(-b1 + -b2 + -b3) * (-b1 + -b2 + b4) * (-b1 + -b2 + b5) *
(-b1 + -b3 + b4) * (-b1 + -b3 + b5) * (-b1 + b4 + b5) *
(b1 + b2 + b3 + -b4) * (b1 + b2 + b3 + -b5) * (b1 + b2 + -b4 + -b5)
* (b1 + b3 + -b4 + -b5) * (-b2 + -b3 + b4) * (-b2 + -b3 + b5) *
(-b2 + b4 + b5) * (b2 + b3 + -b4 + -b5) * (-b3 + b4 + b5)
I observed that if you introduce an additional variable
(b6) that is equal to the LSB of the sum
then you only need 13 clauses with 43 literals:
(-b1 + -b2 + -b3) * (-b1 + -b2 + -b6) * (-b1 + -b3 + -b6)
* (-b1 + b4 + b6) * (b1 + -b2 + b3 + b6) * (b1 + b2 + b3 + -b6) *
(b1 + b2 + -b5 + b6) * (-b2 + -b3 + -b6) * (b2 + b3 + -b4 + -b5) *
(-b3 + b4 + b6) * (-b4 + -b5 + -b6) * (-b4 + b5 + b6) *
(b4 + b5 + -b6)
It is of course not clear whether this "optimization"
helps the SAT solver.
J.W.
Weichen
Oct 15, 2008, 1:57:04 AM10/15/08
to MiniSat
Dear J.W.,
Thank you very much for the reply. I learn that the encoding should be
correct, but it is still hard for me to generate it by myself. My
problem is that, given M boolean variables on the left side of the
equation, and N boolean variables on the right side, I need to
generate SAT encoding that guarantees the correctness of the equation,
i.e., there are the same number of variables that are assigned "true"
on both sides. What is the rule to generate the clauses you mentioned?
Thank you very much.
Thank you very much for the reply. I learn that the encoding should be
correct, but it is still hard for me to generate it by myself. My
problem is that, given M boolean variables on the left side of the
equation, and N boolean variables on the right side, I need to
generate SAT encoding that guarantees the correctness of the equation,
i.e., there are the same number of variables that are assigned "true"
on both sides. What is the rule to generate the clauses you mentioned?
Thank you very much.
peter
Oct 15, 2008, 2:06:13 AM10/15/08
to MiniSat
The paper http://minisat.se/downloads/MiniSat+.ps.gz describes a
systematic way to generate a SAT encoding (using extra variables).
Best,
Peter
Weichen
Oct 15, 2008, 3:08:30 AM10/15/08
to MiniSat
Thanks for all the information. I think I have gotten the encoding
method:
First, if M>N, encode no more than N variables are true;
Then, if there is one true assignment on the left, there is at least
one on the right, and vice versa;
Then, if there are two true assignments on the left, there are at
least two on the right, and vice versa;
...
until N true assignment.
Thank you very much!
On Oct 15, 2:06 pm, peter <peter.li...@gmail.com> wrote:
> The paperhttp://minisat.se/downloads/MiniSat+.ps.gzdescribes a
method:
First, if M>N, encode no more than N variables are true;
Then, if there is one true assignment on the left, there is at least
one on the right, and vice versa;
Then, if there are two true assignments on the left, there are at
least two on the right, and vice versa;
...
until N true assignment.
Thank you very much!
On Oct 15, 2:06 pm, peter <peter.li...@gmail.com> wrote:
> The paperhttp://minisat.se/downloads/MiniSat+.ps.gzdescribes a
jw
Oct 15, 2008, 4:59:16 AM10/15/08
to MiniSat
> The paper http://minisat.se/downloads/MiniSat+.ps.gzdescribes a
(I'd never thought that Section 5.3.4 of TAOCP - which I absolutely
love when teaching - is applicable to any present-day problem. Not!)
In general, what is known about CNF minimization?
E.g. I want small CNFs for (non-overflowing) N-bit
binary addition or multiplication (using exactly the 3N variables).
Using some kind of simulated annealing on CNFs,
I get such numbers (clauses/literals)
3bit add: (26/98) mult: (20/58)
4bit add: (62/261) mult: (54/173)
If you can beat this, I'd like to know.
(And yes, I have an application for that.)
J.W.
> systematic way to generate a SAT encoding (using extra variables).
Yes, the "sorting network" encoding is a very clever thing.
(I'd never thought that Section 5.3.4 of TAOCP - which I absolutely
love when teaching - is applicable to any present-day problem. Not!)
In general, what is known about CNF minimization?
E.g. I want small CNFs for (non-overflowing) N-bit
binary addition or multiplication (using exactly the 3N variables).
Using some kind of simulated annealing on CNFs,
I get such numbers (clauses/literals)
3bit add: (26/98) mult: (20/58)
4bit add: (62/261) mult: (54/173)
If you can beat this, I'd like to know.
(And yes, I have an application for that.)
J.W.
peter
Oct 16, 2008, 5:24:14 AM10/16/08
to MiniSat
On Oct 15, 10:59 am, jw <waldm...@imn.htwk-leipzig.de> wrote:
> In general, what is known about CNF minimization?
> E.g. I want small CNFs for (non-overflowing) N-bit
> binary addition or multiplication (using exactly the 3N variables).
> Using some kind of simulated annealing on CNFs,
> I get such numbers (clauses/literals)
>
> 3bit add: (26/98) mult: (20/58)
> 4bit add: (62/261) mult: (54/173)
>
> If you can beat this, I'd like to know.
> (And yes, I have an application for that.)
3bit add: (79/312) mult: (77,292)
4bit add: (283/1413) mult: (378,1838)
However, I am pretty sure that the above is an optimal description of
the solution set (if one restricts oneself to introducing no
additional variables). One has to list all clauses which do not cut
off any solutions and which are minimal in that respect. By non-
overflowing addition you mean all triples (a,b,c) where a+b=c and
a,b,c are N-bit binary numbers, right?
jw
Oct 16, 2008, 12:22:26 PM10/16/08
to MiniSat
> By nonoverflowing addition you mean all triples (a,b,c) where a+b=c and
Here is my current record holder (25 clauses, 94 literals)
for non-overflowing 3-bit addition [x3,x2,x1] + [x6,x5,x4] =
[x9,x8,x7]
(binary encoding of natural number 0 .. 7, lsbs on the right)
(-x1 + -x4 + -x5 + -x6) * (-x1 + -x4 + -x7) * (-x1 + x4 + x7) *
(x1 + -x2 + -x5 + -x8) * (x1 + x2 + -x5 + x8) *
(x1 + x2 + x5 + -x8) * (x1 + -x4 + x7) * (x1 + x4 + -x7) *
(-x2 + -x3 + x8) * (-x2 + -x4 + -x5 + x7 + x8) *
(-x2 + -x4 + x5 + x7 + -x8) * (-x2 + x4 + -x5 + -x7 + -x8) *
(-x2 + -x6 + x8) * (-x2 + x8 + x9) * (x2 + x3 + x6 + -x8 + -x9) *
(x2 + -x4 + x5 + x7 + x8) * (x2 + -x5 + -x7 + x8) *
(x2 + x5 + -x7 + -x8) * (-x3 + -x4 + -x5 + x7) * (-x3 + -x6) *
(-x3 + x9) * (x3 + x4 + x5 + x6 + -x9) * (x3 + x5 + x6 + -x7 + -x9)
* (-x4 + -x5 + x7 + x9) * (-x6 + x9)
E.g. (-x3 + -x6) means that one of
the msbs must be zero (otherwise it will overflow).
I am pretty sure this is correct (since I use it in an application
that would fail otherwise). I am less condident that it is minimal
(let's say, in the number of literals).
For 4 bit, have (56/240) for addition and (39/134) for multiplication
now.
It is clear that multiplication is easier (smaller CNF) than addition
since if will overflow more often , so there are somehow less
conditions to encode.
In general I would assume that "is there an equivalent CNF of size <=
S"
corresponds to some vertex cover problem so I don't expect an easy
algorithm to find one.
It would of course be "recursively funny" if we could solve this
problem via transformation to SAT...
But the graph looks exponentially large (it consists of all possible
clauses).
> a,b,c are N-bit binary numbers, right?
Yes.
Here is my current record holder (25 clauses, 94 literals)
for non-overflowing 3-bit addition [x3,x2,x1] + [x6,x5,x4] =
[x9,x8,x7]
(binary encoding of natural number 0 .. 7, lsbs on the right)
(-x1 + -x4 + -x5 + -x6) * (-x1 + -x4 + -x7) * (-x1 + x4 + x7) *
(x1 + -x2 + -x5 + -x8) * (x1 + x2 + -x5 + x8) *
(x1 + x2 + x5 + -x8) * (x1 + -x4 + x7) * (x1 + x4 + -x7) *
(-x2 + -x3 + x8) * (-x2 + -x4 + -x5 + x7 + x8) *
(-x2 + -x4 + x5 + x7 + -x8) * (-x2 + x4 + -x5 + -x7 + -x8) *
(-x2 + -x6 + x8) * (-x2 + x8 + x9) * (x2 + x3 + x6 + -x8 + -x9) *
(x2 + -x4 + x5 + x7 + x8) * (x2 + -x5 + -x7 + x8) *
(x2 + x5 + -x7 + -x8) * (-x3 + -x4 + -x5 + x7) * (-x3 + -x6) *
(-x3 + x9) * (x3 + x4 + x5 + x6 + -x9) * (x3 + x5 + x6 + -x7 + -x9)
* (-x4 + -x5 + x7 + x9) * (-x6 + x9)
E.g. (-x3 + -x6) means that one of
the msbs must be zero (otherwise it will overflow).
I am pretty sure this is correct (since I use it in an application
that would fail otherwise). I am less condident that it is minimal
(let's say, in the number of literals).
For 4 bit, have (56/240) for addition and (39/134) for multiplication
now.
It is clear that multiplication is easier (smaller CNF) than addition
since if will overflow more often , so there are somehow less
conditions to encode.
In general I would assume that "is there an equivalent CNF of size <=
S"
corresponds to some vertex cover problem so I don't expect an easy
algorithm to find one.
It would of course be "recursively funny" if we could solve this
problem via transformation to SAT...
But the graph looks exponentially large (it consists of all possible
clauses).
peter
Oct 16, 2008, 1:50:22 PM10/16/08
to MiniSat
OK, I stand corrected. I was confused, thinking that all valid clauses
which are minimal in that respect are necessary. Nevertheless, maybe
my confusion can be good for something, in the following way: In the
minimal set cover problem you alluded to, one might restrict oneself
to the aforementioned clauses (as opposed to all clauses). Their
number can be found in my previous mail (actually there's a typo, the
312 is supposed to be a 321). That should be entirely feasible for N=3
and 4.
peter
Oct 19, 2008, 11:33:27 AM10/19/08
to MiniSat
So, I just went through with the idea I described in my previous post
and these are the clauses I found. I used coin cbc/clp in order to
solver the set cover problems. Unless I made a mistake, these clause
sets are all minimal (either w.r.t. #clauses, w.r.t. #literals, or
simultaneously).
Sorry for the big post.
Peter
3bit add: (24/90) mult: (20/57)
4bit add: (43/191) mult: (36/124), (37/123)
5bit add: (67/314), (69/313)
3bit add: (24/90):
(-x3 + -x6)
* (-x3 + x9)
* (-x2 + -x3 + x8)
* (-x2 + -x6 + x8)
* (-x2 + x8 + x9)
* (-x2 + x8 + x9)
* (x1 + -x4 + x7)
* (x1 + x4 + -x7)
* (x1 + x4 + -x7)
* (-x1 + -x4 + -x7)
* (x1 + x2 + -x5 + x8)
* (x2 + x4 + -x5 + x8)
* (x1 + x2 + x5 + -x8)
* (x1 + -x2 + -x5 + -x8)
* (x2 + x4 + x5 + -x8)
* (-x2 + x4 + -x5 + -x8)
* (-x1 + -x3 + -x5 + x7)
* (-x1 + -x5 + -x6 + x7)
* (-x1 + -x5 + x7 + x9)
* (x1 + x3 + x5 + x6 + -x9)
* (x3 + x4 + x5 + x6 + -x9)
* (x2 + x3 + x6 + -x8 + -x9)
* (-x1 + x2 + x5 + x7 + x8)
* (-x1 + -x2 + -x5 + x7 + x8)
* (-x1 + -x2 + x5 + x7 + -x8)
3bit mult: (20/57)
(-x3 + -x6)
* (-x2 + -x6)
* (-x3 + -x5)
* (x1 + -x7)
* (x4 + -x7)
* (-x1 + -x6 + x9)
* (-x2 + -x5 + x9)
* (-x3 + -x4 + x9)
* (x1 + -x6 + -x9)
* (-x3 + x4 + -x9)
* (-x1 + -x5 + x8)
* (-x2 + -x4 + x8)
* (x1 + x2 + -x8)
* (x2 + x5 + -x8)
* (x1 + x4 + -x8)
* (x4 + x5 + -x8)
* (-x1 + -x4 + x7)
* (-x2 + -x5 + -x7)
* (x3 + x5 + x6 + -x9)
* (x2 + -x5 + x6 + -x9)
4bit add: (43/191)
(-x4 + -x8)
* (-x4 + x12)
* (-x8 + x12)
* (-x3 + -x4 + x11)
* (-x3 + -x8 + x11)
* (-x3 + x11 + x12)
* (-x1 + x5 + x9)
* (x1 + x5 + -x9)
* (-x1 + -x5 + -x9)
* (-x2 + -x4 + -x7 + x10)
* (-x2 + -x7 + -x8 + x10)
* (x1 + x2 + -x6 + x10)
* (-x2 + -x7 + x10 + x12)
* (x1 + x2 + x6 + -x10)
* (x1 + -x2 + -x6 + -x10)
* (-x2 + x5 + -x6 + -x10)
* (x2 + -x6 + -x9 + x10)
* (x2 + x6 + -x9 + -x10)
* (x1 + x3 + x6 + -x7 + x11)
* (x3 + x5 + x6 + -x7 + x11)
* (x1 + x3 + x6 + x7 + -x11)
* (x1 + -x3 + x6 + -x7 + -x11)
* (x3 + x5 + x6 + x7 + -x11)
* (x3 + x4 + x8 + -x11 + -x12)
* (-x2 + x3 + x7 + x10 + x11)
* (-x2 + -x3 + -x7 + x10 + x11)
* (-x2 + -x3 + x7 + x10 + -x11)
* (x2 + x3 + -x7 + -x10 + x11)
* (x2 + x3 + x7 + -x10 + -x11)
* (x2 + -x3 + -x7 + -x10 + -x11)
* (-x4 + -x5 + -x6 + -x7 + x9)
* (-x5 + -x6 + -x7 + -x8 + x9)
* (-x5 + -x6 + -x7 + x9 + x12)
* (x2 + -x5 + x6 + x9 + x10)
* (-x2 + -x5 + -x6 + x9 + x10)
* (-x2 + -x5 + x6 + x9 + -x10)
* (-x3 + x6 + -x7 + -x9 + -x11)
* (x1 + x4 + x6 + x7 + x8 + -x12)
* (x2 + x4 + x7 + x8 + -x10 + -x12)
* (x3 + -x5 + -x6 + x7 + x9 + x11)
* (-x3 + -x5 + -x6 + -x7 + x9 + x11)
* (-x3 + -x5 + -x6 + x7 + x9 + -x11)
* (x4 + x6 + x7 + x8 + -x9 + -x12)
4bit mult: (36/124)
(-x4 + -x8)
* (-x3 + -x8)
* (-x2 + -x8)
* (-x4 + -x7)
* (-x3 + -x7)
* (-x4 + -x6)
* (x1 + -x9)
* (x5 + -x9)
* (-x1 + -x8 + x12)
* (-x2 + -x7 + x12)
* (-x3 + -x6 + x12)
* (-x4 + -x5 + x12)
* (-x1 + -x7 + x11)
* (-x3 + -x5 + x11)
* (x1 + x2 + -x10)
* (x2 + x6 + -x10)
* (x1 + x5 + -x10)
* (x5 + x6 + -x10)
* (-x1 + -x5 + x9)
* (x1 + x2 + -x7 + -x12)
* (-x2 + -x6 + x11 + x12)
* (x1 + x2 + x3 + -x11)
* (x1 + x3 + x6 + -x11)
* (x2 + x5 + x7 + -x11)
* (x5 + x6 + x7 + -x11)
* (-x2 + -x5 + x6 + x10)
* (-x2 + -x5 + x10 + -x11)
* (-x2 + -x6 + x9 + x11)
* (-x1 + -x6 + x9 + x10)
* (x3 + x7 + -x9 + -x11)
* (x2 + -x6 + -x9 + x10)
* (x1 + x3 + x4 + x7 + -x12)
* (x2 + x4 + x6 + x8 + -x12)
* (x5 + x6 + x7 + x8 + -x12)
* (-x1 + x3 + -x6 + x8 + -x10 + -x12)
* (-x2 + x4 + -x5 + x7 + -x10 + -x12)
4bit mult: (37/123)
(-x4 + -x8)
* (-x3 + -x8)
* (-x2 + -x8)
* (-x4 + -x7)
* (-x3 + -x7)
* (-x4 + -x6)
* (x1 + -x9)
* (x5 + -x9)
* (-x1 + -x8 + x12)
* (-x2 + -x7 + x12)
* (-x3 + -x6 + x12)
* (-x4 + -x5 + x12)
* (x1 + -x8 + -x12)
* (-x4 + x5 + -x12)
* (-x1 + -x7 + x11)
* (-x3 + -x5 + x11)
* (x1 + x2 + -x10)
* (x2 + x6 + -x10)
* (x1 + x5 + -x10)
* (x5 + x6 + -x10)
* (-x1 + -x5 + x9)
* (-x1 + -x2 + -x6 + -x7)
* (-x3 + x4 + x6 + -x12)
* (x1 + x2 + x3 + -x11)
* (x1 + x3 + x6 + -x11)
* (x2 + x5 + x7 + -x11)
* (x5 + x6 + x7 + -x11)
* (-x2 + -x5 + x6 + x10)
* (-x2 + -x5 + x10 + -x11)
* (-x2 + -x6 + x9 + x11)
* (-x1 + -x6 + x9 + x10)
* (-x2 + -x6 + -x9 + x12)
* (x3 + x7 + -x9 + -x11)
* (x2 + -x6 + -x9 + x10)
* (x2 + x3 + x4 + x8 + -x12)
* (x3 + x5 + x7 + x8 + -x12)
* (-x2 + x4 + -x5 + x7 + -x10 + -x12)
5bit add: (67/314)
(-x5 + -x10)
* (-x5 + x15)
* (-x10 + x15)
* (-x4 + -x5 + -x9)
* (-x4 + -x9 + -x10)
* (-x4 + -x9 + x15)
* (-x4 + -x5 + x14)
* (-x4 + -x10 + x14)
* (-x5 + -x9 + x14)
* (-x9 + -x10 + x14)
* (-x4 + x14 + x15)
* (-x9 + x14 + x15)
* (x1 + -x6 + x11)
* (x1 + x6 + -x11)
* (-x1 + -x6 + -x11)
* (x1 + -x2 + x7 + x12)
* (-x2 + x6 + x7 + x12)
* (x1 + x2 + x7 + -x12)
* (x2 + x6 + x7 + -x12)
* (-x2 + x6 + -x7 + -x12)
* (-x2 + -x7 + -x11 + -x12)
* (x4 + x5 + x9 + x10 + -x15)
* (x3 + -x4 + x8 + x9 + x14)
* (x3 + x4 + x8 + -x9 + x14)
* (x3 + x4 + x8 + x9 + -x14)
* (x1 + x2 + -x3 + x8 + x13)
* (x1 + x2 + x3 + -x8 + x13)
* (x2 + -x3 + x6 + x8 + x13)
* (x2 + x3 + x6 + -x8 + x13)
* (x4 + -x8 + x9 + x13 + x14)
* (-x4 + -x8 + -x9 + x13 + x14)
* (-x4 + -x8 + x9 + x13 + -x14)
* (x4 + -x8 + -x9 + x13 + -x14)
* (x1 + x2 + -x3 + -x8 + -x13)
* (x2 + x3 + x6 + x8 + -x13)
* (x2 + -x3 + x6 + -x8 + -x13)
* (x3 + -x4 + x9 + -x13 + x14)
* (x3 + x4 + -x9 + -x13 + x14)
* (-x4 + x8 + x9 + -x13 + x14)
* (x4 + x8 + -x9 + -x13 + x14)
* (x3 + x4 + x9 + -x13 + -x14)
* (x4 + x8 + x9 + -x13 + -x14)
* (x3 + -x7 + x8 + x12 + x13)
* (-x3 + -x7 + -x8 + x12 + x13)
* (x3 + -x7 + -x8 + x12 + -x13)
* (-x3 + x7 + x8 + -x12 + x13)
* (x3 + x7 + -x8 + -x12 + x13)
* (x3 + x7 + x8 + -x12 + -x13)
* (-x3 + x7 + -x8 + -x12 + -x13)
* (-x1 + x2 + x7 + x11 + x12)
* (-x1 + -x2 + -x7 + x11 + x12)
* (-x1 + x2 + -x7 + x11 + -x12)
* (x2 + x3 + x8 + -x11 + -x13)
* (x3 + x5 + x8 + x10 + -x14 + -x15)
* (x3 + x5 + x10 + -x13 + -x14 + -x15)
* (x5 + x8 + x10 + -x13 + -x14 + -x15)
* (-x3 + x4 + -x7 + x9 + x12 + x14)
* (-x3 + -x4 + -x7 + -x9 + x12 + x14)
* (-x3 + -x4 + -x7 + x9 + x12 + -x14)
* (-x3 + x4 + -x7 + -x9 + x12 + -x14)
* (-x1 + -x2 + x3 + x8 + x11 + x13)
* (-x1 + -x2 + -x3 + -x8 + x11 + x13)
* (-x1 + -x2 + x3 + -x8 + x11 + -x13)
* (-x1 + -x2 + -x3 + x4 + x9 + x11 + x14)
* (-x1 + -x2 + -x3 + -x4 + -x9 + x11 + x14)
* (-x1 + -x2 + -x3 + -x4 + x9 + x11 + -x14)
* (-x1 + -x2 + -x3 + x4 + -x9 + x11 + -x14)
5bit add: (69/313)
(-x5 + -x10)
* (-x5 + x15)
* (-x10 + x15)
* (-x4 + -x5 + -x9)
* (-x4 + -x9 + -x10)
* (-x4 + -x9 + x15)
* (-x4 + -x5 + x14)
* (-x4 + -x10 + x14)
* (-x5 + -x9 + x14)
* (-x9 + -x10 + x14)
* (-x4 + x14 + x15)
* (-x9 + x14 + x15)
* (-x1 + x6 + x11)
* (x1 + x6 + -x11)
* (-x1 + -x6 + -x11)
* (x1 + x2 + -x7 + x12)
* (x1 + x2 + x7 + -x12)
* (x1 + -x2 + -x7 + -x12)
* (x2 + x6 + x7 + -x12)
* (x2 + -x7 + -x11 + x12)
* (-x2 + -x7 + -x11 + -x12)
* (x4 + x5 + x9 + x10 + -x15)
* (x3 + -x4 + x8 + x9 + x14)
* (x3 + x4 + x8 + -x9 + x14)
* (-x3 + x4 + -x8 + x9 + x14)
* (-x3 + -x4 + -x8 + -x9 + x14)
* (x3 + x4 + x8 + x9 + -x14)
* (-x3 + -x4 + -x8 + x9 + -x14)
* (-x3 + x4 + -x8 + -x9 + -x14)
* (x1 + -x3 + x7 + x8 + x13)
* (x1 + x3 + x7 + -x8 + x13)
* (-x3 + x6 + x7 + x8 + x13)
* (-x3 + x4 + x9 + x13 + x14)
* (-x3 + -x4 + -x9 + x13 + x14)
* (x4 + -x8 + x9 + x13 + x14)
* (-x4 + -x8 + -x9 + x13 + x14)
* (-x3 + -x4 + x9 + x13 + -x14)
* (-x3 + x4 + -x9 + x13 + -x14)
* (-x4 + -x8 + x9 + x13 + -x14)
* (x4 + -x8 + -x9 + x13 + -x14)
* (x1 + x3 + x7 + x8 + -x13)
* (x1 + -x3 + x7 + -x8 + -x13)
* (x3 + x6 + x7 + x8 + -x13)
* (-x3 + x6 + x7 + -x8 + -x13)
* (x3 + -x4 + x9 + -x13 + x14)
* (x3 + x4 + -x9 + -x13 + x14)
* (-x4 + x8 + x9 + -x13 + x14)
* (x4 + x8 + -x9 + -x13 + x14)
* (x3 + x4 + x9 + -x13 + -x14)
* (x4 + x8 + x9 + -x13 + -x14)
* (-x2 + x3 + x8 + x12 + x13)
* (-x2 + -x3 + -x8 + x12 + x13)
* (-x2 + -x3 + x8 + x12 + -x13)
* (-x2 + x3 + -x8 + x12 + -x13)
* (x2 + -x3 + x8 + -x12 + x13)
* (x2 + x3 + -x8 + -x12 + x13)
* (x2 + x3 + x8 + -x12 + -x13)
* (x2 + -x3 + -x8 + -x12 + -x13)
* (x2 + -x6 + x7 + x11 + x12)
* (-x2 + -x6 + -x7 + x11 + x12)
* (-x2 + -x6 + x7 + x11 + -x12)
* (x3 + x7 + -x8 + -x11 + x13)
* (x3 + x5 + x8 + x10 + -x14 + -x15)
* (x3 + x5 + x10 + -x13 + -x14 + -x15)
* (x5 + x8 + x10 + -x13 + -x14 + -x15)
* (x3 + -x6 + -x7 + x8 + x11 + x13)
* (-x3 + -x6 + -x7 + -x8 + x11 + x13)
* (-x3 + -x6 + -x7 + x8 + x11 + -x13)
* (x3 + -x6 + -x7 + -x8 + x11 + -x13)
jw
Oct 21, 2008, 6:34:27 AM10/21/08
to MiniSat
> and these are the clauses I found. I used coin cbc/clp in order to
> solver the set cover problems.
them
in my application - which is basically a constraint solver for systems
of (in)equalities between nonlinear expressions (using plus, times)
where unknowns (and intermediate results) are restricted to small bit
width.
It is entirely possible that small CNFs are not best with this respect
(feeding them to a SAT solver) because e.g. additional clauses might
help
unit propagation.
J.W.
jw
Nov 10, 2008, 5:15:56 PM11/10/08
to MiniSat
> 3bit add: (24/90) mult: (20/57)
> 4bit add: (43/191) mult: (36/124)
CNFs
in http://termination-portal.org/wiki/Termination_Competition
(currently running). - J.W.
Reply all
Reply to author
Forward
0 new messages