backends/picosat/picomcs.c

   1 #include <assert.h>
   2 #include <stdlib.h>
   3 #include <stdio.h>
   4 #include <stdarg.h>
   5 #include <ctype.h>
   6 #include <string.h>
   7 #include <unistd.h>
   8
   9 #include "picosat.h"
  10
  11 typedef struct Clause { int cid, * lits; struct Clause * next; } Clause;
  12 typedef struct MCS { int mid, * clauses; struct MCS * next; } MCS;
  13
  14 static int nvars;
  15 static char * marked;
  16
  17 static Clause * first_clause, * last_clause;
  18 static int nclauses, first_cid, last_cid;
  19
  20 static MCS * first_mcs, * last_mcs;
  21 static int nmcs;
  22
  23 static int * stk, szstk, nstk;
  24
  25 static int verbose, join, noprint;
  26
  27 static int lineno = 1, close_input;
  28 static const char * input_name;
  29 static FILE * input;
  30
  31 static PicoSAT * ps;
  32
  33 static void release_clauses (void) {
  34   Clause * p, * next;
  35   for (p = first_clause; p; p = next) {
  36     next = p->next;
  37     free (p->lits);
  38     free (p);
  39   }
  40 }
  41
  42 static void release_mss (void) {
  43   MCS * p, * next;
  44   for (p = first_mcs; p; p = next) {
  45     next = p->next;
  46     free (p->clauses);
  47     free (p);
  48   }
  49 }
  50
  51 static void release (void) {
  52   release_clauses ();
  53   release_mss ();
  54   free (marked);
  55   free (stk);
  56 }
  57
  58 static void push_stack (int n) {
  59   if (nstk == szstk)
  60     stk = realloc (stk, (szstk = szstk ? 2*szstk : 1) * sizeof *stk);
  61   stk[nstk++] = n;
  62 }
  63
  64 static void push_clause (void) {
  65   Clause * clause;
  66   size_t bytes;
  67   clause = malloc (sizeof *clause);
  68   clause->cid = ++nclauses;
  69   clause->next = 0;
  70   push_stack (0);
  71   bytes = nstk * sizeof *clause->lits;
  72   clause->lits = malloc (bytes);
  73   memcpy (clause->lits, stk, bytes);
  74   if (last_clause) last_clause->next = clause;
  75   else first_clause = clause;
  76   last_clause = clause;
  77   nstk = 0;
  78 }
  79
  80 static void push_mcs (void) {
  81   MCS * mcs;
  82   size_t bytes;
  83   mcs = malloc (sizeof *mcs);
  84   mcs->mid = ++nmcs;
  85   mcs->next = 0;
  86   push_stack (0);
  87   bytes = nstk * sizeof *mcs->clauses;
  88   mcs->clauses = malloc (bytes);
  89   memcpy (mcs->clauses, stk, bytes);
  90   if (last_mcs) last_mcs->next = mcs;
  91   else first_mcs = mcs;
  92   last_mcs = mcs;
  93   nstk = 0;
  94 }
  95
  96 static int nextch (void) {
  97   int res = getc (input);
  98   if (res == '\n') lineno++;
  99   return res;
 100 }
 101
 102 static void msg (int level, const char * fmt, ...) {
 103   va_list ap;
 104   if (level > verbose) return;
 105   printf ("c [picomcs] ");
 106   va_start (ap, fmt);
 107   vprintf (fmt, ap);
 108   va_end (ap);
 109   fputc ('\n', stdout);
 110   fflush (stdout);
 111 }
 112
 113 static const char * parse (void) {
 114   int ch, expclauses, lit, sign;
 115   size_t bytes;
 116   msg (1, "parsing %s", input_name);
 117 COMMENTS:
 118   ch = nextch ();
 119   if (ch == 'c') {
 120     while ((ch = nextch ()) != '\n')
 121       if (ch == EOF) return "out of file in comment";
 122     goto COMMENTS;
 123   }
 124   if (ch != 'p')
 125 INVALID_HEADER:
 126     return "invalid header";
 127   ungetc (ch, input);
 128   if (fscanf (input, "p cnf %d %d", &nvars, &expclauses) != 2)
 129     goto INVALID_HEADER;
 130   msg (1, "found 'p cnf %d %d' header", nvars, expclauses);
 131   bytes = (1 + nvars + expclauses) * sizeof *marked;
 132   marked = malloc (bytes);
 133   memset (marked, 0, bytes);
 134 LIT:
 135   ch = nextch ();
 136   if (ch == ' '  || ch == '\n' || ch == '\t' || ch == '\r') goto LIT;
 137   if (ch == EOF) {
 138     assert (nclauses <= expclauses);
 139     if (nclauses < expclauses) return "clauses missing";
 140     return 0;
 141   }
 142   if (ch == '-') {
 143     ch = nextch ();
 144     if (!isdigit (ch)) return "expected digit after '-'";
 145     if (ch == '0') return "expected positive digit after '-'";
 146     sign = -1;
 147   } else if (!isdigit (ch)) return "expected '-' or digit";
 148   else sign = 1;
 149   lit = ch - '0';
 150   while (isdigit (ch = nextch ()))
 151     lit = 10*lit + (ch - '0');
 152   if (lit) {
 153     if (lit > nvars) return "maximum variable index exceeded";
 154     if (nclauses == expclauses) return "too many clauses";
 155     push_stack (sign * lit);
 156   } else {
 157     assert (nclauses < expclauses);
 158     push_clause ();
 159   }
 160   goto LIT;
 161 }
 162
 163 #ifndef NDEBUG
 164 static void dump_clause (Clause * c) {
 165   int * p, lit;
 166   for (p = c->lits; (lit = *p); p++)
 167     printf ("%d ", lit);
 168   printf ("0\n");
 169 }
 170
 171 void dump (void) {
 172   Clause * p;
 173   printf ("p cnf %d %d\n", nvars, nclauses);
 174   for (p = first_clause; p; p = p->next)
 175     dump_clause (p);
 176 }
 177 #endif
 178
 179 static int clause2selvar (Clause * c) {
 180   int res = c->cid + nvars;
 181   assert (first_cid <= res && res <= last_cid);
 182   return res;
 183 }
 184
 185 static void encode_clause (Clause * c) {
 186   int * p, lit;
 187   if (verbose >= 2) {
 188     printf ("c [picomcs] encode clause %d :", c->cid);
 189     printf (" %d", -clause2selvar (c));
 190     for (p = c->lits; (lit = *p); p++) printf (" %d", lit);
 191     fputc ('\n', stdout), fflush (stdout);
 192   }
 193   picosat_add (ps, -clause2selvar (c));
 194   for (p = c->lits; (lit = *p); p++) picosat_add (ps, lit);
 195   picosat_add (ps, 0);
 196 }
 197
 198 static void encode (void) {
 199   Clause * p;
 200   first_cid = nvars + 1;
 201   last_cid = nvars + nclauses;
 202   msg (2, "selector variables range %d to %d", first_cid, last_cid);
 203   for (p = first_clause; p; p = p->next)
 204     encode_clause (p);
 205   msg (1, "encoded %d clauses", nclauses);
 206 }
 207
 208 static void camcs (void) {
 209   int cid, i;
 210   const int * mcs, * p;
 211   msg (1, "starting to compute all minimal correcting sets");
 212   while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps))) {
 213     for (p = mcs; (cid = *p); p++)
 214       push_stack (cid);
 215     if (verbose >= 2) {
 216       printf ("c [picomcs] mcs %d :", nmcs);
 217       for (i = 0; i < nstk; i++) printf (" %d", stk[i] - nvars);
 218       fputc ('\n', stdout);
 219       fflush (stdout);
 220     } else if (verbose && isatty (1)) {
 221       printf ("\rc [picomcs] mcs %d", nmcs);
 222       fflush (stdout);
 223     }
 224     push_mcs ();
 225   }
 226   if (verbose && isatty (1)) fputc ('\r', stdout);
 227   msg (1, "found %d minimal correcting sets", nmcs);
 228 }
 229
 230 static void cumcscb (void * state, int nmcs, int nhumus) {
 231   int * ptr = state;
 232   *ptr = nmcs;
 233   ptr[0] = nmcs, ptr[1] = nhumus;
 234   if (!verbose || (!isatty (1) && verbose == 1)) return;
 235   if (verbose == 1) fputc ('\r', stdout);
 236   printf ("c [picomcs] mcs %d humus %d", nmcs, nhumus);
 237   if (verbose >= 2) fputc ('\n', stdout);
 238   fflush (stdout);
 239 }
 240
 241 static void cumcs (void) {
 242   int stats[2], count, cid;
 243   const int * humus, * p;
 244   stats[0] = stats[1] = 0;
 245   humus = picosat_humus (ps, cumcscb, stats);
 246   if (isatty (1) && verbose == 1) fputc ('\n', stdout);
 247   count = 0;
 248   for (p = humus; (cid = *p); p++) {
 249     if (marked[cid]) continue;
 250     marked[cid] = 1;
 251     count++;
 252   }
 253   assert (count == stats[1]);
 254   msg (1,
 255     "computed union of minimal correcting sets of size %d with %d mcs",
 256     stats[1], stats[0]);
 257 }
 258
 259 static void
 260 print_umcs (void) {
 261   int cid;
 262   printf ("v");
 263   for (cid = first_cid; cid <= last_cid; cid++)
 264     if (marked[cid])
 265       printf (" %d", cid - nvars);
 266   printf (" 0\n");
 267 }
 268
 269 static void
 270 print_mcs (MCS * mcs)
 271 {
 272   const int * p;
 273   int cid;
 274   printf ("v");
 275   for (p = mcs->clauses; (cid = *p); p++)
 276     printf (" %d", cid - nvars);
 277   printf (" 0\n");
 278 }
 279
 280 static void
 281 print_all_mcs (void)
 282 {
 283   MCS * p;
 284   for (p = first_mcs; p; p = p->next)
 285     print_mcs (p);
 286 }
 287
 288 int main (int argc, char ** argv) {
 289   const char * perr;
 290   int i, res;
 291   for (i = 1; i < argc; i++) {
 292     if (!strcmp (argv[i], "-h")) {
 293       printf ("usage: picomcs [-h][-v][-j][-n][<input>]\n");
 294       exit (0);
 295     }
 296     else if (!strcmp (argv[i], "-v")) verbose++;
 297     else if (!strcmp (argv[i], "-j")) join = 1;
 298     else if (!strcmp (argv[i], "-n")) noprint = 1;
 299     else if (argv[i][0] == '-') {
 300       fprintf (stderr, "*** picomcs: invalid option '%s'\n", argv[i]);
 301       exit (1);
 302     } else if (input_name) {
 303       fprintf (stderr, "*** picomcs: two input files specified\n");
 304       exit (1);
 305     } else if (!(input = fopen ((input_name = argv[i]), "r"))) {
 306       fprintf (stderr, "*** picomcs: can not read '%s'\n", argv[i]);
 307       exit (1);
 308     } else close_input = 1;
 309   }
 310   if (!input_name) input_name = "<stdin>", input = stdin;
 311   if ((perr = parse ())) {
 312     fprintf (stderr, "%s:%d: parse error: %s\n", input_name, lineno, perr);
 313     exit (1);
 314   }
 315   if (close_input) fclose (input);
 316   ps = picosat_init ();
 317   picosat_set_prefix (ps, "c [picosat] ");
 318   encode ();
 319   for (i = first_cid; i <= last_cid; i++)
 320     picosat_set_default_phase_lit (ps, i, 1);
 321   for (i = first_cid; i <= last_cid; i++) picosat_assume (ps, i);
 322   res = picosat_sat (ps, -1);
 323   if (res == 10) printf ("s SATISFIABLE\n");
 324   else printf ("s UNSATISFIABLE\n");
 325   fflush (stdout);
 326   if (join) cumcs (); else camcs ();
 327   if (verbose) picosat_stats (ps);
 328   picosat_reset (ps);
 329   if (!noprint) {
 330     if (join) print_umcs (); else print_all_mcs ();
 331   }
 332   release ();
 333   return res;
 334 }