×

CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. (English) Zbl 1402.68163

Summary: Weighted maximum satisfiability and (unweighted) partial maximum satisfiability (PMS) are two significant generalizations of maximum satisfiability (MAX-SAT), and weighted partial maximum satisfiability (WPMS) is the combination of the two, with more important applications in practice. Recently, great breakthroughs have been made on stochastic local search (SLS) for weighted MAX-SAT and PMS, resulting in several state-of-the-art SLS algorithms CCLS, Dist and DistUP. However, compared to the great progress of SLS on weighted MAX-SAT and PMS, the performance of SLS on WPMS lags far behind. In this paper, we present a new SLS algorithm named CCEHC for WPMS. CCEHC employs an extended framework of CCLS with a heuristic emphasizing hard clauses, called EHC. With strong accents on hard clauses, EHC has three components: a variable selection mechanism focusing on configuration checking based only on hard clauses, a weighting scheme for hard clauses, and a biased random walk component. Extensive experiments demonstrate that CCEHC significantly outperforms its state-of-the-art SLS competitors. Further experimental results on comparing CCEHC with a state-of-the-art complete solver show the effectiveness of CCEHC on a number of application WPMS instances, and indicate that CCEHC might be beneficial in practice. Also, empirical analyses confirm the effectiveness of each component underlying the EHC heuristic.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Purdom, P. W., Solving satisfiability with less searching, IEEE Trans. Pattern Anal. Mach. Intell., 6, 4, 510-513 (1984) · Zbl 0545.68052
[2] Smyth, K.; Hoos, H. H.; Stützle, T., Iterated robust tabu search for MAX-SAT, (Proceedings of Canadian Conference on AI 2003 (2003)), 129-144
[3] Cai, S.; Luo, C.; Thornton, J.; Su, K., Tailoring local search for partial MaxSAT, (Proceedings of AAAI 2014 (2014)), 2623-2629
[4] Allouche, D.; Traoré, S.; André, I.; de Givry, S.; Katsirelos, G.; Barbe, S.; Schiex, T., Computational protein design as a cost function network optimization problem, (Proceedings of CP 2012 (2012)), 840-849
[5] Allouche, D.; André, I.; Barbe, S.; Davies, J.; de Givry, S.; Katsirelos, G.; O’Sullivan, B.; Prestwich, S. D.; Schiex, T.; Traoré, S., Computational protein design as an optimization problem, Artif. Intell., 212, 59-79 (2014) · Zbl 1407.92099
[6] Naji-Azimi, Z.; Toth, P.; Galli, L., An electromagnetism metaheuristic for the unicost set covering problem, Eur. J. Oper. Res., 205, 2, 290-300 (2010) · Zbl 1188.90218
[7] Liao, X.; Koshimura, M.; Fujita, H.; Hasegawa, R., Solving the coalition structure generation problem with MaxSAT, (Proceedings of ICTAI 2012 (2012)), 910-915
[8] Chieu, H. L.; Lee, W. S., Relaxed survey propagation for the weighted maximum satisfiability problem, J. Artif. Intell. Res., 36, 229-266 (2009) · Zbl 1192.68640
[9] Lin, H.; Su, K., Exploiting inference rules to compute lower bounds for MAX-SAT solving, (Proceedings of IJCAI 2007 (2007)), 2334-2339
[10] Lin, H.; Su, K.; Li, C. M., Within-problem learning for efficient lower bound computation in Max-SAT solving, (Proceedings of AAAI 2008 (2008)), 351-356
[11] Li, C. M.; Manyà, F.; Mohamedou, N. O.; Planes, J., Exploiting cycle structures in Max-SAT, (Proceedings of SAT 2009 (2009)), 467-480 · Zbl 1247.68256
[12] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203
[13] Davis, M.; Logemann, G.; Loveland, D. W., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002
[14] Ansótegui, C.; Bonet, M. L.; Gabàs, J.; Levy, J., Improving WPM2 for (weighted) partial MaxSAT, (Proceedings of CP 2013 (2013)), 117-132
[15] Ansótegui, C.; Bonet, M. L.; Levy, J., SAT-based MaxSAT algorithms, Artif. Intell., 196, 77-105 (2013) · Zbl 1270.68265
[16] Narodytska, N.; Bacchus, F., Maximum satisfiability using core-guided MaxSAT resolution, (Proceedings of AAAI 2014 (2014)), 2717-2723
[17] Silva, J. P.M.; Sakallah, K. A., GRASP - a new search algorithm for satisfiability, (Proceedings of ICCAD 1996 (1996)), 220-227
[18] Silva, J. P.M.; Sakallah, K. A., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388
[19] Hoos, H. H.; Stützle, T., Stochastic Local Search: Foundations & Applications (2004), Elsevier/Morgan Kaufmann · Zbl 1126.68032
[20] Selman, B.; Levesque, H. J.; Mitchell, D. G., A new method for solving hard satisfiability problems, (Proceedings of AAAI 1992 (1992)), 440-446
[21] Selman, B.; Kautz, H. A.; Cohen, B., Noise strategies for improving local search, (Proceedings of AAAI 1994 (1994)), 337-343
[22] Luo, C.; Cai, S.; Wu, W.; Jie, Z.; Su, K., CCLS: an efficient local search algorithm for weighted maximum satisfiability, IEEE Trans. Comput., 64, 7, 1830-1843 (2015) · Zbl 1360.68786
[23] Cai, S.; Luo, C.; Lin, J.; Su, K., New local search methods for partial MaxSAT, Artif. Intell., 240, 1-18 (2016) · Zbl 1386.68152
[24] Cai, S.; Su, K., Local search for Boolean satisfiability with configuration checking and subscore, Artif. Intell., 204, 75-98 (2013) · Zbl 1334.68200
[25] Cai, S.; Luo, C.; Su, K., Scoring functions based on second level score for k-SAT with long clauses, J. Artif. Intell. Res., 51, 413-441 (2014) · Zbl 1367.68261
[26] Cai, S.; Su, K.; Luo, C.; Sattar, A., NuMVC: an efficient local search algorithm for minimum vertex cover, J. Artif. Intell. Res., 46, 687-716 (2013) · Zbl 1280.90098
[27] Luo, C.; Su, K.; Cai, S., Improving local search for random 3-SAT using quantitative configuration checking, (Proceedings of ECAI 2012 (2012)), 570-575 · Zbl 1327.68225
[28] Luo, C.; Cai, S.; Wu, W.; Su, K., Focused random walk with configuration checking and break minimum for satisfiability, (Proceedings of CP 2013 (2013)), 481-496
[29] Luo, C.; Cai, S.; Su, K.; Wu, W., Clause states based configuration checking in local search for satisfiability, IEEE Trans. Cybern., 45, 5, 1014-1027 (2015)
[30] Cai, S.; Jie, Z.; Su, K., An effective variable selection heuristic in SLS for weighted Max-2-SAT, J. Heuristics, 21, 3, 433-456 (2015)
[31] Luo, C.; Cai, S.; Wu, W.; Su, K., Double configuration checking in stochastic local search for satisfiability, (Proceedings of AAAI 2014 (2014)), 2703-2709
[32] Wu, Z.; Wah, B. W., An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems, (Proceedings of AAAI 2000 (2000)), 310-315
[33] Schuurmans, D.; Southey, F.; Holte, R. C., The exponentiated subgradient algorithm for heuristic Boolean programming, (Proceedings of IJCAI 2001 (2001)), 334-341
[34] Hutter, F.; Tompkins, D. A.D.; Hoos, H. H., Scaling and probabilistic smoothing: efficient dynamic local search for SAT, (Proceedings of CP 2002 (2002)), 233-248
[35] Thornton, J.; Pham, D. N.; Bain, S.; Ferreira, V., Additive versus multiplicative clause weighting for SAT, (Proc. of AAAI 2004 (2004)), 191-196
[36] Ishtaiwi, A.; Thornton, J.; Sattar, A.; Pham, D. N., Neighbourhood clause weight redistribution in local search for SAT, (Proceedings of CP 2005 (2005)), 772-776 · Zbl 1153.68050
[37] Jiang, Y.; Kautz, H.; Selman, B., Solving problems with hard and soft constraints using a stochastic algorithm for MAX-SAT, (First International Joint Workshop on Artificial Intelligence and Operations Research (1995))
[38] Ansótegui, C.; Gabàs, J., Solving (weighted) partial MaxSAT with ILP, (Proceedings of CPAIOR 2013 (2013)), 403-409
[39] Xu, K.; Li, W., Many hard examples in exact phase transitions, Theor. Comput. Sci., 355, 3, 291-302 (2006) · Zbl 1088.68163
[40] Xu, K.; Li, W., Exact phase transitions in random constraint satisfaction problems, J. Artif. Intell. Res., 12, 93-103 (2000) · Zbl 0940.68099
[41] Gwynne, M.; Kullmann, O., Towards a better understanding of SAT translations, (The Twelfth International Workshop on Logic and Computational Complexity (2011))
[42] Sánchez, M.; de Givry, S.; Schiex, T., Mendelian error detection in complex pedigrees using weighted constraint satisfaction techniques, Constraints, 13, 1-2, 130-154 (2008) · Zbl 1144.92324
[43] Sanchez, J. M., Cluster expansions and the configurational energy of alloys, Phys. Rev. B, 48, 18, 14013-14015 (1993)
[44] Liu, B.; Baas, B. M., Parallel AES encryption engines for many-core processor arrays, IEEE Trans. Comput., 62, 3, 536-547 (2013) · Zbl 1365.68243
[45] Trimberger, S., Security in SRAM FPGAs, IEEE Des. Test Comput., 24, 6, 581 (2007)
[46] Kermani, M. M.; Reyhani-Masoleh, A., Concurrent structure-independent fault detection schemes for the advanced encryption standard, IEEE Trans. Comput., 59, 5, 608-622 (2010) · Zbl 1366.94518
[47] Aceto, L.; Hansen, J. A.; Ingólfsdóttir, A.; Johnsen, J.; Knudsen, J., The complexity of checking consistency of pedigree information and related problems, J. Comput. Sci. Technol., 19, 1, 42-59 (2004)
[48] Huang, W.; Kitchaev, D. A.; Dacek, S.; Rong, Z.; Urban, A.; Cao, S.; Luo, C.; Ceder, G., Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAX-SAT, Phys. Rev. B, 94, Article 134424 pp. (2016)
[49] Ising, E., Beitrag zur theorie des ferromagnetismus, Z. Phys., 31, 1, 253-258 (1925) · Zbl 1439.82056
[50] van de Walle, A.; Ceder, G., Automating first-principles phase diagram calculations, J. Phase Equilib., 23, 4, 348-359 (2002)
[51] Hinuma, Y.; Meng, Y. S.; Ceder, G., Temperature-concentration phase diagram of \(P 2 \text{-Na}_x \text{CoO}_2\) from first-principles calculations, Phys. Rev. B, 77, Article 224111 pp. (2008)
[52] Kügel, A., Improved exact solver for the weighted Max-SAT problem, (Proceedings of Pragmatics of SAT 2010 (2010)), 15-27
[53] Abramé, A.; Habet, D., Inference rules in local search for Max-SAT, (Proceedings of ICTAI 2012 (2012)), 207-214
[54] Berre, D. L.; Parrain, A., The Sat4j library, release 2.2, J. Satisf. Boolean Model. Comput., 7, 2-3, 59-64 (2010)
[55] Thornton, J.; Bain, S.; Sattar, A.; Pham, D. N., A two level local search for MAX-SAT problems with hard and soft constraints, (Proceedings of Australian Joint Conference on AI 2002 (2002)), 603-614 · Zbl 1032.68753
[56] Roussel, O., Controlling a solver execution with the runsolver tool, J. Satisf. Boolean Model. Comput., 7, 4, 139-144 (2011) · Zbl 1331.68210
[57] Hutter, F.; Hoos, H. H.; Leyton-Brown, K.; Stützle, T., ParamILS: an automatic algorithm configuration framework, J. Artif. Intell. Res., 36, 267-306 (2009) · Zbl 1192.68831
[58] Hutter, F.; Hoos, H. H.; Leyton-Brown, K., Sequential model-based optimization for general algorithm configuration, (Proceedings of LION 2011 (2011)), 507-523
[59] Cai, S., Balance between complexity and quality: local search for minimum vertex cover in massive graphs, (Proceedings of IJCAI 2015 (2015)), 747-753
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.