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 }
die(const char * fmt,...)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 
msg(const char * fmt,...)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);
percent(double a,double b)61   stk[nstk++] = n;
62 }
callback(void * dummy,const int * mus)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 }
335