×

zbMATH — the first resource for mathematics

A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem. (English) Zbl 1179.90234
Summary: Given a CNF (conjunctive normal form) Boolean expression with clauses of size at most two, the Max-2-SAT problem asks to find a truth assignment to the Boolean variables that makes true the maximum number of clauses. In this paper, we describe an innovative upper bound computation procedure which is centered around the use of equations and inequalities that are satisfied by all solutions to the problem. The procedure is incorporated in a branch-and-bound algorithm for Max-2-SAT. An initial solution to the problem is provided by an iterated tabu search heuristic. We present computational experience on the Max-2-SAT benchmark instances from the Max-SAT Evaluation 2007. The results show that the developed branch-and-bound algorithm is very competitive with the best previously reported techniques.

MSC:
90C09 Boolean programming
90C57 Polyhedral combinatorics, branch-and-bound, branch-and-cut
Software:
MAX-2-SAT; MaxSolver
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alber, J.; Gramm, J.; Niedermeier, R., Faster exact algorithms for hard problems: a parameterized point of view, Discrete math., 229, 3-27, (2001) · Zbl 0973.68256
[2] Alsinet, T.; Manyà, F.; Planes, J., An efficient solver for weighted MAX-SAT, J. global optim., 41, 61-73, (2008) · Zbl 1146.90480
[3] N. Bansal, V. Raman, Upper bounds for MaxSat: further improved, in: The 10th International Symposium on Algorithms and Computation (ISAAC’99), Chennai, India, December 16-18, 1999, Lect. Notes Comput. Sci., vol. 1741, 1999, pp. 247-258. · Zbl 0971.68069
[4] R. Battiti, P. Campigotto, Reactive search for MAX-SAT: diversification-bias properties with prohibitions and penalties, Technical Report DIT-07-058, Informatica e Telecomunicazioni, University of Trento, Trento, Italy, 2007.
[5] Borchers, B.; Furman, J., A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, J. comb. optim., 2, 299-306, (1999) · Zbl 0954.90026
[6] J. Cheriyan, W.H. Cunningham, L. Tunçel, Y. Wang, A linear programming and rounding approach to Max-2-SAT, in: D.S. Johnson, M.A. Trick (Eds.), Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, Amer. Math. Soc., Providence, RI, USA, 1996, pp. 395-414. · Zbl 0864.90102
[7] S. de Givry, J. Larrosa, P. Meseguer, T. Schiex, Solving Max-SAT as weighted CSP, in: The Nineth International Conference on Principles and Practice of Constraint Programming, Kinsale, Ireland, September 29 to October 3, 2003, Lect. Notes Comput. Sci., vol. 2833, 2003, pp. 363-376. · Zbl 1273.68368
[8] de Klerk, E.; Warners, J.P., Semidefinite programming approaches for MAX-2-SAT and MAX-3-SAT: computational perspectives, (), 161-176 · Zbl 1029.90053
[9] Di Battista, G.; Erlebach, T.; Hall, A.; Patrignani, M.; Pizzonia, M.; Schank, T., Computing the types of the relationships between autonomous systems, IEEE/ACM trans. network., 15, 267-280, (2007)
[10] Dimitropoulos, X.; Krioukov, D.; Fomenkov, M.; Huffaker, B.; Hyun, Y.; Claffy, K.C.; Riley, G., AS relationships: inference and validation, ACM SIGCOMM comput. commun. rev., 37, 29-40, (2007)
[11] X. Dimitropoulos, D. Krioukov, B. Huffaker, K.C. Claffy, G. Riley, Inferring AS relationships: dead end or lively beginning? in: The Fourth International Workshop on Efficient and Experimental Algorithms (WEA’05), May 2005, Lect. Notes Comput. Sci., vol. 3503, 2005, pp. 113-125. · Zbl 1121.90348
[12] Glover, F., Tabu search – part I, ORSA J. comput., 1, 190-206, (1989) · Zbl 0753.90054
[13] Goemans, M.X.; Williamson, D.P., Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM, 42, 1115-1145, (1995) · Zbl 0885.68088
[14] C.P. Gomes, W.-J. van Hoeve, L. Leahu, The power of semidefinite programming relaxations for MAX-SAT, in: The Third International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2006), Cork, Ireland, May 31 to June 2, 2006, Lect. Notes Comput. Sci., vol. 3990, 2006, pp. 104-118. · Zbl 1177.68186
[15] F. Heras, J. Larrosa, New inference rules for efficient Max-SAT solving, in: Proceedings of the 21st National Conference on Artificial Intelligence, Boston, MA, July 16-20, 2006, AAAI Press, Menlo Park, CA, 2006, pp. 68-73.
[16] A. Ishtaiwi, J. Thornton, A. Sattar, Weight redistribution for unweighted MAX-SAT, in: The 20th Australian Joint Conference on Artificial Intelligence, Gold Coast, Australia, December 2-6, 2007, Lect. Notes Comput. Sci., vol. 4830, 2007, pp. 687-693.
[17] S. Joy, J.E. Mitchell, B. Borchers, Solving MAX-SAT and weighted MAX-SAT problems using branch-and-cut, Technical Report, Mathematical Sciences, Rensselaer Polytechnic Institute, Troy, NY 12180, 1998. · Zbl 0889.68074
[18] Kastner, R.; Bozorgzadeh, E.; Sarrafzadeh, M., Pattern routing: use and theory for increasing predictability and avoiding coupling, IEEE trans. comput.-aided des. integr. circuits syst., 21, 777-790, (2002)
[19] J. Larrosa, F. Heras, Resolution in Max-SAT and its relation to local consistency in weighted CSPs, in: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI-05), Edinburgh, Scotland, July 30 to August 5, 2005, pp. 193-198. · Zbl 1153.68463
[20] M. Lewin, D. Livnat, U. Zwick, Improved rounding techniques for the MAX 2-SAT and MAX DI-CUT problems, in: The Nineth International IPCO Conference on Integer Programming and Combinatorial Optimization, Cambridge, Massachusetts, May 27-29, 2002, Lect. Notes Comput. Sci., vol. 2337, 2002, pp. 67-82. · Zbl 1049.90535
[21] C.M. Li, F. Manyà, J. Planes, Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT, in: Proceedings of the 21st National Conference on Artificial Intelligence, Boston, MA, July 16-20, 2006, AAAI Press, Menlo Park, CA, 2006, pp. 86-91.
[22] Li, C.M.; Manyà, F.; Planes, J., New inference rules for MAX-SAT, J. artif. intell. res., 30, 321-359, (2007) · Zbl 1182.68254
[23] Miyashiro, R.; Matsui, T., Semidefinite programming based approaches to the break minimization problem, Comput. oper. res., 33, 1975-1982, (2006) · Zbl 1090.90154
[24] Palubeckis, G., Iterated tabu search for the unconstrained binary quadratic optimization problem, Informatica, 17, 279-296, (2006) · Zbl 1098.90048
[25] Palubeckis, G., Iterated tabu search for the maximum diversity problem, Appl. math. comput., 189, 371-383, (2007) · Zbl 1122.65362
[26] Palubeckis, G., On the recursive largest first algorithm for graph colouring, Int. J. comput. math., 85, 191-200, (2008) · Zbl 1139.05024
[27] Palubeckis, G., On the graph coloring polytope, Inf. technol. control, 37, 7-11, (2008)
[28] K. Pipatsrisawat, A. Darwiche, Clone: solving weighted Max-SAT in a reduced search space, in: The 20th Australian Joint Conference on Artificial Intelligence, Gold Coast, Australia, December 2-6, 2007, Lect. Notes Comput. Sci., vol. 4830, 2007, pp. 223-233.
[29] Shen, H.; Zhang, H., Improving exact algorithms for MAX-2-SAT, Ann. math. artif. intel., 44, 419-436, (2005) · Zbl 1086.68058
[30] R. Straub, H. Prautzsch, Creating optimized cut-out sheets for paper models from meshes, Paper presented at the Nineth SIAM Conference on Geometric Design and Computing, Phoenix, AZ, USA, October 30 to November 3, 2005, <http://i33www.ibds.uni-karlsruhe.de/papers/cut-out-sheets.pdf>.
[31] T. Stützle, H. Hoos, A. Roli, A review of the literature on local search algorithms for MAX-SAT, Technical Report AIDA-01-02, Darmstadt University of Technology, Computer Science Department, Intellectics Group, Darmstadt, Germany, 2001.
[32] R.J. Wallace, E.C. Freuder, Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems, in: D.S. Johnson, M.A. Trick (Eds.), Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, Amer. Math. Soc., Providence, RI, USA, 1996, pp. 587-615. · Zbl 0859.68072
[33] Xing, Z.; Zhang, W., Maxsolver: an efficient exact algorithm for weighted maximum satisfiability, Artif. intell., 164, 47-80, (2005) · Zbl 1132.68716
[34] Xu, H.; Rutenbar, R.A.; Sakallah, K., Sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing, IEEE trans. comput.-aided des. integr. circuits syst., 22, 814-820, (2003)
[35] Yannakakis, M., On the approximation of maximum satisfiability, J. algorithm, 17, 475-502, (1994) · Zbl 0820.68056
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.