lemon-project-template-glpk

annotate deps/glpk/src/glpapi19.c @ 11:4fc6ad2fb8a6

find changesets by author, revision, files, or words in the commit message
Test GLPK in src/main.cc
author Alpar Juttner <alpar@cs.elte.hu>
date Sun, 06 Nov 2011 21:43:29 +0100
parents
children
rev   line source
alpar@9 1 /* glpapi19.c (driver to MiniSat solver) */
alpar@9 2
alpar@9 3 /***********************************************************************
alpar@9 4 * This code is part of GLPK (GNU Linear Programming Kit).
alpar@9 5 *
alpar@9 6 * Copyright (C) 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008,
alpar@9 7 * 2009, 2010, 2011 Andrew Makhorin, Department for Applied Informatics,
alpar@9 8 * Moscow Aviation Institute, Moscow, Russia. All rights reserved.
alpar@9 9 * E-mail: <mao@gnu.org>.
alpar@9 10 *
alpar@9 11 * GLPK is free software: you can redistribute it and/or modify it
alpar@9 12 * under the terms of the GNU General Public License as published by
alpar@9 13 * the Free Software Foundation, either version 3 of the License, or
alpar@9 14 * (at your option) any later version.
alpar@9 15 *
alpar@9 16 * GLPK is distributed in the hope that it will be useful, but WITHOUT
alpar@9 17 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
alpar@9 18 * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
alpar@9 19 * License for more details.
alpar@9 20 *
alpar@9 21 * You should have received a copy of the GNU General Public License
alpar@9 22 * along with GLPK. If not, see <http://www.gnu.org/licenses/>.
alpar@9 23 ***********************************************************************/
alpar@9 24
alpar@9 25 #include "glpapi.h"
alpar@9 26 #include "minisat/minisat.h"
alpar@9 27
alpar@9 28 int glp_minisat1(glp_prob *P)
alpar@9 29 { /* solve CNF-SAT problem with MiniSat solver */
alpar@9 30 solver *s;
alpar@9 31 GLPAIJ *aij;
alpar@9 32 int i, j, len, ret, *ind;
alpar@9 33 double sum;
alpar@9 34 /* check problem object */
alpar@9 35 if (P == NULL || P->magic != GLP_PROB_MAGIC)
alpar@9 36 xerror("glp_minisat1: P = %p; invalid problem object\n",
alpar@9 37 P);
alpar@9 38 if (P->tree != NULL)
alpar@9 39 xerror("glp_minisat1: operation not allowed\n");
alpar@9 40 /* integer solution is currently undefined */
alpar@9 41 P->mip_stat = GLP_UNDEF;
alpar@9 42 P->mip_obj = 0.0;
alpar@9 43 /* check that problem object encodes CNF-SAT instance */
alpar@9 44 if (glp_check_cnfsat(P) != 0)
alpar@9 45 { xprintf("glp_minisat1: problem object does not encode CNF-SAT "
alpar@9 46 "instance\n");
alpar@9 47 ret = GLP_EDATA;
alpar@9 48 goto done;
alpar@9 49 }
alpar@9 50 /* solve CNF-SAT problem */
alpar@9 51 xprintf("Solving CNF-SAT problem...\n");
alpar@9 52 xprintf("Instance has %d variable%s, %d clause%s, and %d literal%"
alpar@9 53 "s\n", P->n, P->n == 1 ? "" : "s", P->m, P->m == 1 ? "" : "s",
alpar@9 54 P->nnz, P->nnz == 1 ? "" : "s");
alpar@9 55 /* if CNF-SAT has no clauses, it is satisfiable */
alpar@9 56 if (P->m == 0)
alpar@9 57 { P->mip_stat = GLP_OPT;
alpar@9 58 for (j = 1; j <= P->n; j++)
alpar@9 59 P->col[j]->mipx = 0.0;
alpar@9 60 goto fini;
alpar@9 61 }
alpar@9 62 /* if CNF-SAT has an empty clause, it is unsatisfiable */
alpar@9 63 for (i = 1; i <= P->m; i++)
alpar@9 64 { if (P->row[i]->ptr == NULL)
alpar@9 65 { P->mip_stat = GLP_NOFEAS;
alpar@9 66 goto fini;
alpar@9 67 }
alpar@9 68 }
alpar@9 69 /* prepare input data for the solver */
alpar@9 70 s = solver_new();
alpar@9 71 solver_setnvars(s, P->n);
alpar@9 72 ind = xcalloc(1+P->n, sizeof(int));
alpar@9 73 for (i = 1; i <= P->m; i++)
alpar@9 74 { len = 0;
alpar@9 75 for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
alpar@9 76 { ind[++len] = toLit(aij->col->j-1);
alpar@9 77 if (aij->val < 0.0)
alpar@9 78 ind[len] = lit_neg(ind[len]);
alpar@9 79 }
alpar@9 80 xassert(len > 0);
alpar@9 81 xassert(solver_addclause(s, &ind[1], &ind[1+len]));
alpar@9 82 }
alpar@9 83 xfree(ind);
alpar@9 84 /* call the solver */
alpar@9 85 s->verbosity = 1;
alpar@9 86 if (solver_solve(s, 0, 0))
alpar@9 87 { /* instance is reported as satisfiable */
alpar@9 88 P->mip_stat = GLP_OPT;
alpar@9 89 /* copy solution to the problem object */
alpar@9 90 xassert(s->model.size == P->n);
alpar@9 91 for (j = 1; j <= P->n; j++)
alpar@9 92 { P->col[j]->mipx =
alpar@9 93 s->model.ptr[j-1] == l_True ? 1.0 : 0.0;
alpar@9 94 }
alpar@9 95 /* compute row values */
alpar@9 96 for (i = 1; i <= P->m; i++)
alpar@9 97 { sum = 0;
alpar@9 98 for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
alpar@9 99 sum += aij->val * aij->col->mipx;
alpar@9 100 P->row[i]->mipx = sum;
alpar@9 101 }
alpar@9 102 /* check integer feasibility */
alpar@9 103 for (i = 1; i <= P->m; i++)
alpar@9 104 { if (P->row[i]->mipx < P->row[i]->lb)
alpar@9 105 { /* solution is wrong */
alpar@9 106 P->mip_stat = GLP_UNDEF;
alpar@9 107 break;
alpar@9 108 }
alpar@9 109 }
alpar@9 110 }
alpar@9 111 else
alpar@9 112 { /* instance is reported as unsatisfiable */
alpar@9 113 P->mip_stat = GLP_NOFEAS;
alpar@9 114 }
alpar@9 115 solver_delete(s);
alpar@9 116 fini: /* report the instance status */
alpar@9 117 if (P->mip_stat == GLP_OPT)
alpar@9 118 { xprintf("SATISFIABLE\n");
alpar@9 119 ret = 0;
alpar@9 120 }
alpar@9 121 else if (P->mip_stat == GLP_NOFEAS)
alpar@9 122 { xprintf("UNSATISFIABLE\n");
alpar@9 123 ret = 0;
alpar@9 124 }
alpar@9 125 else
alpar@9 126 { xprintf("glp_minisat1: solver failed\n");
alpar@9 127 ret = GLP_EFAIL;
alpar@9 128 }
alpar@9 129 done: return ret;
alpar@9 130 }
alpar@9 131
alpar@9 132 /* eof */