diff options
Diffstat (limited to 'scripts/picosat-959/picomus.c')
-rw-r--r-- | scripts/picosat-959/picomus.c | 385 |
1 files changed, 385 insertions, 0 deletions
diff --git a/scripts/picosat-959/picomus.c b/scripts/picosat-959/picomus.c new file mode 100644 index 0000000..0f2784f --- /dev/null +++ b/scripts/picosat-959/picomus.c @@ -0,0 +1,385 @@ +/**************************************************************************** +Copyright (c) 2011-2012, Armin Biere, Johannes Kepler University. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to +deal in the Software without restriction, including without limitation the +rights to use, copy, modify, merge, publish, distribute, sublicense, and/or +sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS +IN THE SOFTWARE. +****************************************************************************/ + +#include "picosat.h" + +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <stdarg.h> +#include <ctype.h> + +#define MAXNONREDROUNDS 3 +#define MINCOREROUNDS 5 +#define MAXCOREROUNDS 100 + +typedef struct Cls { int lit, red, * lits; } Cls; + +static int verbose = 1, nowitness; +static int fclose_input, pclose_input, close_output; +static FILE * input_file, * output_file; +static const char * input_name, * output_name; +static int lineno = 1; +static int nvars, nclauses; +static Cls * clauses; +static int * lits, nlits, szlits; +static double start; +static int reductions; + +static PicoSAT * ps; + +static int next (void) { + int res = fgetc (input_file); + if (res == '\n') lineno++; + return res; +} + +static void msg (int level, const char * fmt, ...) { + va_list ap; + if (verbose < level) return; + fputs ("c [picomus] ", stdout); + va_start (ap, fmt); + vfprintf (stdout, fmt, ap); + va_end (ap); + fputc ('\n', stdout); + fflush (stdout); +} + +static void warn (const char * fmt, ...) { + va_list ap; + fputs ("c [picomus] WARNING: ", stdout); + va_start (ap, fmt); + vfprintf (stdout, fmt, ap); + va_end (ap); + fputc ('\n', stdout); + fflush (stdout); +} + +static const char * parse (void) { + int ch, n, lit, sign, i; + Cls * c; +HEADER: + ch = next (); + if (ch == 'c') { + while ((ch = next ()) != '\n') + if (ch == EOF) return "EOF after 'c'"; + goto HEADER; + } + if (ch == '\r') goto HEADER; + if (ch != 'p') return "expected 'c' or 'p'"; + if (fscanf (input_file, " cnf %d %d", &nvars, &nclauses) != 2) + return "invalid header"; + msg (1, "p cnf %d %d", nvars, nclauses); + clauses = calloc (nclauses, sizeof *clauses); + lit = n = 0; +LIT: + ch = next (); + if (ch == ' ' || ch == '\n' || ch == '\t' || ch == '\r') goto LIT; + if (ch == 'c') { + while ((ch = next ()) != '\n') + if (ch == EOF) return "EOF after 'c'"; + goto LIT; + } + if (ch == EOF) { + if (lit) return "zero missing"; + if (n < nclauses) return "clauses missing"; + return 0; + } + if (n == nclauses) return "too many clauses"; + if (ch == '-') { + sign = -1; + ch = next (); + if (!isdigit (ch)) return "expected digit after '-'"; + } else sign = 1; + if (!isdigit (ch)) return "expected digit"; + lit = ch - '0'; + while (isdigit (ch = next ())) + lit = 10 * lit + (ch - '0'); + if (lit > nvars) return "maximum variable index exceeded"; + if (lit) { + lit *= sign; + if (nlits == szlits) { + szlits = szlits ? 2 * szlits : 1; + lits = realloc (lits, szlits * sizeof *lits); + } + lits[nlits++] = lit; + } else { + c = clauses + n++; + c->lits = malloc ((nlits + 1) * sizeof *c->lits); + for (i = 0; i < nlits; i++) + c->lits[i] = lits[i]; + c->lits[i] = 0; + nlits = 0; + } + goto LIT; +} + +static void die (const char * fmt, ...) { + va_list ap; + fputs ("*** picomus: ", stdout); + va_start (ap, fmt); + vfprintf (stdout, fmt, ap); + va_end (ap); + fputc ('\n', stdout); + fflush (stdout); + exit (1); +} + +static double percent (double a, double b) { return b?100.0*a/b:0.0; } + +static void callback (void * dummy, const int * mus) { + int remaining; + const int * p; + (void) dummy; + if (!verbose) return; + remaining = 0; + for (p = mus; *p; p++) remaining++; + assert (remaining <= nclauses); + reductions++; + msg (1, "reduction %d to %d = %.0f%% out of %d after %.1f sec", + reductions, + remaining, percent (remaining, nclauses), nclauses, + picosat_time_stamp () - start); +} + +int main (int argc, char ** argv) { + int i, * p, n, oldn, red, nonred, res, round, printed, len; + const char * err; + const int * q; + char * cmd; + Cls * c; +#ifndef NDEBUG + int tmp; +#endif + start = picosat_time_stamp (); + for (i = 1; i < argc; i++) { + if (!strcmp (argv[i], "-h")) { + printf ( + "picomus [-v][-h][-a][<input>[<output>]]\n" + "\n" + "This tool is a SAT solver that uses the PicoSAT library to\n" + "generate a 'minimal unsatisfiable core' also known as 'minimal\n" + "unsatisfiable set' (MUS) of a CNF in DIMACS format.\n" + "\n" + "Both file arguments can be \"-\" and then denote <stdin> resp.\n" + "<stdout>. If no input file is given <stdin> is used. If no\n" + "output file is specified the MUS is computed and only printed\n" + "to <stdout> in the format of the SAT competition 2011 MUS track.\n" + "\n" + "If '-n' is specified solution respectively MUS printing\n" + "on <stdout> (using the 'v ...' format) is suppressed.\n" + "If <output> is specified an MUS is written to this file,\n" + "even if '-n' is used.\n" + "\n" +#ifndef TRACE + "WARNING: PicosSAT is compiled without trace support.\n" + "\n" + "This typically slows down this MUS extractor, since\n" + "it only relies on clause selector variables and\n" + "can not make use of core extraction. To enable\n" + "trace generation use './configure --trace' or\n" + "'./configure -O --trace' when building PicoSAT.\n" +#else + "Since trace generation code is included, this binary\n" + "uses also core extraction in addition to clause selector\n" + "variables.\n" +#endif + ); + exit (0); + } else if (!strcmp (argv[i], "-v")) verbose++; + else if (!strcmp (argv[i], "-n")) nowitness = 1; + else if (argv[i][0] == '-') + die ("invalid command line option '%s'", argv[i]); + else if (output_name) die ("too many arguments"); + else if (!input_name) input_name = argv[i]; + else output_name = argv[i]; + } + if (!output_name) warn ("no output file given"); + if (input_name && strcmp (input_name, "-")) { + len = strlen (input_name); + if (len >= 3 && !strcmp (input_name + len - 3, ".gz")) { + cmd = malloc (len + 20); + sprintf (cmd, "gunzip -c %s 2>/dev/null", input_name); + input_file = popen (cmd, "r"); + pclose_input = 1; + free (cmd); + } else input_file = fopen (input_name, "r"), fclose_input = 1; + if (!input_file) die ("can not read '%s'", input_name); + } else input_file = stdin, input_name = "-"; + if ((err = parse ())) { + fprintf (stdout, "%s:%d: %s\n", input_name, lineno, err); + fflush (stdout); + exit (1); + } + if (fclose_input) fclose (input_file); + if (pclose_input) pclose (input_file); + ps = picosat_init (); + picosat_set_prefix (ps, "c [picosat] "); + picosat_set_output (ps, stdout); + if (verbose > 1) picosat_set_verbosity (ps, verbose - 1); + printed = 0; + if (!picosat_enable_trace_generation (ps)) + warn ("PicoSAT compiled without trace generation"), + warn ("core extraction disabled"); + else { + n = nclauses; + nonred = 0; + for (round = 1; round <= MAXCOREROUNDS; round++) { + if (verbose > 1) + msg (1, "starting core extraction round %d", round); + picosat_set_seed (ps, round); + for (i = 0; i < nclauses; i++) { + c = clauses + i; + if (c->red) { + picosat_add (ps, 1); + picosat_add (ps, -1); + } else { + for (p = c->lits; *p; p++) + picosat_add (ps, *p); + } +#ifndef NDEBUG + tmp = +#endif + picosat_add (ps, 0); + assert (tmp == i); + } + res = picosat_sat (ps, -1); + if (res == 10) { assert (round == 1); goto SAT; } + assert (res == 20); + if (!printed) { + assert (round == 1); + printed = 1; + printf ("s UNSATISFIABLE\n"); + fflush (stdout); + } + for (i = 0; i < nclauses; i++) { + c = clauses + i; + if (c->red) { assert (!picosat_coreclause (ps, i)); continue; } + if (picosat_coreclause (ps, i)) continue; + c->red = 1; + } + oldn = n; + n = 0; + for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++; + msg (1, "extracted core %d of size %d = %0.f%% out of %d after %.1f sec", + round, n, percent (n, nclauses), nclauses, + picosat_time_stamp () - start); + assert (oldn >= n); + picosat_reset (ps); + ps = picosat_init (); + picosat_set_prefix (ps, "c [picosat] "); + picosat_set_output (ps, stdout); + if (round >= MINCOREROUNDS) { + red = oldn - n; + if (red < 10 && (100*red + 99)/oldn < 2) { + nonred++; + if (nonred > MAXNONREDROUNDS) break; + } + } + if (round < MAXCOREROUNDS) picosat_enable_trace_generation (ps); + } + } + for (i = 0; i < nclauses; i++) { + c = clauses + i; + if (c->red) { + picosat_add (ps, 1); + picosat_add (ps, -1); +#ifndef NDEBUG + tmp = +#endif + picosat_add (ps, 0); + assert (tmp == i); + continue; + } + c->lit = nvars + i + 1; + picosat_add (ps, -c->lit); + for (p = c->lits; *p; p++) + (void) picosat_add (ps, *p); +#ifndef NDEBUG + tmp = +#endif + picosat_add (ps, 0); + assert (tmp == i); + } + for (i = 0; i < nclauses; i++) { + c = clauses + i; + if (c->red) continue; + picosat_assume (ps, c->lit); + } + res = picosat_sat (ps, -1); + if (res == 20) { + if (!printed) printf ("s UNSATISFIABLE\n"), fflush (stdout); + for (i = 0; i < nclauses; i++) clauses[i].red = 1; + q = picosat_mus_assumptions (ps, 0, callback, 1); + while ((i = *q++)) { + i -= nvars + 1; + assert (0 <= i && i < nclauses); + clauses[i].red = 0; + } + } else { +SAT: + assert (res == 10); + printf ("s SATISFIABLE\n"); fflush (stdout); + if (!nowitness) { + for (i = 1; i <= nvars; i++) + printf ("v %d\n", ((picosat_deref (ps, i) < 0) ? -1 : 1) * i); + printf ("v 0\n"); + } + } + if (verbose) picosat_stats (ps); + picosat_reset (ps); + n = 0; + for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++; + red = nclauses - n; + msg (1, "found %d redundant clauses %.0f%%", red, percent (red, nclauses)); + msg (0, "computed MUS of size %d out of %d (%.0f%%)", + n, nclauses, percent (n, nclauses)); + if (output_name && strcmp (output_name, "-")) { + output_file = fopen (output_name, "w"); + if (!output_file) die ("can not write '%s'", output_name); + close_output = 1; + } else if (output_name && !strcmp (output_name, "-")) output_file = stdout; + if (output_file) { + fprintf (output_file, "p cnf %d %d\n", nvars, n); + for (i = 0; i < nclauses; i++) + if (!clauses[i].red) { + for (p = clauses[i].lits; *p; p++) fprintf (output_file, "%d ", *p); + fprintf (output_file, "0\n"); + } + if (close_output) fclose (output_file); + } + if (res == 20) { + if (!nowitness) { + for (i = 0; i < nclauses; i++) + if (!clauses[i].red) printf ("v %d\n", i+1); + printf ("v 0\n"); + } + } + msg (1, "%s %d irredundant clauses %.0f%%", + output_file ? "printed" : "computed", n, percent (n, nclauses)); + for (i = 0; i < nclauses; i++) free (clauses[i].lits); + free (clauses); + free (lits); + msg (1, "%d reductions in %.1f seconds", + reductions, picosat_time_stamp () - start); + return res; +} |