Abstract
For the last ten years, a significant amount of work in the constraint community has been devoted to the improvement of complete methods for solving soft constraints networks. We wanted to see how recent progress in the weighted CSP (WCSP) field could compete with other approaches in related fields. One of these fields is propositional logic and the well-known Max-SAT problem. In this paper, we show how Max-SAT can be encoded as a weighted constraint network, either directly or using a dual encoding. We then solve Max-SAT instances using state-of-the-art algorithms for weighted Max-CSP, dedicated Max-SAT solvers and the state-of-the-art MIP solver CPLEX. The results show that, despite a limited adaptation to CNF structure, WCSP-solver based methods are competitive with existing methods and can even outperform them, especially on the hardest, most over-constrained problems.
This research is partially supported by the French-Spanish collaboration PICASSO 05158SM – Integrated Action HF02-69. The second and third authors are also supported by the REPLI project TIC-2002-04470-C03.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Pbs: A backtracksearch pseudo-boolean solver and optimizer. In: Symposium on the Theory and Applications of Satisfiability Testing (SAT), Cincinnati (OH), pp. 346–353 (2002)
Barth, P.: A davis-putnam based enumeration algorithm for linear pseudo-boolean optimization. Tech. Rep. MPI-I-95-2-003, Max-Planck Institut Für Informatik (1995)
Borchers, B., Mitchell, J., Joy, S.: A branch-and-cut algorithm for MAXSAT and weighted MAX-SAT. In: Du, D., Gu, J., Pardalos, P. (eds.) Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 519–536. AMS, Providence (1997)
Borning, A., Mahert, M., Martindale, A., Wilson, M.: Constraint hierarchies and logic programming. In: Int. conf. on logic programming, pp. 149–164 (1989)
Dixon, H., Ginsberg, M.: Inference methods for a pseudo-boolean satisfiability solver. In: Proceedings of the Eighteenth National Conference on Artificial Intelligence (AAAI 2002), pp. 635–640 (2002)
Freuder, E., Wallace, R.: Partial constraint satisfaction. Artificial Intelligence 58, 21–70 (1992)
Freuder, E.C.: Partial constraint satisfaction. In: Proc. of the 11th IJCAI, Detroit, MI, pp. 278–283 (1989)
Gramm, J., Hirsch, E.A., Niedermeier, R., Rossmanith, P.: New worstcase upper bounds for MAX-2-SAT with application to MAX-CUT. Tech. Rep. TR00-037, Electronic Colloquium on Computational Complexity (2000)
Gramm, J., Niedermeier, R.: Faster exact solutions for max2Sat. In: Bongiovanni, G., Petreschi, R., Gambosi, G. (eds.) CIAC 2000. LNCS, vol. 1767, pp. 174–186. Springer, Heidelberg (2000)
Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Computing 44, 279–303 (1990)
ILOG. Cplex solver 8.1.0 (2002), http://www.ilog.com/products/cplex
Johnson, D.S., Trick, M.A. (eds.): Second DIMACS implementation challenge:cliques, coloring and satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26. AMS, Providence (1996)
Larrosa, J.: On arc and node consistency in weighted CSP. In: Proc. AAAI 2002, Edmondton, CA (2002)
Larrosa, J., Dechter, R.: CP 2000. LNCS, vol. 1894, p. 531. Springer, Heidelberg (2000)
Larrosa, J., Schiex, T.: In: the quest of the best form of local consistency for weighted CSP. In: Proc. of the 18th IJCAI, Acapulco, Mexico (August 2003), see http://www.inra.fr/bia/T/schiex/Export/ijcai03.pdf
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: 38th Design Automation Conference (DAC 2001), June 2001, pp. 530–535 (2001)
Resende, M., Pitsoulis, L., Pardalos, P.: Approximate solution of weighted max-SAT problems using GRASP. In: Du, D., Gu, J., Pardalos, P. (eds.) Satisfiability problem: Theory and Applications, pp. 393–405. AMS, Providence (1997)
Rosenfeld, A., Hummel, R., Zucker, S.: Scene labeling by relaxation operations. IEEE Trans. on Systems, Man, and Cybernetics 6(6), 173–184 (1976)
Schiex, T. Arc cohérence pour contraintes molles. In: Actes de JNPC 2000, Marseille (June 2000)
Schiex, T.: Arc consistency for soft constraints. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 411–424. Springer, Heidelberg (2000)
Schiex, T., Fargier, H., Verfaillie, G.: Valued constraint satisfaction problems: hard and easy problems. In: Proc. of the 14th IJCAI, Montréal, Canada, August 1995, pp. 631–637 (1995)
Selman, B., Kautz, H., Cohen, B.: Noise strategies for improving local search. In: Proc. of AAAI 1994, Seattle, WA, pp. 337–343 (1994)
van Gelder, A.: Cnfgen formula generator (1993), ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/contributed/UCSC/instances
van Hentenryck, P., Deville, Y.: The cardinality operator: A new logical connective for constraint logic programming. In: Proc. of the 8th international conference on logic programming, Paris, France (June 1991)
Whittemore, J., Kim, J., Sakallah, K.: SATIRE: A new incremental satisfiability engine. In: Proceedings of the 38th conference on Design automation, Las Vegas, NV, pp. 542–545. ACM, New York (2001)
Xu, H., Rutenbar, R.A., Sakallah, K.: sub-SAT: A formulation for relaxed boolean satisfiability with applications in routing. In: Proc. Int. Symp. on Physical Design, San Diego, CA (April 2002)
Zhang, W.: Phase transitions and backbones of 3-SAT and maximum 3-SAT. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 153–167. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Givry, S., Larrosa, J., Meseguer, P., Schiex, T. (2003). Solving Max-SAT as Weighted CSP. In: Rossi, F. (eds) Principles and Practice of Constraint Programming – CP 2003. CP 2003. Lecture Notes in Computer Science, vol 2833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45193-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-45193-8_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20202-8
Online ISBN: 978-3-540-45193-8
eBook Packages: Springer Book Archive