1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/deps/glpk/src/glpapi19.c	Sun Nov 06 20:59:10 2011 +0100
     1.3 @@ -0,0 +1,132 @@
     1.4 +/* glpapi19.c (driver to MiniSat solver) */
     1.5 +
     1.6 +/***********************************************************************
     1.7 +*  This code is part of GLPK (GNU Linear Programming Kit).
     1.8 +*
     1.9 +*  Copyright (C) 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008,
    1.10 +*  2009, 2010, 2011 Andrew Makhorin, Department for Applied Informatics,
    1.11 +*  Moscow Aviation Institute, Moscow, Russia. All rights reserved.
    1.12 +*  E-mail: <mao@gnu.org>.
    1.13 +*
    1.14 +*  GLPK is free software: you can redistribute it and/or modify it
    1.15 +*  under the terms of the GNU General Public License as published by
    1.16 +*  the Free Software Foundation, either version 3 of the License, or
    1.17 +*  (at your option) any later version.
    1.18 +*
    1.19 +*  GLPK is distributed in the hope that it will be useful, but WITHOUT
    1.20 +*  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
    1.21 +*  or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
    1.22 +*  License for more details.
    1.23 +*
    1.24 +*  You should have received a copy of the GNU General Public License
    1.25 +*  along with GLPK. If not, see <http://www.gnu.org/licenses/>.
    1.26 +***********************************************************************/
    1.27 +
    1.28 +#include "glpapi.h"
    1.29 +#include "minisat/minisat.h"
    1.30 +
    1.31 +int glp_minisat1(glp_prob *P)
    1.32 +{     /* solve CNF-SAT problem with MiniSat solver */
    1.33 +      solver *s;
    1.34 +      GLPAIJ *aij;
    1.35 +      int i, j, len, ret, *ind;
    1.36 +      double sum;
    1.37 +      /* check problem object */
    1.38 +      if (P == NULL || P->magic != GLP_PROB_MAGIC)
    1.39 +         xerror("glp_minisat1: P = %p; invalid problem object\n",
    1.40 +            P);
    1.41 +      if (P->tree != NULL)
    1.42 +         xerror("glp_minisat1: operation not allowed\n");
    1.43 +      /* integer solution is currently undefined */
    1.44 +      P->mip_stat = GLP_UNDEF;
    1.45 +      P->mip_obj = 0.0;
    1.46 +      /* check that problem object encodes CNF-SAT instance */
    1.47 +      if (glp_check_cnfsat(P) != 0)
    1.48 +      {  xprintf("glp_minisat1: problem object does not encode CNF-SAT "
    1.49 +            "instance\n");
    1.50 +         ret = GLP_EDATA;
    1.51 +         goto done;
    1.52 +      }
    1.53 +      /* solve CNF-SAT problem */
    1.54 +      xprintf("Solving CNF-SAT problem...\n");
    1.55 +      xprintf("Instance has %d variable%s, %d clause%s, and %d literal%"
    1.56 +         "s\n", P->n, P->n == 1 ? "" : "s", P->m, P->m == 1 ? "" : "s",
    1.57 +         P->nnz, P->nnz == 1 ? "" : "s");
    1.58 +      /* if CNF-SAT has no clauses, it is satisfiable */
    1.59 +      if (P->m == 0)
    1.60 +      {  P->mip_stat = GLP_OPT;
    1.61 +         for (j = 1; j <= P->n; j++)
    1.62 +            P->col[j]->mipx = 0.0;
    1.63 +         goto fini;
    1.64 +      }
    1.65 +      /* if CNF-SAT has an empty clause, it is unsatisfiable */
    1.66 +      for (i = 1; i <= P->m; i++)
    1.67 +      {  if (P->row[i]->ptr == NULL)
    1.68 +         {  P->mip_stat = GLP_NOFEAS;
    1.69 +            goto fini;
    1.70 +         }
    1.71 +      }
    1.72 +      /* prepare input data for the solver */
    1.73 +      s = solver_new();
    1.74 +      solver_setnvars(s, P->n);
    1.75 +      ind = xcalloc(1+P->n, sizeof(int));
    1.76 +      for (i = 1; i <= P->m; i++)
    1.77 +      {  len = 0;
    1.78 +         for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
    1.79 +         {  ind[++len] = toLit(aij->col->j-1);
    1.80 +            if (aij->val < 0.0)
    1.81 +               ind[len] = lit_neg(ind[len]);
    1.82 +         }
    1.83 +         xassert(len > 0);
    1.84 +         xassert(solver_addclause(s, &ind[1], &ind[1+len]));
    1.85 +      }
    1.86 +      xfree(ind);
    1.87 +      /* call the solver */
    1.88 +      s->verbosity = 1;
    1.89 +      if (solver_solve(s, 0, 0))
    1.90 +      {  /* instance is reported as satisfiable */
    1.91 +         P->mip_stat = GLP_OPT;
    1.92 +         /* copy solution to the problem object */
    1.93 +         xassert(s->model.size == P->n);
    1.94 +         for (j = 1; j <= P->n; j++)
    1.95 +         {  P->col[j]->mipx =
    1.96 +               s->model.ptr[j-1] == l_True ? 1.0 : 0.0;
    1.97 +         }
    1.98 +         /* compute row values */
    1.99 +         for (i = 1; i <= P->m; i++)
   1.100 +         {  sum = 0;
   1.101 +            for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next)
   1.102 +               sum += aij->val * aij->col->mipx;
   1.103 +            P->row[i]->mipx = sum;
   1.104 +         }
   1.105 +         /* check integer feasibility */
   1.106 +         for (i = 1; i <= P->m; i++)
   1.107 +         {  if (P->row[i]->mipx < P->row[i]->lb)
   1.108 +            {  /* solution is wrong */
   1.109 +               P->mip_stat = GLP_UNDEF;
   1.110 +               break;
   1.111 +            }
   1.112 +         }
   1.113 +      }
   1.114 +      else
   1.115 +      {  /* instance is reported as unsatisfiable */
   1.116 +         P->mip_stat = GLP_NOFEAS;
   1.117 +      }
   1.118 +      solver_delete(s);
   1.119 +fini: /* report the instance status */
   1.120 +      if (P->mip_stat == GLP_OPT)
   1.121 +      {  xprintf("SATISFIABLE\n");
   1.122 +         ret = 0;
   1.123 +      }
   1.124 +      else if (P->mip_stat == GLP_NOFEAS)
   1.125 +      {  xprintf("UNSATISFIABLE\n");
   1.126 +         ret = 0;
   1.127 +      }
   1.128 +      else
   1.129 +      {  xprintf("glp_minisat1: solver failed\n");
   1.130 +         ret = GLP_EFAIL;
   1.131 +      }
   1.132 +done: return ret;
   1.133 +}
   1.134 +
   1.135 +/* eof */