lemon-project-template-glpk
view deps/glpk/src/glpnpp06.c @ 9:33de93886c88
Import GLPK 4.47
| author | Alpar Juttner <alpar@cs.elte.hu> |
|---|---|
| date | Sun, 06 Nov 2011 20:59:10 +0100 |
| parents | |
| children |
line source
1 /* glpnpp06.c (translate feasibility problem to CNF-SAT) */
3 /***********************************************************************
4 * This code is part of GLPK (GNU Linear Programming Kit).
5 *
6 * Copyright (C) 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008,
7 * 2009, 2010, 2011 Andrew Makhorin, Department for Applied Informatics,
8 * Moscow Aviation Institute, Moscow, Russia. All rights reserved.
9 * E-mail: <mao@gnu.org>.
10 *
11 * GLPK is free software: you can redistribute it and/or modify it
12 * under the terms of the GNU General Public License as published by
13 * the Free Software Foundation, either version 3 of the License, or
14 * (at your option) any later version.
15 *
16 * GLPK is distributed in the hope that it will be useful, but WITHOUT
17 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
18 * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
19 * License for more details.
20 *
21 * You should have received a copy of the GNU General Public License
22 * along with GLPK. If not, see <http://www.gnu.org/licenses/>.
23 ***********************************************************************/
25 #include "glpnpp.h"
27 /***********************************************************************
28 * npp_sat_free_row - process free (unbounded) row
29 *
30 * This routine processes row p, which is free (i.e. has no finite
31 * bounds):
32 *
33 * -inf < sum a[p,j] x[j] < +inf. (1)
34 *
35 * The constraint (1) cannot be active and therefore it is redundant,
36 * so the routine simply removes it from the original problem. */
38 void npp_sat_free_row(NPP *npp, NPPROW *p)
39 { /* the row should be free */
40 xassert(p->lb == -DBL_MAX && p->ub == +DBL_MAX);
41 /* remove the row from the problem */
42 npp_del_row(npp, p);
43 return;
44 }
46 /***********************************************************************
47 * npp_sat_fixed_col - process fixed column
48 *
49 * This routine processes column q, which is fixed:
50 *
51 * x[q] = s[q], (1)
52 *
53 * where s[q] is a fixed column value.
54 *
55 * The routine substitutes fixed value s[q] into constraint rows and
56 * then removes column x[q] from the original problem.
57 *
58 * Substitution of x[q] = s[q] into row i gives:
59 *
60 * L[i] <= sum a[i,j] x[j] <= U[i] ==>
61 * j
62 *
63 * L[i] <= sum a[i,j] x[j] + a[i,q] x[q] <= U[i] ==>
64 * j!=q
65 *
66 * L[i] <= sum a[i,j] x[j] + a[i,q] s[q] <= U[i] ==>
67 * j!=q
68 *
69 * L~[i] <= sum a[i,j] x[j] <= U~[i],
70 * j!=q
71 *
72 * where
73 *
74 * L~[i] = L[i] - a[i,q] s[q], (2)
75 *
76 * U~[i] = U[i] - a[i,q] s[q] (3)
77 *
78 * are, respectively, lower and upper bound of row i in the transformed
79 * problem.
80 *
81 * On recovering solution x[q] is assigned the value of s[q]. */
83 struct sat_fixed_col
84 { /* fixed column */
85 int q;
86 /* column reference number for variable x[q] */
87 int s;
88 /* value, at which x[q] is fixed */
89 };
91 static int rcv_sat_fixed_col(NPP *, void *);
93 int npp_sat_fixed_col(NPP *npp, NPPCOL *q)
94 { struct sat_fixed_col *info;
95 NPPROW *i;
96 NPPAIJ *aij;
97 int temp;
98 /* the column should be fixed */
99 xassert(q->lb == q->ub);
100 /* create transformation stack entry */
101 info = npp_push_tse(npp,
102 rcv_sat_fixed_col, sizeof(struct sat_fixed_col));
103 info->q = q->j;
104 info->s = (int)q->lb;
105 xassert((double)info->s == q->lb);
106 /* substitute x[q] = s[q] into constraint rows */
107 if (info->s == 0)
108 goto skip;
109 for (aij = q->ptr; aij != NULL; aij = aij->c_next)
110 { i = aij->row;
111 if (i->lb != -DBL_MAX)
112 { i->lb -= aij->val * (double)info->s;
113 temp = (int)i->lb;
114 if ((double)temp != i->lb)
115 return 1; /* integer arithmetic error */
116 }
117 if (i->ub != +DBL_MAX)
118 { i->ub -= aij->val * (double)info->s;
119 temp = (int)i->ub;
120 if ((double)temp != i->ub)
121 return 2; /* integer arithmetic error */
122 }
123 }
124 skip: /* remove the column from the problem */
125 npp_del_col(npp, q);
126 return 0;
127 }
129 static int rcv_sat_fixed_col(NPP *npp, void *info_)
130 { struct sat_fixed_col *info = info_;
131 npp->c_value[info->q] = (double)info->s;
132 return 0;
133 }
135 /***********************************************************************
136 * npp_sat_is_bin_comb - test if row is binary combination
137 *
138 * This routine tests if the specified row is a binary combination,
139 * i.e. all its constraint coefficients are +1 and -1 and all variables
140 * are binary. If the test was passed, the routine returns non-zero,
141 * otherwise zero. */
143 int npp_sat_is_bin_comb(NPP *npp, NPPROW *row)
144 { NPPCOL *col;
145 NPPAIJ *aij;
146 xassert(npp == npp);
147 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
148 { if (!(aij->val == +1.0 || aij->val == -1.0))
149 return 0; /* non-unity coefficient */
150 col = aij->col;
151 if (!(col->is_int && col->lb == 0.0 && col->ub == 1.0))
152 return 0; /* non-binary column */
153 }
154 return 1; /* test was passed */
155 }
157 /***********************************************************************
158 * npp_sat_num_pos_coef - determine number of positive coefficients
159 *
160 * This routine returns the number of positive coefficients in the
161 * specified row. */
163 int npp_sat_num_pos_coef(NPP *npp, NPPROW *row)
164 { NPPAIJ *aij;
165 int num = 0;
166 xassert(npp == npp);
167 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
168 { if (aij->val > 0.0)
169 num++;
170 }
171 return num;
172 }
174 /***********************************************************************
175 * npp_sat_num_neg_coef - determine number of negative coefficients
176 *
177 * This routine returns the number of negative coefficients in the
178 * specified row. */
180 int npp_sat_num_neg_coef(NPP *npp, NPPROW *row)
181 { NPPAIJ *aij;
182 int num = 0;
183 xassert(npp == npp);
184 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
185 { if (aij->val < 0.0)
186 num++;
187 }
188 return num;
189 }
191 /***********************************************************************
192 * npp_sat_is_cover_ineq - test if row is covering inequality
193 *
194 * The canonical form of a covering inequality is the following:
195 *
196 * sum x[j] >= 1, (1)
197 * j in J
198 *
199 * where all x[j] are binary variables.
200 *
201 * In general case a covering inequality may have one of the following
202 * two forms:
203 *
204 * sum x[j] - sum x[j] >= 1 - |J-|, (2)
205 * j in J+ j in J-
206 *
207 *
208 * sum x[j] - sum x[j] <= |J+| - 1. (3)
209 * j in J+ j in J-
210 *
211 * Obviously, the inequality (2) can be transformed to the form (1) by
212 * substitution x[j] = 1 - x'[j] for all j in J-, where x'[j] is the
213 * negation of variable x[j]. And the inequality (3) can be transformed
214 * to (2) by multiplying both left- and right-hand sides by -1.
215 *
216 * This routine returns one of the following codes:
217 *
218 * 0, if the specified row is not a covering inequality;
219 *
220 * 1, if the specified row has the form (2);
221 *
222 * 2, if the specified row has the form (3). */
224 int npp_sat_is_cover_ineq(NPP *npp, NPPROW *row)
225 { xassert(npp == npp);
226 if (row->lb != -DBL_MAX && row->ub == +DBL_MAX)
227 { /* row is inequality of '>=' type */
228 if (npp_sat_is_bin_comb(npp, row))
229 { /* row is a binary combination */
230 if (row->lb == 1.0 - npp_sat_num_neg_coef(npp, row))
231 { /* row has the form (2) */
232 return 1;
233 }
234 }
235 }
236 else if (row->lb == -DBL_MAX && row->ub != +DBL_MAX)
237 { /* row is inequality of '<=' type */
238 if (npp_sat_is_bin_comb(npp, row))
239 { /* row is a binary combination */
240 if (row->ub == npp_sat_num_pos_coef(npp, row) - 1.0)
241 { /* row has the form (3) */
242 return 2;
243 }
244 }
245 }
246 /* row is not a covering inequality */
247 return 0;
248 }
250 /***********************************************************************
251 * npp_sat_is_pack_ineq - test if row is packing inequality
252 *
253 * The canonical form of a packing inequality is the following:
254 *
255 * sum x[j] <= 1, (1)
256 * j in J
257 *
258 * where all x[j] are binary variables.
259 *
260 * In general case a packing inequality may have one of the following
261 * two forms:
262 *
263 * sum x[j] - sum x[j] <= 1 - |J-|, (2)
264 * j in J+ j in J-
265 *
266 *
267 * sum x[j] - sum x[j] >= |J+| - 1. (3)
268 * j in J+ j in J-
269 *
270 * Obviously, the inequality (2) can be transformed to the form (1) by
271 * substitution x[j] = 1 - x'[j] for all j in J-, where x'[j] is the
272 * negation of variable x[j]. And the inequality (3) can be transformed
273 * to (2) by multiplying both left- and right-hand sides by -1.
274 *
275 * This routine returns one of the following codes:
276 *
277 * 0, if the specified row is not a packing inequality;
278 *
279 * 1, if the specified row has the form (2);
280 *
281 * 2, if the specified row has the form (3). */
283 int npp_sat_is_pack_ineq(NPP *npp, NPPROW *row)
284 { xassert(npp == npp);
285 if (row->lb == -DBL_MAX && row->ub != +DBL_MAX)
286 { /* row is inequality of '<=' type */
287 if (npp_sat_is_bin_comb(npp, row))
288 { /* row is a binary combination */
289 if (row->ub == 1.0 - npp_sat_num_neg_coef(npp, row))
290 { /* row has the form (2) */
291 return 1;
292 }
293 }
294 }
295 else if (row->lb != -DBL_MAX && row->ub == +DBL_MAX)
296 { /* row is inequality of '>=' type */
297 if (npp_sat_is_bin_comb(npp, row))
298 { /* row is a binary combination */
299 if (row->lb == npp_sat_num_pos_coef(npp, row) - 1.0)
300 { /* row has the form (3) */
301 return 2;
302 }
303 }
304 }
305 /* row is not a packing inequality */
306 return 0;
307 }
309 /***********************************************************************
310 * npp_sat_is_partn_eq - test if row is partitioning equality
311 *
312 * The canonical form of a partitioning equality is the following:
313 *
314 * sum x[j] = 1, (1)
315 * j in J
316 *
317 * where all x[j] are binary variables.
318 *
319 * In general case a partitioning equality may have one of the following
320 * two forms:
321 *
322 * sum x[j] - sum x[j] = 1 - |J-|, (2)
323 * j in J+ j in J-
324 *
325 *
326 * sum x[j] - sum x[j] = |J+| - 1. (3)
327 * j in J+ j in J-
328 *
329 * Obviously, the equality (2) can be transformed to the form (1) by
330 * substitution x[j] = 1 - x'[j] for all j in J-, where x'[j] is the
331 * negation of variable x[j]. And the equality (3) can be transformed
332 * to (2) by multiplying both left- and right-hand sides by -1.
333 *
334 * This routine returns one of the following codes:
335 *
336 * 0, if the specified row is not a partitioning equality;
337 *
338 * 1, if the specified row has the form (2);
339 *
340 * 2, if the specified row has the form (3). */
342 int npp_sat_is_partn_eq(NPP *npp, NPPROW *row)
343 { xassert(npp == npp);
344 if (row->lb == row->ub)
345 { /* row is equality constraint */
346 if (npp_sat_is_bin_comb(npp, row))
347 { /* row is a binary combination */
348 if (row->lb == 1.0 - npp_sat_num_neg_coef(npp, row))
349 { /* row has the form (2) */
350 return 1;
351 }
352 if (row->ub == npp_sat_num_pos_coef(npp, row) - 1.0)
353 { /* row has the form (3) */
354 return 2;
355 }
356 }
357 }
358 /* row is not a partitioning equality */
359 return 0;
360 }
362 /***********************************************************************
363 * npp_sat_reverse_row - multiply both sides of row by -1
364 *
365 * This routines multiplies by -1 both left- and right-hand sides of
366 * the specified row:
367 *
368 * L <= sum x[j] <= U,
369 *
370 * that results in the following row:
371 *
372 * -U <= sum (-x[j]) <= -L.
373 *
374 * If no integer overflow occured, the routine returns zero, otherwise
375 * non-zero. */
377 int npp_sat_reverse_row(NPP *npp, NPPROW *row)
378 { NPPAIJ *aij;
379 int temp, ret = 0;
380 double old_lb, old_ub;
381 xassert(npp == npp);
382 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
383 { aij->val = -aij->val;
384 temp = (int)aij->val;
385 if ((double)temp != aij->val)
386 ret = 1;
387 }
388 old_lb = row->lb, old_ub = row->ub;
389 if (old_ub == +DBL_MAX)
390 row->lb = -DBL_MAX;
391 else
392 { row->lb = -old_ub;
393 temp = (int)row->lb;
394 if ((double)temp != row->lb)
395 ret = 2;
396 }
397 if (old_lb == -DBL_MAX)
398 row->ub = +DBL_MAX;
399 else
400 { row->ub = -old_lb;
401 temp = (int)row->ub;
402 if ((double)temp != row->ub)
403 ret = 3;
404 }
405 return ret;
406 }
408 /***********************************************************************
409 * npp_sat_split_pack - split packing inequality
410 *
411 * Let there be given a packing inequality in canonical form:
412 *
413 * sum t[j] <= 1, (1)
414 * j in J
415 *
416 * where t[j] = x[j] or t[j] = 1 - x[j], x[j] is a binary variable.
417 * And let J = J1 U J2 is a partition of the set of literals. Then the
418 * inequality (1) is obviously equivalent to the following two packing
419 * inequalities:
420 *
421 * sum t[j] <= y <--> sum t[j] + (1 - y) <= 1, (2)
422 * j in J1 j in J1
423 *
424 * sum t[j] <= 1 - y <--> sum t[j] + y <= 1, (3)
425 * j in J2 j in J2
426 *
427 * where y is a new binary variable added to the transformed problem.
428 *
429 * Assuming that the specified row is a packing inequality (1), this
430 * routine constructs the set J1 by including there first nlit literals
431 * (terms) from the specified row, and the set J2 = J \ J1. Then the
432 * routine creates a new row, which corresponds to inequality (2), and
433 * replaces the specified row with inequality (3). */
435 NPPROW *npp_sat_split_pack(NPP *npp, NPPROW *row, int nlit)
436 { NPPROW *rrr;
437 NPPCOL *col;
438 NPPAIJ *aij;
439 int k;
440 /* original row should be packing inequality (1) */
441 xassert(npp_sat_is_pack_ineq(npp, row) == 1);
442 /* and nlit should be less than the number of literals (terms)
443 in the original row */
444 xassert(0 < nlit && nlit < npp_row_nnz(npp, row));
445 /* create new row corresponding to inequality (2) */
446 rrr = npp_add_row(npp);
447 rrr->lb = -DBL_MAX, rrr->ub = 1.0;
448 /* move first nlit literals (terms) from the original row to the
449 new row; the original row becomes inequality (3) */
450 for (k = 1; k <= nlit; k++)
451 { aij = row->ptr;
452 xassert(aij != NULL);
453 /* add literal to the new row */
454 npp_add_aij(npp, rrr, aij->col, aij->val);
455 /* correct rhs */
456 if (aij->val < 0.0)
457 rrr->ub -= 1.0, row->ub += 1.0;
458 /* remove literal from the original row */
459 npp_del_aij(npp, aij);
460 }
461 /* create new binary variable y */
462 col = npp_add_col(npp);
463 col->is_int = 1, col->lb = 0.0, col->ub = 1.0;
464 /* include literal (1 - y) in the new row */
465 npp_add_aij(npp, rrr, col, -1.0);
466 rrr->ub -= 1.0;
467 /* include literal y in the original row */
468 npp_add_aij(npp, row, col, +1.0);
469 return rrr;
470 }
472 /***********************************************************************
473 * npp_sat_encode_pack - encode packing inequality
474 *
475 * Given a packing inequality in canonical form:
476 *
477 * sum t[j] <= 1, (1)
478 * j in J
479 *
480 * where t[j] = x[j] or t[j] = 1 - x[j], x[j] is a binary variable,
481 * this routine translates it to CNF by replacing it with the following
482 * equivalent set of edge packing inequalities:
483 *
484 * t[j] + t[k] <= 1 for all j, k in J, j != k. (2)
485 *
486 * Then the routine transforms each edge packing inequality (2) to
487 * corresponding covering inequality (that encodes two-literal clause)
488 * by multiplying both its part by -1:
489 *
490 * - t[j] - t[k] >= -1 <--> (1 - t[j]) + (1 - t[k]) >= 1. (3)
491 *
492 * On exit the routine removes the original row from the problem. */
494 void npp_sat_encode_pack(NPP *npp, NPPROW *row)
495 { NPPROW *rrr;
496 NPPAIJ *aij, *aik;
497 /* original row should be packing inequality (1) */
498 xassert(npp_sat_is_pack_ineq(npp, row) == 1);
499 /* create equivalent system of covering inequalities (3) */
500 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
501 { /* due to symmetry only one of inequalities t[j] + t[k] <= 1
502 and t[k] <= t[j] <= 1 can be considered */
503 for (aik = aij->r_next; aik != NULL; aik = aik->r_next)
504 { /* create edge packing inequality (2) */
505 rrr = npp_add_row(npp);
506 rrr->lb = -DBL_MAX, rrr->ub = 1.0;
507 npp_add_aij(npp, rrr, aij->col, aij->val);
508 if (aij->val < 0.0)
509 rrr->ub -= 1.0;
510 npp_add_aij(npp, rrr, aik->col, aik->val);
511 if (aik->val < 0.0)
512 rrr->ub -= 1.0;
513 /* and transform it to covering inequality (3) */
514 npp_sat_reverse_row(npp, rrr);
515 xassert(npp_sat_is_cover_ineq(npp, rrr) == 1);
516 }
517 }
518 /* remove the original row from the problem */
519 npp_del_row(npp, row);
520 return;
521 }
523 /***********************************************************************
524 * npp_sat_encode_sum2 - encode 2-bit summation
525 *
526 * Given a set containing two literals x and y this routine encodes
527 * the equality
528 *
529 * x + y = s + 2 * c, (1)
530 *
531 * where
532 *
533 * s = (x + y) % 2 (2)
534 *
535 * is a binary variable modeling the low sum bit, and
536 *
537 * c = (x + y) / 2 (3)
538 *
539 * is a binary variable modeling the high (carry) sum bit. */
541 void npp_sat_encode_sum2(NPP *npp, NPPLSE *set, NPPSED *sed)
542 { NPPROW *row;
543 int x, y, s, c;
544 /* the set should contain exactly two literals */
545 xassert(set != NULL);
546 xassert(set->next != NULL);
547 xassert(set->next->next == NULL);
548 sed->x = set->lit;
549 xassert(sed->x.neg == 0 || sed->x.neg == 1);
550 sed->y = set->next->lit;
551 xassert(sed->y.neg == 0 || sed->y.neg == 1);
552 sed->z.col = NULL, sed->z.neg = 0;
553 /* perform encoding s = (x + y) % 2 */
554 sed->s = npp_add_col(npp);
555 sed->s->is_int = 1, sed->s->lb = 0.0, sed->s->ub = 1.0;
556 for (x = 0; x <= 1; x++)
557 { for (y = 0; y <= 1; y++)
558 { for (s = 0; s <= 1; s++)
559 { if ((x + y) % 2 != s)
560 { /* generate CNF clause to disable infeasible
561 combination */
562 row = npp_add_row(npp);
563 row->lb = 1.0, row->ub = +DBL_MAX;
564 if (x == sed->x.neg)
565 npp_add_aij(npp, row, sed->x.col, +1.0);
566 else
567 { npp_add_aij(npp, row, sed->x.col, -1.0);
568 row->lb -= 1.0;
569 }
570 if (y == sed->y.neg)
571 npp_add_aij(npp, row, sed->y.col, +1.0);
572 else
573 { npp_add_aij(npp, row, sed->y.col, -1.0);
574 row->lb -= 1.0;
575 }
576 if (s == 0)
577 npp_add_aij(npp, row, sed->s, +1.0);
578 else
579 { npp_add_aij(npp, row, sed->s, -1.0);
580 row->lb -= 1.0;
581 }
582 }
583 }
584 }
585 }
586 /* perform encoding c = (x + y) / 2 */
587 sed->c = npp_add_col(npp);
588 sed->c->is_int = 1, sed->c->lb = 0.0, sed->c->ub = 1.0;
589 for (x = 0; x <= 1; x++)
590 { for (y = 0; y <= 1; y++)
591 { for (c = 0; c <= 1; c++)
592 { if ((x + y) / 2 != c)
593 { /* generate CNF clause to disable infeasible
594 combination */
595 row = npp_add_row(npp);
596 row->lb = 1.0, row->ub = +DBL_MAX;
597 if (x == sed->x.neg)
598 npp_add_aij(npp, row, sed->x.col, +1.0);
599 else
600 { npp_add_aij(npp, row, sed->x.col, -1.0);
601 row->lb -= 1.0;
602 }
603 if (y == sed->y.neg)
604 npp_add_aij(npp, row, sed->y.col, +1.0);
605 else
606 { npp_add_aij(npp, row, sed->y.col, -1.0);
607 row->lb -= 1.0;
608 }
609 if (c == 0)
610 npp_add_aij(npp, row, sed->c, +1.0);
611 else
612 { npp_add_aij(npp, row, sed->c, -1.0);
613 row->lb -= 1.0;
614 }
615 }
616 }
617 }
618 }
619 return;
620 }
622 /***********************************************************************
623 * npp_sat_encode_sum3 - encode 3-bit summation
624 *
625 * Given a set containing at least three literals this routine chooses
626 * some literals x, y, z from that set and encodes the equality
627 *
628 * x + y + z = s + 2 * c, (1)
629 *
630 * where
631 *
632 * s = (x + y + z) % 2 (2)
633 *
634 * is a binary variable modeling the low sum bit, and
635 *
636 * c = (x + y + z) / 2 (3)
637 *
638 * is a binary variable modeling the high (carry) sum bit. */
640 void npp_sat_encode_sum3(NPP *npp, NPPLSE *set, NPPSED *sed)
641 { NPPROW *row;
642 int x, y, z, s, c;
643 /* the set should contain at least three literals */
644 xassert(set != NULL);
645 xassert(set->next != NULL);
646 xassert(set->next->next != NULL);
647 sed->x = set->lit;
648 xassert(sed->x.neg == 0 || sed->x.neg == 1);
649 sed->y = set->next->lit;
650 xassert(sed->y.neg == 0 || sed->y.neg == 1);
651 sed->z = set->next->next->lit;
652 xassert(sed->z.neg == 0 || sed->z.neg == 1);
653 /* perform encoding s = (x + y + z) % 2 */
654 sed->s = npp_add_col(npp);
655 sed->s->is_int = 1, sed->s->lb = 0.0, sed->s->ub = 1.0;
656 for (x = 0; x <= 1; x++)
657 { for (y = 0; y <= 1; y++)
658 { for (z = 0; z <= 1; z++)
659 { for (s = 0; s <= 1; s++)
660 { if ((x + y + z) % 2 != s)
661 { /* generate CNF clause to disable infeasible
662 combination */
663 row = npp_add_row(npp);
664 row->lb = 1.0, row->ub = +DBL_MAX;
665 if (x == sed->x.neg)
666 npp_add_aij(npp, row, sed->x.col, +1.0);
667 else
668 { npp_add_aij(npp, row, sed->x.col, -1.0);
669 row->lb -= 1.0;
670 }
671 if (y == sed->y.neg)
672 npp_add_aij(npp, row, sed->y.col, +1.0);
673 else
674 { npp_add_aij(npp, row, sed->y.col, -1.0);
675 row->lb -= 1.0;
676 }
677 if (z == sed->z.neg)
678 npp_add_aij(npp, row, sed->z.col, +1.0);
679 else
680 { npp_add_aij(npp, row, sed->z.col, -1.0);
681 row->lb -= 1.0;
682 }
683 if (s == 0)
684 npp_add_aij(npp, row, sed->s, +1.0);
685 else
686 { npp_add_aij(npp, row, sed->s, -1.0);
687 row->lb -= 1.0;
688 }
689 }
690 }
691 }
692 }
693 }
694 /* perform encoding c = (x + y + z) / 2 */
695 sed->c = npp_add_col(npp);
696 sed->c->is_int = 1, sed->c->lb = 0.0, sed->c->ub = 1.0;
697 for (x = 0; x <= 1; x++)
698 { for (y = 0; y <= 1; y++)
699 { for (z = 0; z <= 1; z++)
700 { for (c = 0; c <= 1; c++)
701 { if ((x + y + z) / 2 != c)
702 { /* generate CNF clause to disable infeasible
703 combination */
704 row = npp_add_row(npp);
705 row->lb = 1.0, row->ub = +DBL_MAX;
706 if (x == sed->x.neg)
707 npp_add_aij(npp, row, sed->x.col, +1.0);
708 else
709 { npp_add_aij(npp, row, sed->x.col, -1.0);
710 row->lb -= 1.0;
711 }
712 if (y == sed->y.neg)
713 npp_add_aij(npp, row, sed->y.col, +1.0);
714 else
715 { npp_add_aij(npp, row, sed->y.col, -1.0);
716 row->lb -= 1.0;
717 }
718 if (z == sed->z.neg)
719 npp_add_aij(npp, row, sed->z.col, +1.0);
720 else
721 { npp_add_aij(npp, row, sed->z.col, -1.0);
722 row->lb -= 1.0;
723 }
724 if (c == 0)
725 npp_add_aij(npp, row, sed->c, +1.0);
726 else
727 { npp_add_aij(npp, row, sed->c, -1.0);
728 row->lb -= 1.0;
729 }
730 }
731 }
732 }
733 }
734 }
735 return;
736 }
738 /***********************************************************************
739 * npp_sat_encode_sum_ax - encode linear combination of 0-1 variables
740 *
741 * PURPOSE
742 *
743 * Given a linear combination of binary variables:
744 *
745 * sum a[j] x[j], (1)
746 * j
747 *
748 * which is the linear form of the specified row, this routine encodes
749 * (i.e. translates to CNF) the following equality:
750 *
751 * n
752 * sum |a[j]| t[j] = sum 2**(k-1) * y[k], (2)
753 * j k=1
754 *
755 * where t[j] = x[j] (if a[j] > 0) or t[j] = 1 - x[j] (if a[j] < 0),
756 * and y[k] is either t[j] or a new literal created by the routine or
757 * a constant zero. Note that the sum in the right-hand side of (2) can
758 * be thought as a n-bit representation of the sum in the left-hand
759 * side, which is a non-negative integer number.
760 *
761 * ALGORITHM
762 *
763 * First, the number of bits, n, sufficient to represent any value in
764 * the left-hand side of (2) is determined. Obviously, n is the number
765 * of bits sufficient to represent the sum (sum |a[j]|).
766 *
767 * Let
768 *
769 * n
770 * |a[j]| = sum 2**(k-1) b[j,k], (3)
771 * k=1
772 *
773 * where b[j,k] is k-th bit in a n-bit representation of |a[j]|. Then
774 *
775 * m n
776 * sum |a[j]| * t[j] = sum 2**(k-1) sum b[j,k] * t[j]. (4)
777 * j k=1 j=1
778 *
779 * Introducing the set
780 *
781 * J[k] = { j : b[j,k] = 1 } (5)
782 *
783 * allows rewriting (4) as follows:
784 *
785 * n
786 * sum |a[j]| * t[j] = sum 2**(k-1) sum t[j]. (6)
787 * j k=1 j in J[k]
788 *
789 * Thus, our goal is to provide |J[k]| <= 1 for all k, in which case
790 * we will have the representation (1).
791 *
792 * Let |J[k]| = 2, i.e. J[k] has exactly two literals u and v. In this
793 * case we can apply the following transformation:
794 *
795 * u + v = s + 2 * c, (7)
796 *
797 * where s and c are, respectively, low (sum) and high (carry) bits of
798 * the sum of two bits. This allows to replace two literals u and v in
799 * J[k] by one literal s, and carry out literal c to J[k+1].
800 *
801 * If |J[k]| >= 3, i.e. J[k] has at least three literals u, v, and w,
802 * we can apply the following transformation:
803 *
804 * u + v + w = s + 2 * c. (8)
805 *
806 * Again, literal s replaces literals u, v, and w in J[k], and literal
807 * c goes into J[k+1].
808 *
809 * On exit the routine stores each literal from J[k] in element y[k],
810 * 1 <= k <= n. If J[k] is empty, y[k] is set to constant false.
811 *
812 * RETURNS
813 *
814 * The routine returns n, the number of literals in the right-hand side
815 * of (2), 0 <= n <= NBIT_MAX. If the sum (sum |a[j]|) is too large, so
816 * more than NBIT_MAX (= 31) literals are needed to encode the original
817 * linear combination, the routine returns a negative value. */
819 #define NBIT_MAX 31
820 /* maximal number of literals in the right hand-side of (2) */
822 static NPPLSE *remove_lse(NPP *npp, NPPLSE *set, NPPCOL *col)
823 { /* remove specified literal from specified literal set */
824 NPPLSE *lse, *prev = NULL;
825 for (lse = set; lse != NULL; prev = lse, lse = lse->next)
826 if (lse->lit.col == col) break;
827 xassert(lse != NULL);
828 if (prev == NULL)
829 set = lse->next;
830 else
831 prev->next = lse->next;
832 dmp_free_atom(npp->pool, lse, sizeof(NPPLSE));
833 return set;
834 }
836 int npp_sat_encode_sum_ax(NPP *npp, NPPROW *row, NPPLIT y[])
837 { NPPAIJ *aij;
838 NPPLSE *set[1+NBIT_MAX], *lse;
839 NPPSED sed;
840 int k, n, temp;
841 double sum;
842 /* compute the sum (sum |a[j]|) */
843 sum = 0.0;
844 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
845 sum += fabs(aij->val);
846 /* determine n, the number of bits in the sum */
847 temp = (int)sum;
848 if ((double)temp != sum)
849 return -1; /* integer arithmetic error */
850 for (n = 0; temp > 0; n++, temp >>= 1);
851 xassert(0 <= n && n <= NBIT_MAX);
852 /* build initial sets J[k], 1 <= k <= n; see (5) */
853 /* set[k] is a pointer to the list of literals in J[k] */
854 for (k = 1; k <= n; k++)
855 set[k] = NULL;
856 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
857 { temp = (int)fabs(aij->val);
858 xassert((int)temp == fabs(aij->val));
859 for (k = 1; temp > 0; k++, temp >>= 1)
860 { if (temp & 1)
861 { xassert(k <= n);
862 lse = dmp_get_atom(npp->pool, sizeof(NPPLSE));
863 lse->lit.col = aij->col;
864 lse->lit.neg = (aij->val > 0.0 ? 0 : 1);
865 lse->next = set[k];
866 set[k] = lse;
867 }
868 }
869 }
870 /* main transformation loop */
871 for (k = 1; k <= n; k++)
872 { /* reduce J[k] and set y[k] */
873 for (;;)
874 { if (set[k] == NULL)
875 { /* J[k] is empty */
876 /* set y[k] to constant false */
877 y[k].col = NULL, y[k].neg = 0;
878 break;
879 }
880 if (set[k]->next == NULL)
881 { /* J[k] contains one literal */
882 /* set y[k] to that literal */
883 y[k] = set[k]->lit;
884 dmp_free_atom(npp->pool, set[k], sizeof(NPPLSE));
885 break;
886 }
887 if (set[k]->next->next == NULL)
888 { /* J[k] contains two literals */
889 /* apply transformation (7) */
890 npp_sat_encode_sum2(npp, set[k], &sed);
891 }
892 else
893 { /* J[k] contains at least three literals */
894 /* apply transformation (8) */
895 npp_sat_encode_sum3(npp, set[k], &sed);
896 /* remove third literal from set[k] */
897 set[k] = remove_lse(npp, set[k], sed.z.col);
898 }
899 /* remove second literal from set[k] */
900 set[k] = remove_lse(npp, set[k], sed.y.col);
901 /* remove first literal from set[k] */
902 set[k] = remove_lse(npp, set[k], sed.x.col);
903 /* include new literal s to set[k] */
904 lse = dmp_get_atom(npp->pool, sizeof(NPPLSE));
905 lse->lit.col = sed.s, lse->lit.neg = 0;
906 lse->next = set[k];
907 set[k] = lse;
908 /* include new literal c to set[k+1] */
909 xassert(k < n); /* FIXME: can "overflow" happen? */
910 lse = dmp_get_atom(npp->pool, sizeof(NPPLSE));
911 lse->lit.col = sed.c, lse->lit.neg = 0;
912 lse->next = set[k+1];
913 set[k+1] = lse;
914 }
915 }
916 return n;
917 }
919 /***********************************************************************
920 * npp_sat_normalize_clause - normalize clause
921 *
922 * This routine normalizes the specified clause, which is a disjunction
923 * of literals, by replacing multiple literals, which refer to the same
924 * binary variable, with a single literal.
925 *
926 * On exit the routine returns the number of literals in the resulting
927 * clause. However, if the specified clause includes both a literal and
928 * its negation, the routine returns a negative value meaning that the
929 * clause is equivalent to the value true. */
931 int npp_sat_normalize_clause(NPP *npp, int size, NPPLIT lit[])
932 { int j, k, new_size;
933 xassert(npp == npp);
934 xassert(size >= 0);
935 new_size = 0;
936 for (k = 1; k <= size; k++)
937 { for (j = 1; j <= new_size; j++)
938 { if (lit[k].col == lit[j].col)
939 { /* lit[k] refers to the same variable as lit[j], which
940 is already included in the resulting clause */
941 if (lit[k].neg == lit[j].neg)
942 { /* ignore lit[k] due to the idempotent law */
943 goto skip;
944 }
945 else
946 { /* lit[k] is NOT lit[j]; the clause is equivalent to
947 the value true */
948 return -1;
949 }
950 }
951 }
952 /* include lit[k] in the resulting clause */
953 lit[++new_size] = lit[k];
954 skip: ;
955 }
956 return new_size;
957 }
959 /***********************************************************************
960 * npp_sat_encode_clause - translate clause to cover inequality
961 *
962 * Given a clause
963 *
964 * OR t[j], (1)
965 * j in J
966 *
967 * where t[j] is a literal, i.e. t[j] = x[j] or t[j] = NOT x[j], this
968 * routine translates it to the following equivalent cover inequality,
969 * which is added to the transformed problem:
970 *
971 * sum t[j] >= 1, (2)
972 * j in J
973 *
974 * where t[j] = x[j] or t[j] = 1 - x[j].
975 *
976 * If necessary, the clause should be normalized before a call to this
977 * routine. */
979 NPPROW *npp_sat_encode_clause(NPP *npp, int size, NPPLIT lit[])
980 { NPPROW *row;
981 int k;
982 xassert(size >= 1);
983 row = npp_add_row(npp);
984 row->lb = 1.0, row->ub = +DBL_MAX;
985 for (k = 1; k <= size; k++)
986 { xassert(lit[k].col != NULL);
987 if (lit[k].neg == 0)
988 npp_add_aij(npp, row, lit[k].col, +1.0);
989 else if (lit[k].neg == 1)
990 { npp_add_aij(npp, row, lit[k].col, -1.0);
991 row->lb -= 1.0;
992 }
993 else
994 xassert(lit != lit);
995 }
996 return row;
997 }
999 /***********************************************************************
1000 * npp_sat_encode_geq - encode "not less than" constraint
1001 *
1002 * PURPOSE
1003 *
1004 * This routine translates to CNF the following constraint:
1005 *
1006 * n
1007 * sum 2**(k-1) * y[k] >= b, (1)
1008 * k=1
1009 *
1010 * where y[k] is either a literal (i.e. y[k] = x[k] or y[k] = 1 - x[k])
1011 * or constant false (zero), b is a given lower bound.
1012 *
1013 * ALGORITHM
1014 *
1015 * If b < 0, the constraint is redundant, so assume that b >= 0. Let
1016 *
1017 * n
1018 * b = sum 2**(k-1) b[k], (2)
1019 * k=1
1020 *
1021 * where b[k] is k-th binary digit of b. (Note that if b >= 2**n and
1022 * therefore cannot be represented in the form (2), the constraint (1)
1023 * is infeasible.) In this case the condition (1) is equivalent to the
1024 * following condition:
1025 *
1026 * y[n] y[n-1] ... y[2] y[1] >= b[n] b[n-1] ... b[2] b[1], (3)
1027 *
1028 * where ">=" is understood lexicographically.
1029 *
1030 * Algorithmically the condition (3) can be tested as follows:
1031 *
1032 * for (k = n; k >= 1; k--)
1033 * { if (y[k] < b[k])
1034 * y is less than b;
1035 * if (y[k] > b[k])
1036 * y is greater than b;
1037 * }
1038 * y is equal to b;
1039 *
1040 * Thus, y is less than b iff there exists k, 1 <= k <= n, for which
1041 * the following condition is satisfied:
1042 *
1043 * y[n] = b[n] AND ... AND y[k+1] = b[k+1] AND y[k] < b[k]. (4)
1044 *
1045 * Negating the condition (4) we have that y is not less than b iff for
1046 * all k, 1 <= k <= n, the following condition is satisfied:
1047 *
1048 * y[n] != b[n] OR ... OR y[k+1] != b[k+1] OR y[k] >= b[k]. (5)
1049 *
1050 * Note that if b[k] = 0, the literal y[k] >= b[k] is always true, in
1051 * which case the entire clause (5) is true and can be omitted.
1052 *
1053 * RETURNS
1054 *
1055 * Normally the routine returns zero. However, if the constraint (1) is
1056 * infeasible, the routine returns non-zero. */
1058 int npp_sat_encode_geq(NPP *npp, int n, NPPLIT y[], int rhs)
1059 { NPPLIT lit[1+NBIT_MAX];
1060 int j, k, size, temp, b[1+NBIT_MAX];
1061 xassert(0 <= n && n <= NBIT_MAX);
1062 /* if the constraint (1) is redundant, do nothing */
1063 if (rhs < 0)
1064 return 0;
1065 /* determine binary digits of b according to (2) */
1066 for (k = 1, temp = rhs; k <= n; k++, temp >>= 1)
1067 b[k] = temp & 1;
1068 if (temp != 0)
1069 { /* b >= 2**n; the constraint (1) is infeasible */
1070 return 1;
1071 }
1072 /* main transformation loop */
1073 for (k = 1; k <= n; k++)
1074 { /* build the clause (5) for current k */
1075 size = 0; /* clause size = number of literals */
1076 /* add literal y[k] >= b[k] */
1077 if (b[k] == 0)
1078 { /* b[k] = 0 -> the literal is true */
1079 goto skip;
1080 }
1081 else if (y[k].col == NULL)
1082 { /* y[k] = 0, b[k] = 1 -> the literal is false */
1083 xassert(y[k].neg == 0);
1084 }
1085 else
1086 { /* add literal y[k] = 1 */
1087 lit[++size] = y[k];
1088 }
1089 for (j = k+1; j <= n; j++)
1090 { /* add literal y[j] != b[j] */
1091 if (y[j].col == NULL)
1092 { xassert(y[j].neg == 0);
1093 if (b[j] == 0)
1094 { /* y[j] = 0, b[j] = 0 -> the literal is false */
1095 continue;
1096 }
1097 else
1098 { /* y[j] = 0, b[j] = 1 -> the literal is true */
1099 goto skip;
1100 }
1101 }
1102 else
1103 { lit[++size] = y[j];
1104 if (b[j] != 0)
1105 lit[size].neg = 1 - lit[size].neg;
1106 }
1107 }
1108 /* normalize the clause */
1109 size = npp_sat_normalize_clause(npp, size, lit);
1110 if (size < 0)
1111 { /* the clause is equivalent to the value true */
1112 goto skip;
1113 }
1114 if (size == 0)
1115 { /* the clause is equivalent to the value false; this means
1116 that the constraint (1) is infeasible */
1117 return 2;
1118 }
1119 /* translate the clause to corresponding cover inequality */
1120 npp_sat_encode_clause(npp, size, lit);
1121 skip: ;
1122 }
1123 return 0;
1124 }
1126 /***********************************************************************
1127 * npp_sat_encode_leq - encode "not greater than" constraint
1128 *
1129 * PURPOSE
1130 *
1131 * This routine translates to CNF the following constraint:
1132 *
1133 * n
1134 * sum 2**(k-1) * y[k] <= b, (1)
1135 * k=1
1136 *
1137 * where y[k] is either a literal (i.e. y[k] = x[k] or y[k] = 1 - x[k])
1138 * or constant false (zero), b is a given upper bound.
1139 *
1140 * ALGORITHM
1141 *
1142 * If b < 0, the constraint is infeasible, so assume that b >= 0. Let
1143 *
1144 * n
1145 * b = sum 2**(k-1) b[k], (2)
1146 * k=1
1147 *
1148 * where b[k] is k-th binary digit of b. (Note that if b >= 2**n and
1149 * therefore cannot be represented in the form (2), the constraint (1)
1150 * is redundant.) In this case the condition (1) is equivalent to the
1151 * following condition:
1152 *
1153 * y[n] y[n-1] ... y[2] y[1] <= b[n] b[n-1] ... b[2] b[1], (3)
1154 *
1155 * where "<=" is understood lexicographically.
1156 *
1157 * Algorithmically the condition (3) can be tested as follows:
1158 *
1159 * for (k = n; k >= 1; k--)
1160 * { if (y[k] < b[k])
1161 * y is less than b;
1162 * if (y[k] > b[k])
1163 * y is greater than b;
1164 * }
1165 * y is equal to b;
1166 *
1167 * Thus, y is greater than b iff there exists k, 1 <= k <= n, for which
1168 * the following condition is satisfied:
1169 *
1170 * y[n] = b[n] AND ... AND y[k+1] = b[k+1] AND y[k] > b[k]. (4)
1171 *
1172 * Negating the condition (4) we have that y is not greater than b iff
1173 * for all k, 1 <= k <= n, the following condition is satisfied:
1174 *
1175 * y[n] != b[n] OR ... OR y[k+1] != b[k+1] OR y[k] <= b[k]. (5)
1176 *
1177 * Note that if b[k] = 1, the literal y[k] <= b[k] is always true, in
1178 * which case the entire clause (5) is true and can be omitted.
1179 *
1180 * RETURNS
1181 *
1182 * Normally the routine returns zero. However, if the constraint (1) is
1183 * infeasible, the routine returns non-zero. */
1185 int npp_sat_encode_leq(NPP *npp, int n, NPPLIT y[], int rhs)
1186 { NPPLIT lit[1+NBIT_MAX];
1187 int j, k, size, temp, b[1+NBIT_MAX];
1188 xassert(0 <= n && n <= NBIT_MAX);
1189 /* check if the constraint (1) is infeasible */
1190 if (rhs < 0)
1191 return 1;
1192 /* determine binary digits of b according to (2) */
1193 for (k = 1, temp = rhs; k <= n; k++, temp >>= 1)
1194 b[k] = temp & 1;
1195 if (temp != 0)
1196 { /* b >= 2**n; the constraint (1) is redundant */
1197 return 0;
1198 }
1199 /* main transformation loop */
1200 for (k = 1; k <= n; k++)
1201 { /* build the clause (5) for current k */
1202 size = 0; /* clause size = number of literals */
1203 /* add literal y[k] <= b[k] */
1204 if (b[k] == 1)
1205 { /* b[k] = 1 -> the literal is true */
1206 goto skip;
1207 }
1208 else if (y[k].col == NULL)
1209 { /* y[k] = 0, b[k] = 0 -> the literal is true */
1210 xassert(y[k].neg == 0);
1211 goto skip;
1212 }
1213 else
1214 { /* add literal y[k] = 0 */
1215 lit[++size] = y[k];
1216 lit[size].neg = 1 - lit[size].neg;
1217 }
1218 for (j = k+1; j <= n; j++)
1219 { /* add literal y[j] != b[j] */
1220 if (y[j].col == NULL)
1221 { xassert(y[j].neg == 0);
1222 if (b[j] == 0)
1223 { /* y[j] = 0, b[j] = 0 -> the literal is false */
1224 continue;
1225 }
1226 else
1227 { /* y[j] = 0, b[j] = 1 -> the literal is true */
1228 goto skip;
1229 }
1230 }
1231 else
1232 { lit[++size] = y[j];
1233 if (b[j] != 0)
1234 lit[size].neg = 1 - lit[size].neg;
1235 }
1236 }
1237 /* normalize the clause */
1238 size = npp_sat_normalize_clause(npp, size, lit);
1239 if (size < 0)
1240 { /* the clause is equivalent to the value true */
1241 goto skip;
1242 }
1243 if (size == 0)
1244 { /* the clause is equivalent to the value false; this means
1245 that the constraint (1) is infeasible */
1246 return 2;
1247 }
1248 /* translate the clause to corresponding cover inequality */
1249 npp_sat_encode_clause(npp, size, lit);
1250 skip: ;
1251 }
1252 return 0;
1253 }
1255 /***********************************************************************
1256 * npp_sat_encode_row - encode constraint (row) of general type
1257 *
1258 * PURPOSE
1259 *
1260 * This routine translates to CNF the following constraint (row):
1261 *
1262 * L <= sum a[j] x[j] <= U, (1)
1263 * j
1264 *
1265 * where all x[j] are binary variables.
1266 *
1267 * ALGORITHM
1268 *
1269 * First, the routine performs substitution x[j] = t[j] for j in J+
1270 * and x[j] = 1 - t[j] for j in J-, where J+ = { j : a[j] > 0 } and
1271 * J- = { j : a[j] < 0 }. This gives:
1272 *
1273 * L <= sum a[j] t[j] + sum a[j] (1 - t[j]) <= U ==>
1274 * j in J+ j in J-
1275 *
1276 * L' <= sum |a[j]| t[j] <= U', (2)
1277 * j
1278 *
1279 * where
1280 *
1281 * L' = L - sum a[j], U' = U - sum a[j]. (3)
1282 * j in J- j in J-
1283 *
1284 * (Actually only new bounds L' and U' are computed.)
1285 *
1286 * Then the routine translates to CNF the following equality:
1287 *
1288 * n
1289 * sum |a[j]| t[j] = sum 2**(k-1) * y[k], (4)
1290 * j k=1
1291 *
1292 * where y[k] is either some t[j] or a new literal or a constant zero
1293 * (see the routine npp_sat_encode_sum_ax).
1294 *
1295 * Finally, the routine translates to CNF the following conditions:
1296 *
1297 * n
1298 * sum 2**(k-1) * y[k] >= L' (5)
1299 * k=1
1300 *
1301 * and
1302 *
1303 * n
1304 * sum 2**(k-1) * y[k] <= U' (6)
1305 * k=1
1306 *
1307 * (see the routines npp_sat_encode_geq and npp_sat_encode_leq).
1308 *
1309 * All resulting clauses are encoded as cover inequalities and included
1310 * into the transformed problem.
1311 *
1312 * Note that on exit the routine removes the specified constraint (row)
1313 * from the original problem.
1314 *
1315 * RETURNS
1316 *
1317 * The routine returns one of the following codes:
1318 *
1319 * 0 - translation was successful;
1320 * 1 - constraint (1) was found infeasible;
1321 * 2 - integer arithmetic error occured. */
1323 int npp_sat_encode_row(NPP *npp, NPPROW *row)
1324 { NPPAIJ *aij;
1325 NPPLIT y[1+NBIT_MAX];
1326 int n, rhs;
1327 double lb, ub;
1328 /* the row should not be free */
1329 xassert(!(row->lb == -DBL_MAX && row->ub == +DBL_MAX));
1330 /* compute new bounds L' and U' (3) */
1331 lb = row->lb;
1332 ub = row->ub;
1333 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
1334 { if (aij->val < 0.0)
1335 { if (lb != -DBL_MAX)
1336 lb -= aij->val;
1337 if (ub != -DBL_MAX)
1338 ub -= aij->val;
1339 }
1340 }
1341 /* encode the equality (4) */
1342 n = npp_sat_encode_sum_ax(npp, row, y);
1343 if (n < 0)
1344 return 2; /* integer arithmetic error */
1345 /* encode the condition (5) */
1346 if (lb != -DBL_MAX)
1347 { rhs = (int)lb;
1348 if ((double)rhs != lb)
1349 return 2; /* integer arithmetic error */
1350 if (npp_sat_encode_geq(npp, n, y, rhs) != 0)
1351 return 1; /* original constraint is infeasible */
1352 }
1353 /* encode the condition (6) */
1354 if (ub != +DBL_MAX)
1355 { rhs = (int)ub;
1356 if ((double)rhs != ub)
1357 return 2; /* integer arithmetic error */
1358 if (npp_sat_encode_leq(npp, n, y, rhs) != 0)
1359 return 1; /* original constraint is infeasible */
1360 }
1361 /* remove the specified row from the problem */
1362 npp_del_row(npp, row);
1363 return 0;
1364 }
1366 /***********************************************************************
1367 * npp_sat_encode_prob - encode 0-1 feasibility problem
1368 *
1369 * This routine translates the specified 0-1 feasibility problem to an
1370 * equivalent SAT-CNF problem.
1371 *
1372 * N.B. Currently this is a very crude implementation.
1373 *
1374 * RETURNS
1375 *
1376 * 0 success;
1377 *
1378 * GLP_ENOPFS primal/integer infeasibility detected;
1379 *
1380 * GLP_ERANGE integer overflow occured. */
1382 int npp_sat_encode_prob(NPP *npp)
1383 { NPPROW *row, *next_row, *prev_row;
1384 NPPCOL *col, *next_col;
1385 int cover = 0, pack = 0, partn = 0, ret;
1386 /* process and remove free rows */
1387 for (row = npp->r_head; row != NULL; row = next_row)
1388 { next_row = row->next;
1389 if (row->lb == -DBL_MAX && row->ub == +DBL_MAX)
1390 npp_sat_free_row(npp, row);
1391 }
1392 /* process and remove fixed columns */
1393 for (col = npp->c_head; col != NULL; col = next_col)
1394 { next_col = col->next;
1395 if (col->lb == col->ub)
1396 xassert(npp_sat_fixed_col(npp, col) == 0);
1397 }
1398 /* only binary variables should remain */
1399 for (col = npp->c_head; col != NULL; col = col->next)
1400 xassert(col->is_int && col->lb == 0.0 && col->ub == 1.0);
1401 /* new rows may be added to the end of the row list, so we walk
1402 from the end to beginning of the list */
1403 for (row = npp->r_tail; row != NULL; row = prev_row)
1404 { prev_row = row->prev;
1405 /* process special cases */
1406 ret = npp_sat_is_cover_ineq(npp, row);
1407 if (ret != 0)
1408 { /* row is covering inequality */
1409 cover++;
1410 /* since it already encodes a clause, just transform it to
1411 canonical form */
1412 if (ret == 2)
1413 { xassert(npp_sat_reverse_row(npp, row) == 0);
1414 ret = npp_sat_is_cover_ineq(npp, row);
1415 }
1416 xassert(ret == 1);
1417 continue;
1418 }
1419 ret = npp_sat_is_partn_eq(npp, row);
1420 if (ret != 0)
1421 { /* row is partitioning equality */
1422 NPPROW *cov;
1423 NPPAIJ *aij;
1424 partn++;
1425 /* transform it to canonical form */
1426 if (ret == 2)
1427 { xassert(npp_sat_reverse_row(npp, row) == 0);
1428 ret = npp_sat_is_partn_eq(npp, row);
1429 }
1430 xassert(ret == 1);
1431 /* and split it into covering and packing inequalities,
1432 both in canonical forms */
1433 cov = npp_add_row(npp);
1434 cov->lb = row->lb, cov->ub = +DBL_MAX;
1435 for (aij = row->ptr; aij != NULL; aij = aij->r_next)
1436 npp_add_aij(npp, cov, aij->col, aij->val);
1437 xassert(npp_sat_is_cover_ineq(npp, cov) == 1);
1438 /* the cover inequality already encodes a clause and do
1439 not need any further processing */
1440 row->lb = -DBL_MAX;
1441 xassert(npp_sat_is_pack_ineq(npp, row) == 1);
1442 /* the packing inequality will be processed below */
1443 pack--;
1444 }
1445 ret = npp_sat_is_pack_ineq(npp, row);
1446 if (ret != 0)
1447 { /* row is packing inequality */
1448 NPPROW *rrr;
1449 int nlit, desired_nlit = 4;
1450 pack++;
1451 /* transform it to canonical form */
1452 if (ret == 2)
1453 { xassert(npp_sat_reverse_row(npp, row) == 0);
1454 ret = npp_sat_is_pack_ineq(npp, row);
1455 }
1456 xassert(ret == 1);
1457 /* process the packing inequality */
1458 for (;;)
1459 { /* determine the number of literals in the remaining
1460 inequality */
1461 nlit = npp_row_nnz(npp, row);
1462 if (nlit <= desired_nlit)
1463 break;
1464 /* split the current inequality into one having not more
1465 than desired_nlit literals and remaining one */
1466 rrr = npp_sat_split_pack(npp, row, desired_nlit-1);
1467 /* translate the former inequality to CNF and remove it
1468 from the original problem */
1469 npp_sat_encode_pack(npp, rrr);
1470 }
1471 /* translate the remaining inequality to CNF and remove it
1472 from the original problem */
1473 npp_sat_encode_pack(npp, row);
1474 continue;
1475 }
1476 /* translate row of general type to CNF and remove it from the
1477 original problem */
1478 ret = npp_sat_encode_row(npp, row);
1479 if (ret == 0)
1480 ;
1481 else if (ret == 1)
1482 ret = GLP_ENOPFS;
1483 else if (ret == 2)
1484 ret = GLP_ERANGE;
1485 else
1486 xassert(ret != ret);
1487 if (ret != 0)
1488 goto done;
1489 }
1490 ret = 0;
1491 if (cover != 0)
1492 xprintf("%d covering inequalities\n", cover);
1493 if (pack != 0)
1494 xprintf("%d packing inequalities\n", pack);
1495 if (partn != 0)
1496 xprintf("%d partitioning equalities\n", partn);
1497 done: return ret;
1498 }
1500 /* eof */