zbMATH — the first resource for mathematics

Resolution for Max-SAT. (English) Zbl 1168.68541
Summary: Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule. Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI
[1] Alekhnovich, M., Mutilated chessboard problem is exponentially hard for resolution, Theoretical computer science, 310, 1-3, 513-525, (2004) · Zbl 1071.68028
[2] T. Alsinet, F. Manyà, J. Planes, Improved branch and bound algorithms for Max-SAT, in: Proc. of the 6th Int. Conf. on the Theory and Applications of Satisfiability Testing, SAT’03, 2003 · Zbl 1124.68429
[3] Alsinet, T.; Manyà, F.; Planes, J., A MAX-SAT solver with lazy data structures, (), 334-342
[4] Alsinet, T.; Manyà, F.; Planes, J., Improved exact solver for weighted MAX-SAT, (), 371-377 · Zbl 1124.68429
[5] Ansótegui, C.; Bonet, M.L.; Levy, J.; Manyà, F., The logic behind weighted CSP, (), 32-37
[6] Atserias, A.; Bonet, M.L., On the automatizability of resolution and related propositional proof systems, (), 569-583 · Zbl 1020.03008
[7] Atserias, A.; Bonet, M.L., On the automatizability of resolution and related propositional proof systems, Information and computation, 189, 2, (2004) · Zbl 1051.03014
[8] Bansal, N.; Raman, V., Upper bounds for maxsat: further improved, (), 247-260 · Zbl 0971.68069
[9] Beame, P.; Karp, R.; Pitassi, T.; Saks, M., The efficiency of resolution and Davis-Putnam procedures, SIAM journal on computing, 31, 4, 1048-1075, (2002) · Zbl 1004.03048
[10] P. Beame, T. Pitassi, Simplified and improved resolution lower bounds, in: Proc. of the 37th Annual Symposium on Foundations of Computer Science, FOCS’96, Burlington, VT, USA, 1996, pp. 274-282
[11] Ben-Sasson, E.; Wigderson, A., Short proofs are narrow—resolution made simple, Journal of the ACM, 48, 2, 149-169, (2001) · Zbl 1089.03507
[12] Bonet, M.L.; Levy, J.; Manyà, F., A complete calculus for MAX-SAT, (), 240-251 · Zbl 1124.68104
[13] Borchers, B.; Furman, J., A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, Journal of combinatorial optimization, 2, 299-306, (1999) · Zbl 0954.90026
[14] S. Dantchev, S. Riis, Planar tautologies, hard for resolution, in: Proc. of the 42nd Annual Symposium on Foundations of Computer Science, FOCS’01, Los Alamitos, CA, USA, 2001, pp. 220-231
[15] Davis, M.; Putnam, H., A computing procedure for quantification theory, Journal of the ACM, 7, 3, 201-215, (1960) · Zbl 0212.34203
[16] Haken, A., The intractability of resolution, Theoretical computer science, 39, 2-3, 297-308, (1985) · Zbl 0586.03010
[17] Heras, F.; Larrosa, J., New inference rules for efficient MAX-SAT solving, (), 68-73
[18] Khanna, S.; Sudan, M.; Trevisan, L.; Williamson, D.P., The approximability of constraint satisfaction problems, SIAM journal on computing, 30, 6, 1863-1920, (2001) · Zbl 0992.68059
[19] Krajícek, J., Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic, Journal of symbolic logic, 62, 2, (1997) · Zbl 0891.03029
[20] Kulikov, A.S., Automated generation of simplification rules for SAT and MAXSAT, (), 430-436 · Zbl 1128.68469
[21] J. Larrosa, F. Heras, Resolution in Max-SAT and its relation to local consistency in weighted CSPs, in: Proc. of the 19th Int. Joint Conference on Artificial Intelligence, IJCAI’05, Edinburgh, Scotland, 2005, pp. 193-198 · Zbl 1153.68463
[22] Li, C.M.; Manyà, F.; Planes, J., Exploiting unit propagation to compute lower bounds in branch and bound MAX-SAT solvers, (), 403-414 · Zbl 1153.68470
[23] Li, C.M.; Manyà, F.; Planes, J., Detecting disjoint inconsistent subformulas for computing lower bounds for MAX-SAT, (), 86-91
[24] Niedermeier, R.; Rossmanith, P., New upper bounds for maximum satisfiability, Journal of algorithms, 36, 1, 63-88, (2000) · Zbl 0959.68049
[25] Papadimitriou, C.M., Computational complexity, (1994), Addison-Wesley Reading, MA · Zbl 0833.68049
[26] Pudlák, P., Lower bounds for resolution and cutting plane proofs and monotone computations, Journal of symbolic logic, 62, 3, (1997) · Zbl 0945.03086
[27] R. Raz, Resolution lower bounds for the weak pigeonhole principle, in: Proc. of the 34th Annual ACM Symposium on Theory of Computing, STOC’02, Montreal, Canada, 2002, pp. 553-562 · Zbl 1192.03043
[28] Razborov, A., Improved resolution lower bounds for the weak pigeonhole principle, Electronic colloquium on computational complexity, 8, 55, (2001)
[29] Rollon, E.; Larrosa, J., Bucket elimination for multiobjective optimization problems, Journal of heuristics, 12, 4-5, (2006) · Zbl 1125.90046
[30] Shen, H.; Zhang, H., Study of lower bound functions for MAX-2-SAT, (), 185-190
[31] Urquhart, A., Hard examples for resolution, Journal of the ACM, 34, 1, 209-219, (1987) · Zbl 0639.68093
[32] Xing, Z.; Zhang, W., Efficient strategies for (weighted) maximum satisfiability, (), 690-705 · Zbl 1152.68591
[33] Xing, Z.; Zhang, W., An efficient exact algorithm for (weighted) maximum satisfiability, Artificial intelligence, 164, 2, 47-80, (2005) · Zbl 1132.68716
[34] Zhang, H.; Shen, H.; Manya, F., Exact algorithms for MAX-SAT, Electronic notes in theoretical computer science, 86, 1, (2003) · Zbl 1261.68073
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.