backends/picosat/picomus.c

   1 /****************************************************************************
   2 Copyright (c) 2011-2014, Armin Biere, Johannes Kepler University.
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy
   5 of this software and associated documentation files (the "Software"), to
   6 deal in the Software without restriction, including without limitation the
   7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
   8 sell copies of the Software, and to permit persons to whom the Software is
   9 furnished to do so, subject to the following conditions:
  10
  11 The above copyright notice and this permission notice shall be included in
  12 all copies or substantial portions of the Software.
  13
  14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
  17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
  20 IN THE SOFTWARE.
  21 ****************************************************************************/
  22
  23 #include "picosat.h"
  24
  25 #include <stdio.h>
  26 #include <assert.h>
  27 #include <string.h>
  28 #include <stdarg.h>
  29 #include <ctype.h>
  30
  31 #define MAXNONREDROUNDS 3
  32 #define MINCOREROUNDS 5
  33 #define MAXCOREROUNDS 100
  34
  35 typedef struct Cls { int lit, red, * lits; } Cls;
  36
  37 static int verbose, nowitness;
  38 static int fclose_input, pclose_input, close_output;
  39 static FILE * input_file, * output_file;
  40 static const char * input_name, * output_name;
  41 static int lineno = 1;
  42 static int nvars, nclauses;
  43 static Cls * clauses;
  44 static int * lits, nlits, szlits;
  45 static double start;
  46 static int reductions;
  47
  48 static PicoSAT * ps;
  49
  50 static int next (void) {
  51   int res = fgetc (input_file);
  52   if (res == '\n') lineno++;
  53   return res;
  54 }
  55
  56 static void msg (int level, const char * fmt, ...) {
  57   va_list ap;
  58   if (verbose < level) return;
  59   fputs ("c [picomus] ", stdout);
  60   va_start (ap, fmt);
  61   vfprintf (stdout, fmt, ap);
  62   va_end (ap);
  63   fputc ('\n', stdout);
  64   fflush (stdout);
  65 }
  66
  67 static void warn (const char * fmt, ...) {
  68   va_list ap;
  69   if (verbose < 0) return;
  70   fputs ("c [picomus] WARNING: ", stdout);
  71   va_start (ap, fmt);
  72   vfprintf (stdout, fmt, ap);
  73   va_end (ap);
  74   fputc ('\n', stdout);
  75   fflush (stdout);
  76 }
  77
  78 static const char * parse (void) {
  79   int ch, n, lit, sign, i;
  80   Cls * c;
  81 HEADER:
  82   ch = next ();
  83   if (ch == 'c') {
  84     while ((ch = next ()) != '\n')
  85       if (ch == EOF) return "EOF after 'c'";
  86     goto HEADER;
  87   }
  88   if (ch == '\r') goto HEADER;
  89   if (ch != 'p') return "expected 'c' or 'p'";
  90   if (fscanf (input_file, " cnf %d %d", &nvars, &nclauses) != 2)
  91     return "invalid header";
  92   msg (1, "p cnf %d %d", nvars, nclauses);
  93   clauses = calloc (nclauses, sizeof *clauses);
  94   lit = n = 0;
  95 LIT:
  96   ch = next ();
  97   if (ch == ' ' || ch == '\n' || ch == '\t' || ch == '\r') goto LIT;
  98   if (ch == 'c') {
  99     while ((ch = next ()) != '\n')
 100       if (ch == EOF) return "EOF after 'c'";
 101     goto LIT;
 102   }
 103   if (ch == EOF) {
 104     if (lit) return "zero missing";
 105     if (n < nclauses) return "clauses missing";
 106     return 0;
 107   }
 108   if (n == nclauses) return "too many clauses";
 109   if (ch == '-') {
 110     sign = -1;
 111     ch = next ();
 112     if (!isdigit (ch)) return "expected digit after '-'";
 113   } else sign = 1;
 114   if (!isdigit (ch)) return "expected digit";
 115   lit = ch - '0';
 116   while (isdigit (ch = next ()))
 117     lit = 10 * lit + (ch - '0');
 118   if (lit > nvars) return "maximum variable index exceeded";
 119   if (lit) {
 120     lit *= sign;
 121     if (nlits == szlits) {
 122       szlits = szlits ? 2 * szlits : 1;
 123       lits = realloc (lits, szlits * sizeof *lits);
 124     }
 125     lits[nlits++] = lit;
 126   } else {
 127     c = clauses + n++;
 128     c->lits = malloc ((nlits + 1) * sizeof *c->lits);
 129     for (i = 0; i < nlits; i++)
 130       c->lits[i] = lits[i];
 131     c->lits[i] = 0;
 132     nlits = 0;
 133   }
 134   goto LIT;
 135 }
 136
 137 static void die (const char * fmt, ...) {
 138   va_list ap;
 139   fputs ("*** picomus: ", stdout);
 140   va_start (ap, fmt);
 141   vfprintf (stdout, fmt, ap);
 142   va_end (ap);
 143   fputc ('\n', stdout);
 144   fflush (stdout);
 145   exit (1);
 146 }
 147
 148 static double percent (double a, double b) { return b?100.0*a/b:0.0; }
 149
 150 static void callback (void * dummy, const int * mus) {
 151   int remaining;
 152   const int * p;
 153   (void) dummy;
 154   if (verbose <= 0) return;
 155   remaining = 0;
 156   for (p = mus; *p; p++) remaining++;
 157   assert (remaining <= nclauses);
 158   reductions++;
 159   msg (1, "reduction %d to %d = %.0f%% out of %d after %.1f sec",
 160        reductions,
 161        remaining, percent (remaining, nclauses), nclauses,
 162        picosat_time_stamp () - start);
 163 }
 164
 165 static const char * USAGE =
 166 "picomus [-h][-v][-q] [ <input> [ <output> ] ]\n"
 167 "\n"
 168 "  -h  print this command line option summary\n"
 169 "  -v  increase verbosity level (default 0 = no messages)\n"
 170 "  -q  be quiet (no warnings nor messages)\n"
 171 "\n"
 172 "This tool is a SAT solver that uses the PicoSAT library to\n"
 173 "generate a 'minimal unsatisfiable core' also known as 'minimal\n"
 174 "unsatisfiable set' (MUS) of a CNF in DIMACS format.\n"
 175 "\n"
 176 "Both file arguments can be \"-\" and then denote <stdin> and\n"
 177 "<stdout> respectively.  If no input file is given <stdin> is used.\n"
 178 "If no output file is specified the MUS is computed and only printed\n"
 179 "to <stdout> in the format of the SAT competition 2011 MUS track.\n"
 180 "\n"
 181 "Note, that the 's ...' lines and in case the instance is satisfiable\n"
 182 "also the 'v ...' lines for the satisfying assignment are always\n"
 183 "printed to <stdout> (or not printed at all with '-q').\n"
 184 "\n"
 185 "If '-n' is specified satisfying assignment and MUS printing\n"
 186 "on <stdout> (using the 'v ...' format) is suppressed.\n"
 187 "The 's ...' line is still printed unless '-q' is specified.\n"
 188 "If <output> is specified an MUS is written to this file,\n"
 189 "even if '-n' or '-q' is used.\n"
 190 "\n"
 191 #ifndef TRACE
 192 "WARNING: PicosSAT is compiled without trace support.\n"
 193 "\n"
 194 "This typically slows down this MUS extractor, since\n"
 195 "it only relies on clause selector variables and\n"
 196 "can not make use of core extraction.  To enable\n"
 197 "trace generation use './configure.sh --trace' or\n"
 198 "'./configure.sh -O --trace' when building PicoSAT.\n"
 199 #else
 200 "Since trace generation code is included, this binary\n"
 201 "uses also core extraction in addition to clause selector\n"
 202 "variables.\n"
 203 #endif
 204 ;
 205
 206 int main (int argc, char ** argv) {
 207   int i, * p, n, oldn, red, nonred, res, round, printed, len;
 208   const char * err;
 209   const int * q;
 210   char * cmd;
 211   Cls * c;
 212 #ifndef NDEBUG
 213   int tmp;
 214 #endif
 215   start = picosat_time_stamp ();
 216   for (i = 1; i < argc; i++) {
 217     if (!strcmp (argv[i], "-h")) {
 218       fputs (USAGE, stdout);
 219       exit (0);
 220     } else if (!strcmp (argv[i], "-v")) {
 221       if (verbose < 0) die ("'-v' option after '-q'");
 222       verbose++;
 223     } else if (!strcmp (argv[i], "-q")) {
 224       if (verbose < 0) die ("two '-q' options");
 225       if (verbose > 0) die ("'-q' option after '-v'");
 226       verbose = -1;
 227     } else if (!strcmp (argv[i], "-n")) nowitness = 1;
 228     else if (argv[i][0] == '-' && argv[i][1])
 229       die ("invalid command line option '%s'", argv[i]);
 230     else if (output_name) die ("too many arguments");
 231     else if (!input_name) input_name = argv[i];
 232     else output_name = argv[i];
 233   }
 234   if (!output_name) warn ("no output file given");
 235   if (input_name && strcmp (input_name, "-")) {
 236     len = strlen (input_name);
 237     if (len >= 3 && !strcmp (input_name + len - 3, ".gz")) {
 238       cmd = malloc (len + 20);
 239       sprintf (cmd, "gunzip -c %s 2>/dev/null", input_name);
 240       input_file = popen (cmd, "r");
 241       pclose_input = 1;
 242       free (cmd);
 243     } else input_file = fopen (input_name, "r"), fclose_input = 1;
 244     if (!input_file) die ("can not read '%s'", input_name);
 245   } else input_file = stdin, input_name = "-";
 246   if ((err =  parse ())) {
 247     fprintf (stdout, "%s:%d: %s\n", input_name, lineno, err);
 248     fflush (stdout);
 249     exit (1);
 250   }
 251   if (fclose_input) fclose (input_file);
 252   if (pclose_input) pclose (input_file);
 253   ps = picosat_init ();
 254   picosat_set_prefix (ps, "c [picosat] ");
 255   picosat_set_output (ps, stdout);
 256   if (verbose > 1) picosat_set_verbosity (ps, verbose - 1);
 257   printed = 0;
 258   if (!picosat_enable_trace_generation (ps))
 259     warn ("PicoSAT compiled without trace generation"),
 260     warn ("core extraction disabled");
 261   else {
 262     n = nclauses;
 263     nonred = 0;
 264     for (round = 1; round <= MAXCOREROUNDS; round++) {
 265       if (verbose > 1)
 266         msg (1, "starting core extraction round %d", round);
 267       picosat_set_seed (ps, round);
 268       for (i = 0; i < nclauses; i++) {
 269         c = clauses + i;
 270         if (c->red) {
 271           picosat_add (ps, 1);
 272           picosat_add (ps, -1);
 273         } else {
 274           for (p = c->lits; *p; p++)
 275             picosat_add (ps, *p);
 276         }
 277 #ifndef NDEBUG
 278         tmp =
 279 #endif
 280         picosat_add (ps, 0);
 281         assert (tmp == i);
 282       }
 283       res = picosat_sat (ps, -1);
 284       if (res == 10) { assert (round == 1); goto SAT; }
 285       assert (res == 20);
 286       if (!printed) {
 287         assert (round == 1);
 288         printed = 1;
 289         if (verbose >= 0)
 290           printf ("s UNSATISFIABLE\n"),
 291           fflush (stdout);
 292       }
 293       for (i = 0; i < nclauses; i++) {
 294         c = clauses + i;
 295         if (c->red) { assert (!picosat_coreclause (ps, i)); continue; }
 296         if (picosat_coreclause (ps, i)) continue;
 297         c->red = 1;
 298       }
 299       oldn = n;
 300       n = 0;
 301       for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++;
 302       msg (1, "extracted core %d of size %d = %0.f%% out of %d after %.1f sec",
 303            round, n, percent (n, nclauses), nclauses,
 304            picosat_time_stamp () - start);
 305       assert (oldn >= n);
 306       picosat_reset (ps);
 307       ps = picosat_init ();
 308       picosat_set_prefix (ps, "c [picosat] ");
 309       picosat_set_output (ps, stdout);
 310       if (round >= MINCOREROUNDS) {
 311         red = oldn - n;
 312         if (red < 10 && (100*red + 99)/oldn < 2) {
 313           nonred++;
 314           if (nonred > MAXNONREDROUNDS) break;
 315         }
 316       }
 317       if (round < MAXCOREROUNDS) picosat_enable_trace_generation (ps);
 318     }
 319   }
 320   for (i = 0; i < nclauses; i++) {
 321     c = clauses + i;
 322     if (c->red) {
 323       picosat_add (ps, 1);
 324       picosat_add (ps, -1);
 325 #ifndef NDEBUG
 326       tmp =
 327 #endif
 328       picosat_add (ps, 0);
 329       assert (tmp == i);
 330       continue;
 331     }
 332     c->lit = nvars + i + 1;
 333     picosat_add (ps, -c->lit);
 334     for (p = c->lits; *p; p++)
 335       (void) picosat_add (ps, *p);
 336 #ifndef NDEBUG
 337     tmp =
 338 #endif
 339     picosat_add (ps, 0);
 340     assert (tmp == i);
 341   }
 342   for (i = 0; i < nclauses; i++) {
 343     c = clauses + i;
 344     if (c->red) continue;
 345     picosat_assume (ps, c->lit);
 346   }
 347   res = picosat_sat (ps, -1);
 348   if (res == 20) {
 349     if (!printed && verbose >= 0)
 350       printf ("s UNSATISFIABLE\n"), fflush (stdout);
 351     for (i = 0; i < nclauses; i++) clauses[i].red = 1;
 352     q = picosat_mus_assumptions (ps, 0, callback, 1);
 353     while ((i = *q++)) {
 354       i -= nvars + 1;
 355       assert (0 <= i && i < nclauses);
 356       clauses[i].red = 0;
 357     }
 358   } else {
 359 SAT:
 360     assert (res == 10);
 361     if (!printed && verbose >= 0)
 362       printf ("s SATISFIABLE\n"), fflush (stdout);
 363     if (!nowitness && verbose >= 0) {
 364       for (i = 1; i <= nvars; i++)
 365         printf ("v %d\n", ((picosat_deref (ps, i) < 0) ? -1 : 1) * i);
 366       printf ("v 0\n");
 367     }
 368   }
 369   if (verbose > 0) picosat_stats (ps);
 370   picosat_reset (ps);
 371   n = 0;
 372   for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++;
 373   red = nclauses - n;
 374   msg (1, "found %d redundant clauses %.0f%%", red, percent (red, nclauses));
 375   if (res == 20)
 376     msg (0, "computed MUS of size %d out of %d (%.0f%%)",
 377          n, nclauses, percent (n, nclauses));
 378   if (output_name && strcmp (output_name, "-")) {
 379     output_file = fopen (output_name, "w");
 380     if (!output_file) die ("can not write '%s'", output_name);
 381     close_output = 1;
 382   } else if (output_name && !strcmp (output_name, "-")) output_file = stdout;
 383   if (output_file) {
 384     fprintf (output_file, "p cnf %d %d\n", nvars, n);
 385     for (i = 0; i < nclauses; i++)
 386       if (!clauses[i].red) {
 387         for (p = clauses[i].lits; *p; p++) fprintf (output_file, "%d ", *p);
 388         fprintf (output_file, "0\n");
 389       }
 390     if (close_output) fclose (output_file);
 391   }
 392   if (res == 20) {
 393     if (!nowitness && verbose >= 0) {
 394       for (i = 0; i < nclauses; i++)
 395         if (!clauses[i].red) printf ("v %d\n", i+1);
 396       printf ("v 0\n");
 397     }
 398   }
 399   msg (1, "%s %d irredundant clauses %.0f%%",
 400        output_file ? "printed" : "computed", n, percent (n, nclauses));
 401   for (i = 0; i < nclauses; i++) free (clauses[i].lits);
 402   free (clauses);
 403   free (lits);
 404   msg (1, "%d reductions in %.1f seconds",
 405        reductions, picosat_time_stamp () - start);
 406   return res;
 407 }