1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 /*
8 Simple MAXSAT solver on top of the Z3 API.
9 */
10 #include<stdio.h>
11 #include<stdlib.h>
12 #include<memory.h>
13 #include<z3.h>
14
15 /**
16 \defgroup maxsat_ex MaxSAT/MaxSMT examples
17 */
18 /**@{*/
19
20 /**
21 \brief Exit gracefully in case of error.
22 */
error(char * msg)23 void error(char * msg)
24 {
25 fprintf(stderr, "%s\n", msg);
26 exit(1);
27 }
28
29 /**
30 \brief Create a logical context.
31 Enable model construction only.
32 */
mk_context()33 Z3_context mk_context()
34 {
35 Z3_config cfg;
36 Z3_context ctx;
37 cfg = Z3_mk_config();
38 Z3_set_param_value(cfg, "MODEL", "true");
39 ctx = Z3_mk_context(cfg);
40 Z3_del_config(cfg);
41 return ctx;
42 }
43
44 /**
45 \brief Create a variable using the given name and type.
46 */
mk_var(Z3_context ctx,const char * name,Z3_sort ty)47 Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
48 {
49 Z3_symbol s = Z3_mk_string_symbol(ctx, name);
50 return Z3_mk_const(ctx, s, ty);
51 }
52
53 /**
54 \brief Create a boolean variable using the given name.
55 */
mk_bool_var(Z3_context ctx,const char * name)56 Z3_ast mk_bool_var(Z3_context ctx, const char * name)
57 {
58 Z3_sort ty = Z3_mk_bool_sort(ctx);
59 return mk_var(ctx, name, ty);
60 }
61
62 /**
63 \brief Create a fresh boolean variable.
64 */
mk_fresh_bool_var(Z3_context ctx)65 Z3_ast mk_fresh_bool_var(Z3_context ctx)
66 {
67 return Z3_mk_fresh_const(ctx, "k", Z3_mk_bool_sort(ctx));
68 }
69
70 /**
71 \brief Create an array with \c num_vars fresh boolean variables.
72 */
mk_fresh_bool_var_array(Z3_context ctx,unsigned num_vars)73 Z3_ast * mk_fresh_bool_var_array(Z3_context ctx, unsigned num_vars)
74 {
75 Z3_ast * result = (Z3_ast *) malloc(sizeof(Z3_ast) * num_vars);
76 unsigned i;
77 for (i = 0; i < num_vars; i++) {
78 result[i] = mk_fresh_bool_var(ctx);
79 }
80 return result;
81 }
82
83 /**
84 \brief Delete array of boolean variables.
85 */
del_bool_var_array(Z3_ast * arr)86 void del_bool_var_array(Z3_ast * arr)
87 {
88 free(arr);
89 }
90
91 /**
92 \brief Create a binary OR.
93 */
mk_binary_or(Z3_context ctx,Z3_ast in_1,Z3_ast in_2)94 Z3_ast mk_binary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2)
95 {
96 Z3_ast args[2] = { in_1, in_2 };
97 return Z3_mk_or(ctx, 2, args);
98 }
99
100 /**
101 \brief Create a ternary OR.
102 */
mk_ternary_or(Z3_context ctx,Z3_ast in_1,Z3_ast in_2,Z3_ast in_3)103 Z3_ast mk_ternary_or(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast in_3)
104 {
105 Z3_ast args[3] = { in_1, in_2, in_3 };
106 return Z3_mk_or(ctx, 3, args);
107 }
108
109 /**
110 \brief Create a binary AND.
111 */
mk_binary_and(Z3_context ctx,Z3_ast in_1,Z3_ast in_2)112 Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2)
113 {
114 Z3_ast args[2] = { in_1, in_2 };
115 return Z3_mk_and(ctx, 2, args);
116 }
117
118
119
120 /**
121 \brief Free the given array of cnstrs that was allocated using get_hard_constraints or get_soft_constraints.
122 */
free_cnstr_array(Z3_ast * cnstrs)123 void free_cnstr_array(Z3_ast * cnstrs)
124 {
125 free(cnstrs);
126 }
127
128 /**
129 \brief Assert hard constraints stored in the given array.
130 */
assert_hard_constraints(Z3_context ctx,Z3_solver s,unsigned num_cnstrs,Z3_ast * cnstrs)131 void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs)
132 {
133 unsigned i;
134 for (i = 0; i < num_cnstrs; i++) {
135 Z3_solver_assert(ctx, s, cnstrs[i]);
136 }
137 }
138
139 /**
140 \brief Assert soft constraints stored in the given array.
141 This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
142 It will also return an array containing these fresh variables.
143 */
assert_soft_constraints(Z3_context ctx,Z3_solver s,unsigned num_cnstrs,Z3_ast * cnstrs)144 Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs)
145 {
146 unsigned i;
147 Z3_ast * aux_vars;
148 aux_vars = mk_fresh_bool_var_array(ctx, num_cnstrs);
149 for (i = 0; i < num_cnstrs; i++) {
150 Z3_ast assumption = cnstrs[i];
151 Z3_solver_assert(ctx, s, mk_binary_or(ctx, assumption, aux_vars[i]));
152 }
153 return aux_vars;
154 }
155
156 /**
157 \brief Create a full adder with inputs \c in_1, \c in_2 and \c cin.
158 The output of the full adder is stored in \c out, and the carry in \c c_out.
159 */
mk_full_adder(Z3_context ctx,Z3_ast in_1,Z3_ast in_2,Z3_ast cin,Z3_ast * out,Z3_ast * cout)160 void mk_full_adder(Z3_context ctx, Z3_ast in_1, Z3_ast in_2, Z3_ast cin, Z3_ast * out, Z3_ast * cout)
161 {
162 *cout = mk_ternary_or(ctx, mk_binary_and(ctx, in_1, in_2), mk_binary_and(ctx, in_1, cin), mk_binary_and(ctx, in_2, cin));
163 *out = Z3_mk_xor(ctx, Z3_mk_xor(ctx, in_1, in_2), cin);
164 }
165
166 /**
167 \brief Create an adder for inputs of size \c num_bits.
168 The arguments \c in1 and \c in2 are arrays of bits of size \c num_bits.
169
170 \remark \c result must be an array of size \c num_bits + 1.
171 */
mk_adder(Z3_context ctx,unsigned num_bits,Z3_ast * in_1,Z3_ast * in_2,Z3_ast * result)172 void mk_adder(Z3_context ctx, unsigned num_bits, Z3_ast * in_1, Z3_ast * in_2, Z3_ast * result)
173 {
174 Z3_ast cin, cout, out;
175 unsigned i;
176 cin = Z3_mk_false(ctx);
177 for (i = 0; i < num_bits; i++) {
178 mk_full_adder(ctx, in_1[i], in_2[i], cin, &out, &cout);
179 result[i] = out;
180 cin = cout;
181 }
182 result[num_bits] = cout;
183 }
184
185 /**
186 \brief Given \c num_ins "numbers" of size \c num_bits stored in \c in.
187 Create floor(num_ins/2) adder circuits. Each circuit is adding two consecutive "numbers".
188 The numbers are stored one after the next in the array \c in.
189 That is, the array \c in has size num_bits * num_ins.
190 Return an array of bits containing \c ceil(num_ins/2) numbers of size \c (num_bits + 1).
191 If num_ins/2 is not an integer, then the last "number" in the output, is the last "number" in \c in with an appended "zero".
192 */
mk_adder_pairs(Z3_context ctx,unsigned num_bits,unsigned num_ins,Z3_ast * in,unsigned * out_num_ins,Z3_ast * out)193 void mk_adder_pairs(Z3_context ctx, unsigned num_bits, unsigned num_ins, Z3_ast * in, unsigned * out_num_ins, Z3_ast * out)
194 {
195 unsigned out_num_bits = num_bits + 1;
196 unsigned i = 0;
197 Z3_ast * _in = in;
198 Z3_ast * _out = out;
199 *out_num_ins = (num_ins % 2 == 0) ? (num_ins / 2) : (num_ins / 2) + 1;
200 for (i = 0; i < num_ins / 2; i++) {
201 mk_adder(ctx, num_bits, _in, _in + num_bits, _out);
202 _in += num_bits;
203 _in += num_bits;
204 _out += out_num_bits;
205 }
206 if (num_ins % 2 != 0) {
207 for (i = 0; i < num_bits; i++) {
208 _out[i] = _in[i];
209 }
210 _out[num_bits] = Z3_mk_false(ctx);
211 }
212 }
213
214 /**
215 \brief Create a counter circuit to count the number of "ones" in lits.
216 The function returns an array of bits (i.e. boolean expressions) containing the output of the circuit.
217 The size of the array is stored in out_sz.
218 */
mk_counter_circuit(Z3_context ctx,unsigned n,Z3_ast * lits,unsigned * out_sz)219 Z3_ast * mk_counter_circuit(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned * out_sz)
220 {
221 unsigned num_ins = n;
222 unsigned num_bits = 1;
223 Z3_ast * aux_1;
224 Z3_ast * aux_2;
225 if (n == 0)
226 return 0;
227 aux_1 = (Z3_ast *) malloc(sizeof(Z3_ast) * (n + 1));
228 aux_2 = (Z3_ast *) malloc(sizeof(Z3_ast) * (n + 1));
229 memcpy(aux_1, lits, sizeof(Z3_ast) * n);
230 while (num_ins > 1) {
231 unsigned new_num_ins;
232 Z3_ast * tmp;
233 mk_adder_pairs(ctx, num_bits, num_ins, aux_1, &new_num_ins, aux_2);
234 num_ins = new_num_ins;
235 num_bits++;
236 #ifdef MAXSAT_DEBUG
237 {
238 unsigned i;
239 printf("num_bits: %d, num_ins: %d \n", num_bits, num_ins);
240 for (i = 0; i < num_ins * num_bits; i++) {
241 printf("bit %d:\n%s\n", i, Z3_ast_to_string(ctx, aux_2[i]));
242 }
243 printf("-----------\n");
244 }
245 #endif
246 tmp = aux_1;
247 aux_1 = aux_2;
248 aux_2 = tmp;
249 }
250 *out_sz = num_bits;
251 free(aux_2);
252 return aux_1;
253 }
254
255 /**
256 \brief Return the \c idx bit of \c val.
257 */
get_bit(unsigned val,unsigned idx)258 int get_bit(unsigned val, unsigned idx)
259 {
260 unsigned mask = 1 << (idx & 31);
261 return (val & mask) != 0;
262 }
263
264 /**
265 \brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k.
266 */
assert_le_k(Z3_context ctx,Z3_solver s,unsigned n,Z3_ast * val,unsigned k)267 void assert_le_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * val, unsigned k)
268 {
269 Z3_ast i1, i2, not_val, out;
270 unsigned idx;
271 not_val = Z3_mk_not(ctx, val[0]);
272 if (get_bit(k, 0))
273 out = Z3_mk_true(ctx);
274 else
275 out = not_val;
276 for (idx = 1; idx < n; idx++) {
277 not_val = Z3_mk_not(ctx, val[idx]);
278 if (get_bit(k, idx)) {
279 i1 = not_val;
280 i2 = out;
281 }
282 else {
283 i1 = Z3_mk_false(ctx);
284 i2 = Z3_mk_false(ctx);
285 }
286 out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out));
287 }
288 // printf("at-most-k:\n%s\n", Z3_ast_to_string(ctx, out));
289 Z3_solver_assert(ctx, s, out);
290 }
291
292 /**
293 \brief Assert that at most \c k literals in \c lits can be true,
294 where \c n is the number of literals in lits.
295
296 We use a simple encoding using an adder (counter).
297 An interesting exercise consists in implementing more sophisticated encodings.
298 */
assert_at_most_k(Z3_context ctx,Z3_solver s,unsigned n,Z3_ast * lits,unsigned k)299 void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, unsigned k)
300 {
301 Z3_ast * counter_bits;
302 unsigned counter_bits_sz;
303 if (k >= n || n <= 1)
304 return; /* nothing to be done */
305 counter_bits = mk_counter_circuit(ctx, n, lits, &counter_bits_sz);
306 assert_le_k(ctx, s, counter_bits_sz, counter_bits, k);
307 del_bool_var_array(counter_bits);
308 }
309
310 /**
311 \brief Assert that at most one literal in \c lits can be true,
312 where \c n is the number of literals in lits.
313 */
assert_at_most_one(Z3_context ctx,Z3_solver s,unsigned n,Z3_ast * lits)314 void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits)
315 {
316 assert_at_most_k(ctx, s, n, lits, 1);
317 }
318
319
mk_solver(Z3_context ctx)320 Z3_solver mk_solver(Z3_context ctx)
321 {
322 Z3_solver r = Z3_mk_solver(ctx);
323 Z3_solver_inc_ref(ctx, r);
324 return r;
325 }
326
327 /**
328 \brief Small test for the at-most-one constraint.
329 */
tst_at_most_one()330 void tst_at_most_one()
331 {
332 Z3_context ctx = mk_context();
333 Z3_solver s = mk_solver(ctx);
334 Z3_ast k1 = mk_bool_var(ctx, "k1");
335 Z3_ast k2 = mk_bool_var(ctx, "k2");
336 Z3_ast k3 = mk_bool_var(ctx, "k3");
337 Z3_ast k4 = mk_bool_var(ctx, "k4");
338 Z3_ast k5 = mk_bool_var(ctx, "k5");
339 Z3_ast k6 = mk_bool_var(ctx, "k6");
340 Z3_ast args1[5] = { k1, k2, k3, k4, k5 };
341 Z3_ast args2[3] = { k4, k5, k6 };
342 Z3_model m = 0;
343 Z3_lbool result;
344 printf("testing at-most-one constraint\n");
345 assert_at_most_one(ctx, s, 5, args1);
346 assert_at_most_one(ctx, s, 3, args2);
347 printf("it must be sat...\n");
348 result = Z3_solver_check(ctx, s);
349 if (result != Z3_L_TRUE)
350 error("BUG");
351 m = Z3_solver_get_model(ctx, s);
352 Z3_model_inc_ref(ctx, m);
353 printf("model:\n%s\n", Z3_model_to_string(ctx, m));
354 Z3_model_dec_ref(ctx, m);
355 Z3_solver_assert(ctx, s, mk_binary_or(ctx, k2, k3));
356 Z3_solver_assert(ctx, s, mk_binary_or(ctx, k1, k6));
357 printf("it must be sat...\n");
358 result = Z3_solver_check(ctx, s);
359 if (result != Z3_L_TRUE)
360 error("BUG");
361 m = Z3_solver_get_model(ctx, s);
362 Z3_model_inc_ref(ctx, m);
363 printf("model:\n%s\n", Z3_model_to_string(ctx, m));
364 Z3_solver_assert(ctx, s, mk_binary_or(ctx, k4, k5));
365 printf("it must be unsat...\n");
366 result = Z3_solver_check(ctx, s);
367 if (result != Z3_L_FALSE)
368 error("BUG");
369 Z3_model_dec_ref(ctx, m);
370 Z3_solver_dec_ref(ctx, s);
371 Z3_del_context(ctx);
372 }
373
374 /**
375 \brief Return the number of soft-constraints that were disable by the given model.
376 A soft-constraint was disabled if the associated auxiliary variable was assigned to true.
377 */
get_num_disabled_soft_constraints(Z3_context ctx,Z3_model m,unsigned num_soft_cnstrs,Z3_ast * aux_vars)378 unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned num_soft_cnstrs, Z3_ast * aux_vars)
379 {
380 unsigned i;
381 unsigned num_disabled = 0;
382 Z3_ast t = Z3_mk_true(ctx);
383 for (i = 0; i < num_soft_cnstrs; i++) {
384 Z3_ast val;
385 if (Z3_model_eval(ctx, m, aux_vars[i], 1, &val) == true) {
386 // printf("%s", Z3_ast_to_string(ctx, aux_vars[i]));
387 // printf(" -> %s\n", Z3_ast_to_string(ctx, val));
388 if (Z3_is_eq_ast(ctx, val, t)) {
389 num_disabled++;
390 }
391 }
392 }
393 return num_disabled;
394 }
395
396 /**
397 \brief Naive maxsat procedure based on linear search and at-most-k
398 constraint. Return the number of soft-constraints that can be
399 satisfied. Return -1 if the hard-constraints cannot be
400 satisfied. That is, the formula cannot be satisfied even if all
401 soft-constraints are ignored.
402
403 Exercise: use binary search to implement MaxSAT.
404 Hint: you will need to use an answer literal to retract the at-most-k constraint.
405 */
naive_maxsat(Z3_context ctx,Z3_solver s,unsigned num_hard_cnstrs,Z3_ast * hard_cnstrs,unsigned num_soft_cnstrs,Z3_ast * soft_cnstrs)406 int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
407 {
408 Z3_ast * aux_vars;
409 Z3_lbool is_sat;
410 unsigned k;
411 assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs);
412 printf("checking whether hard constraints are satisfiable...\n");
413 is_sat = Z3_solver_check(ctx, s);
414 if (is_sat == Z3_L_FALSE) {
415 // It is not possible to make the formula satisfiable even when ignoring all soft constraints.
416 return -1;
417 }
418 if (num_soft_cnstrs == 0)
419 return 0; // nothing to be done...
420 aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs);
421 // Perform linear search.
422 k = num_soft_cnstrs - 1;
423 for (;;) {
424 Z3_model m;
425 unsigned num_disabled;
426 // at most k soft-constraints can be ignored.
427 printf("checking whether at-most %d soft-constraints can be ignored.\n", k);
428 assert_at_most_k(ctx, s, num_soft_cnstrs, aux_vars, k);
429 is_sat = Z3_solver_check(ctx, s);
430 if (is_sat == Z3_L_FALSE) {
431 printf("unsat\n");
432 return num_soft_cnstrs - k - 1;
433 }
434 m = Z3_solver_get_model(ctx, s);
435 Z3_model_inc_ref(ctx, m);
436 num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
437 Z3_model_dec_ref(ctx, m);
438 if (num_disabled > k) {
439 error("BUG");
440 }
441 printf("sat\n");
442 k = num_disabled;
443 if (k == 0) {
444 // it was possible to satisfy all soft-constraints.
445 return num_soft_cnstrs;
446 }
447 k--;
448 }
449 }
450
451 /**
452 \brief Implement one step of the Fu&Malik algorithm.
453 See fu_malik_maxsat function for more details.
454
455 Input: soft constraints + aux-vars (aka answer literals)
456 Output: done/not-done when not done return updated set of soft-constraints and aux-vars.
457 - if SAT --> terminates
458 - if UNSAT
459 * compute unsat core
460 * add blocking variable to soft-constraints in the core
461 - replace soft-constraint with the one with the blocking variable
462 - we should also add an aux-var
463 - replace aux-var with a new one
464 * add at-most-one constraint with blocking
465 */
fu_malik_maxsat_step(Z3_context ctx,Z3_solver s,unsigned num_soft_cnstrs,Z3_ast * soft_cnstrs,Z3_ast * aux_vars)466 int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars)
467 {
468 // create assumptions
469 Z3_ast * assumptions = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs);
470 Z3_lbool is_sat;
471 Z3_ast_vector core;
472 unsigned core_size;
473 unsigned i = 0;
474 unsigned k = 0;
475 Z3_ast * block_vars;
476 for (i = 0; i < num_soft_cnstrs; i++) {
477 // Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i])
478 // So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered.
479 assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
480 }
481
482 is_sat = Z3_solver_check_assumptions(ctx, s, num_soft_cnstrs, assumptions);
483 if (is_sat != Z3_L_FALSE) {
484 return 1; // done
485 }
486 else {
487 core = Z3_solver_get_unsat_core(ctx, s);
488 Z3_ast_vector_inc_ref(ctx, core);
489 core_size = Z3_ast_vector_size(ctx, core);
490 block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size);
491 k = 0;
492 // update soft-constraints and aux_vars
493 for (i = 0; i < num_soft_cnstrs; i++) {
494 unsigned j;
495 // check whether assumption[i] is in the core or not
496 for (j = 0; j < core_size; j++) {
497 if (assumptions[i] == Z3_ast_vector_get(ctx, core, j))
498 break;
499 }
500 if (j < core_size) {
501 // assumption[i] is in the unsat core... so soft_cnstrs[i] is in the unsat core
502 Z3_ast block_var = mk_fresh_bool_var(ctx);
503 Z3_ast new_aux_var = mk_fresh_bool_var(ctx);
504 soft_cnstrs[i] = mk_binary_or(ctx, soft_cnstrs[i], block_var);
505 aux_vars[i] = new_aux_var;
506 block_vars[k] = block_var;
507 k++;
508 // Add new constraint containing the block variable.
509 // Note that we are using the new auxiliary variable to be able to use it as an assumption.
510 Z3_solver_assert(ctx, s, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var));
511 }
512 }
513 assert_at_most_one(ctx, s, k, block_vars);
514 Z3_ast_vector_dec_ref(ctx, core);
515 return 0; // not done.
516 }
517 }
518
519 /**
520 \brief Fu & Malik procedure for MaxSAT. This procedure is based on
521 unsat core extraction and the at-most-one constraint.
522
523 Return the number of soft-constraints that can be
524 satisfied. Return -1 if the hard-constraints cannot be
525 satisfied. That is, the formula cannot be satisfied even if all
526 soft-constraints are ignored.
527
528 For more information on the Fu & Malik procedure:
529
530 Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International
531 Conference on Theory and Applications of Satisfiability Testing, 2006.
532 */
fu_malik_maxsat(Z3_context ctx,Z3_solver s,unsigned num_hard_cnstrs,Z3_ast * hard_cnstrs,unsigned num_soft_cnstrs,Z3_ast * soft_cnstrs)533 int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
534 {
535 Z3_ast * aux_vars;
536 Z3_lbool is_sat;
537 unsigned k;
538 assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs);
539 printf("checking whether hard constraints are satisfiable...\n");
540 is_sat = Z3_solver_check(ctx, s);
541 if (is_sat == Z3_L_FALSE) {
542 // It is not possible to make the formula satisfiable even when ignoring all soft constraints.
543 return -1;
544 }
545 if (num_soft_cnstrs == 0)
546 return 0; // nothing to be done...
547 /*
548 Fu&Malik algorithm is based on UNSAT-core extraction.
549 We accomplish that using auxiliary variables (aka answer literals).
550 */
551 aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs);
552 k = 0;
553 for (;;) {
554 printf("iteration %d\n", k);
555 if (fu_malik_maxsat_step(ctx, s, num_soft_cnstrs, soft_cnstrs, aux_vars)) {
556 return num_soft_cnstrs - k;
557 }
558 k++;
559 }
560 }
561
562 #define NAIVE_MAXSAT 0
563 #define FU_MALIK_MAXSAT 1
564
565 /**
566 \brief Finds the maximal number of assumptions that can be satisfied.
567 An assumption is any formula preceded with the :assumption keyword.
568 "Hard" constraints can be supported by using the :formula keyword.
569
570 Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.
571 Output: the maximum number of assumptions that can be satisfied.
572 */
smtlib_maxsat(char * file_name,int approach)573 int smtlib_maxsat(char * file_name, int approach)
574 {
575 Z3_context ctx;
576 Z3_solver s;
577 unsigned i;
578 Z3_optimize opt;
579 unsigned num_hard_cnstrs, num_soft_cnstrs;
580 Z3_ast * hard_cnstrs, * soft_cnstrs;
581 Z3_ast_vector hard, objs;
582 Z3_app soft;
583 unsigned result = 0;
584 ctx = mk_context();
585 s = mk_solver(ctx);
586 opt = Z3_mk_optimize(ctx);
587 Z3_optimize_inc_ref(ctx, opt);
588 Z3_optimize_from_file(ctx, opt, file_name);
589 hard = Z3_optimize_get_assertions(ctx, opt);
590 Z3_ast_vector_inc_ref(ctx, hard);
591 num_hard_cnstrs = Z3_ast_vector_size(ctx, hard);
592 hard_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_hard_cnstrs));
593 for (i = 0; i < num_hard_cnstrs; i++) {
594 hard_cnstrs[i] = Z3_ast_vector_get(ctx, hard, i);
595 }
596 objs = Z3_optimize_get_objectives(ctx, opt);
597 Z3_ast_vector_inc_ref(ctx, objs);
598
599 // soft constraints are stored in a single objective which is a sum
600 // of if-then-else expressions.
601 soft = Z3_to_app(ctx, Z3_ast_vector_get(ctx, objs, 0));
602 num_soft_cnstrs = Z3_get_app_num_args(ctx, soft);
603 soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs));
604 for (i = 0; i < num_soft_cnstrs; ++i) {
605 soft_cnstrs[i] = Z3_get_app_arg(ctx, Z3_to_app(ctx, Z3_get_app_arg(ctx, soft, i)), 0);
606 }
607
608 switch (approach) {
609 case NAIVE_MAXSAT:
610 result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
611 break;
612 case FU_MALIK_MAXSAT:
613 result = fu_malik_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
614 break;
615 default:
616 /* Exercise: implement your own MaxSAT algorithm.*/
617 error("Not implemented yet.");
618 break;
619 }
620 free_cnstr_array(hard_cnstrs);
621 free_cnstr_array(soft_cnstrs);
622 Z3_solver_dec_ref(ctx, s);
623 Z3_optimize_dec_ref(ctx, opt);
624 return result;
625 }
626
main(int argc,char * argv[])627 int main(int argc, char * argv[]) {
628 #if 1
629 int r;
630 if (argc != 2) {
631 error("usage: maxsat [filename.smt].");
632 }
633 r = smtlib_maxsat(argv[1], FU_MALIK_MAXSAT);
634 printf("result: %d\n", r);
635 #else
636 tst_at_most_one();
637 #endif
638 return 0;
639 }
640
641 /**@}*/
642
643