11 typedef struct Clause
{ int cid
, * lits
; struct Clause
* next
; } Clause
;
12 typedef struct MCS
{ int mid
, * clauses
; struct MCS
* next
; } MCS
;
17 static Clause
* first_clause
, * last_clause
;
18 static int nclauses
, first_cid
, last_cid
;
20 static MCS
* first_mcs
, * last_mcs
;
23 static int * stk
, szstk
, nstk
;
25 static int verbose
, join
, noprint
;
27 static int lineno
= 1, close_input
;
28 static const char * input_name
;
33 static void release_clauses (void) {
35 for (p
= first_clause
; p
; p
= next
) {
42 static void release_mss (void) {
44 for (p
= first_mcs
; p
; p
= next
) {
51 static void release (void) {
58 static void push_stack (int n
) {
60 stk
= realloc (stk
, (szstk
= szstk
? 2*szstk
: 1) * sizeof *stk
);
64 static void push_clause (void) {
67 clause
= malloc (sizeof *clause
);
68 clause
->cid
= ++nclauses
;
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
;
80 static void push_mcs (void) {
83 mcs
= malloc (sizeof *mcs
);
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
;
96 static int nextch (void) {
97 int res
= getc (input
);
98 if (res
== '\n') lineno
++;
102 static void msg (int level
, const char * fmt
, ...) {
104 if (level
> verbose
) return;
105 printf ("c [picomcs] ");
109 fputc ('\n', stdout
);
113 static const char * parse (void) {
114 int ch
, expclauses
, lit
, sign
;
116 msg (1, "parsing %s", input_name
);
120 while ((ch
= nextch ()) != '\n')
121 if (ch
== EOF
) return "out of file in comment";
126 return "invalid header";
128 if (fscanf (input
, "p cnf %d %d", &nvars
, &expclauses
) != 2)
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
);
136 if (ch
== ' ' || ch
== '\n' || ch
== '\t' || ch
== '\r') goto LIT
;
138 assert (nclauses
<= expclauses
);
139 if (nclauses
< expclauses
) return "clauses missing";
144 if (!isdigit (ch
)) return "expected digit after '-'";
145 if (ch
== '0') return "expected positive digit after '-'";
147 } else if (!isdigit (ch
)) return "expected '-' or digit";
150 while (isdigit (ch
= nextch ()))
151 lit
= 10*lit
+ (ch
- '0');
153 if (lit
> nvars
) return "maximum variable index exceeded";
154 if (nclauses
== expclauses
) return "too many clauses";
155 push_stack (sign
* lit
);
157 assert (nclauses
< expclauses
);
164 static void dump_clause (Clause
* c
) {
166 for (p
= c
->lits
; (lit
= *p
); p
++)
173 printf ("p cnf %d %d\n", nvars
, nclauses
);
174 for (p
= first_clause
; p
; p
= p
->next
)
179 static int clause2selvar (Clause
* c
) {
180 int res
= c
->cid
+ nvars
;
181 assert (first_cid
<= res
&& res
<= last_cid
);
185 static void encode_clause (Clause
* c
) {
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
);
193 picosat_add (ps
, -clause2selvar (c
));
194 for (p
= c
->lits
; (lit
= *p
); p
++) picosat_add (ps
, lit
);
198 static void encode (void) {
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
)
205 msg (1, "encoded %d clauses", nclauses
);
208 static void camcs (void) {
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
++)
216 printf ("c [picomcs] mcs %d :", nmcs
);
217 for (i
= 0; i
< nstk
; i
++) printf (" %d", stk
[i
] - nvars
);
218 fputc ('\n', stdout
);
220 } else if (verbose
&& isatty (1)) {
221 printf ("\rc [picomcs] mcs %d", nmcs
);
226 if (verbose
&& isatty (1)) fputc ('\r', stdout
);
227 msg (1, "found %d minimal correcting sets", nmcs
);
230 static void cumcscb (void * state
, int nmcs
, int nhumus
) {
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
);
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
);
248 for (p
= humus
; (cid
= *p
); p
++) {
249 if (marked
[cid
]) continue;
253 assert (count
== stats
[1]);
255 "computed union of minimal correcting sets of size %d with %d mcs",
263 for (cid
= first_cid
; cid
<= last_cid
; cid
++)
265 printf (" %d", cid
- nvars
);
270 print_mcs (MCS
* mcs
)
275 for (p
= mcs
->clauses
; (cid
= *p
); p
++)
276 printf (" %d", cid
- nvars
);
284 for (p
= first_mcs
; p
; p
= p
->next
)
288 int main (int argc
, char ** argv
) {
291 for (i
= 1; i
< argc
; i
++) {
292 if (!strcmp (argv
[i
], "-h")) {
293 printf ("usage: picomcs [-h][-v][-j][-n][<input>]\n");
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
]);
302 } else if (input_name
) {
303 fprintf (stderr
, "*** picomcs: two input files specified\n");
305 } else if (!(input
= fopen ((input_name
= argv
[i
]), "r"))) {
306 fprintf (stderr
, "*** picomcs: can not read '%s'\n", argv
[i
]);
308 } else close_input
= 1;
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
);
315 if (close_input
) fclose (input
);
316 ps
= picosat_init ();
317 picosat_set_prefix (ps
, "c [picosat] ");
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");
326 if (join
) cumcs (); else camcs ();
327 if (verbose
) picosat_stats (ps
);
330 if (join
) print_umcs (); else print_all_mcs ();