lemon-project-template-glpk

view deps/glpk/src/glpapi19.c @ 9:33de93886c88

find changesets by author, revision, files, or words in the commit message
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 /* glpapi19.c (driver to MiniSat solver) */
2
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 ***********************************************************************/
24
25 #include "glpapi.h"
26 #include "minisat/minisat.h"
27
28 int glp_minisat1(glp_prob *P)
29 { /* solve CNF-SAT problem with MiniSat solver */
30 solver *s;
31 GLPAIJ *aij;
32 int i, j, len, ret, *ind;
33 double sum;
34 /* check problem object */
35 if (P == NULL || P->magic != GLP_PROB_MAGIC)
36 xerror("glp_minisat1: P = %p; invalid problem object\n",
37 P);
38 if (P->tree != NULL)
39 xerror("glp_minisat1: operation not allowed\n");
40 /* integer solution is currently undefined */
41 P->mip_stat = GLP_UNDEF;
42 P->mip_obj = 0.0;
43 /* check that problem object encodes CNF-SAT instance */
44 if (glp_check_cnfsat(P) != 0)
45 { xprintf("glp_minisat1: problem object does not encode CNF-SAT "
46 "instance\n");
47 ret = GLP_EDATA;
48 goto done;
49 }
50 /* solve CNF-SAT problem */
51 xprintf("Solving CNF-SAT problem...\n");
52 xprintf("Instance has %d variable%s, %d clause%s, and %d literal%"
53 "s\n", P->n, P->n == 1 ? "" : "s", P->m, P->m == 1 ? "" : "s",
54 P->nnz, P->nnz == 1 ? "" : "s");
55 /* if CNF-SAT has no clauses, it is satisfiable */
56 if (P->m == 0)
57 { P->mip_stat = GLP_OPT;
58 for (j = 1; j <= P->n; j++)
59 P->col[j]->mipx = 0.0;
60 goto fini;
61 }
62 /* if CNF-SAT has an empty clause, it is unsatisfiable */
63 for (i = 1; i <= P->m; i++)
64 { if (P->row[i]->ptr == NULL)
65 { P->mip_stat = GLP_NOFEAS;
66 goto fini;
67 }
68 }
69 /* prepare input data for the solver */
70 s = solver_new();
71 solver_setnvars(s, P->n);
72 ind = xcalloc(1+P->n, sizeof(int));
73 for (i = 1; i <= P->m; i++)
74 { len = 0;
75 for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
76 { ind[++len] = toLit(aij->col->j-1);
77 if (aij->val < 0.0)
78 ind[len] = lit_neg(ind[len]);
79 }
80 xassert(len > 0);
81 xassert(solver_addclause(s, &ind[1], &ind[1+len]));
82 }
83 xfree(ind);
84 /* call the solver */
85 s->verbosity = 1;
86 if (solver_solve(s, 0, 0))
87 { /* instance is reported as satisfiable */
88 P->mip_stat = GLP_OPT;
89 /* copy solution to the problem object */
90 xassert(s->model.size == P->n);
91 for (j = 1; j <= P->n; j++)
92 { P->col[j]->mipx =
93 s->model.ptr[j-1] == l_True ? 1.0 : 0.0;
94 }
95 /* compute row values */
96 for (i = 1; i <= P->m; i++)
97 { sum = 0;
98 for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
99 sum += aij->val * aij->col->mipx;
100 P->row[i]->mipx = sum;
101 }
102 /* check integer feasibility */
103 for (i = 1; i <= P->m; i++)
104 { if (P->row[i]->mipx < P->row[i]->lb)
105 { /* solution is wrong */
106 P->mip_stat = GLP_UNDEF;
107 break;
108 }
109 }
110 }
111 else
112 { /* instance is reported as unsatisfiable */
113 P->mip_stat = GLP_NOFEAS;
114 }
115 solver_delete(s);
116 fini: /* report the instance status */
117 if (P->mip_stat == GLP_OPT)
118 { xprintf("SATISFIABLE\n");
119 ret = 0;
120 }
121 else if (P->mip_stat == GLP_NOFEAS)
122 { xprintf("UNSATISFIABLE\n");
123 ret = 0;
124 }
125 else
126 { xprintf("glp_minisat1: solver failed\n");
127 ret = GLP_EFAIL;
128 }
129 done: return ret;
130 }
131
132 /* eof */