New local search methods for partial MaxSAT.

*(English)*Zbl 1386.68152Summary: Maximum Satisfiability (MaxSAT) is the optimization version of the Satisfiability (SAT) problem. Partial Maximum Satisfiability (PMS) is a generalization of MaxSAT which involves hard and soft clauses and has important real world applications. Local search is a popular approach to solving SAT and MaxSAT and has witnessed great success in these two problems. However, unfortunately, local search algorithms for PMS do not benefit much from local search techniques for SAT and MaxSAT, mainly due to the fact that it contains both hard and soft clauses. This feature makes it more challenging to design efficient local search algorithms for PMS, which is likely the reason of the stagnation of this direction in more than one decade.

In this paper, we propose a number of new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. The first three ideas, including weighting for hard clauses, separating hard and soft score, and a variable selection heuristic based on hard and soft score, are used to develop a local search algorithm for PMS called Dist. The fourth idea, which uses unit propagation with priority on hard unit clauses to generate the initial assignment, is used to improve Dist on industrial instances, leading to the DistUP algorithm.

The effectiveness of our solvers and ideas is illustrated through experimental evaluations on all PMS benchmarks from the MaxSAT Evaluation 2014. According to our experimental results, Dist shows a significant improvement over previous local search solvers on all benchmarks. We also compare our solvers with state-of-the-art complete PMS solvers and a state-of-the-art portfolio solver, and the results show that our solvers have better performance in random and crafted instances but worse in industrial instances. The good performance of Dist has also been confirmed by the fact that Dist won all random and crafted categories of PMS and Weighted PMS in the incomplete solvers track of the MaxSAT Evaluation 2014.

In this paper, we propose a number of new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. The first three ideas, including weighting for hard clauses, separating hard and soft score, and a variable selection heuristic based on hard and soft score, are used to develop a local search algorithm for PMS called Dist. The fourth idea, which uses unit propagation with priority on hard unit clauses to generate the initial assignment, is used to improve Dist on industrial instances, leading to the DistUP algorithm.

The effectiveness of our solvers and ideas is illustrated through experimental evaluations on all PMS benchmarks from the MaxSAT Evaluation 2014. According to our experimental results, Dist shows a significant improvement over previous local search solvers on all benchmarks. We also compare our solvers with state-of-the-art complete PMS solvers and a state-of-the-art portfolio solver, and the results show that our solvers have better performance in random and crafted instances but worse in industrial instances. The good performance of Dist has also been confirmed by the fact that Dist won all random and crafted categories of PMS and Weighted PMS in the incomplete solvers track of the MaxSAT Evaluation 2014.

##### MSC:

68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |

##### Software:

CCASat; CCLS; MaxHS; MiniMaxSat; Open-WBO; Paramils; QMaxSAT; RPOLY; Runsolver; Sat4j; SMAC; UBCSAT; WPM2
Full Text:
DOI

##### References:

[1] | Abramé, André; Habet, Djamal, Inference rules in local search for MAX-SAT, (IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI, Athens, Greece, (2012)), 207-214 |

[2] | Abramé, André; Habet, Djamal, Ahmaxsat: description and evaluation of a branch and bound MAX-SAT solver, J. Satisf. Boolean Model. Comput., 9, 89-128, (2015) |

[3] | Ansótegui, Carlos; Gabàs, Joel, Solving (weighted) partial maxsat with ILP, (Proceedings of the 10th International Conference of Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, CPAIOR, Yorktown Heights, NY, USA, (2013)), 403-409 |

[4] | Ansótegui, Carlos; Bonet, Maria Luisa; Gabàs, Joel; Levy, Jordi, Improving WPM2 for (weighted) partial maxsat, (Proceedings of the 19th International Conference of Principles and Practice of Constraint Programming, CP, Uppsala, Sweden, (2013)), 117-132 |

[5] | Ansótegui, Carlos; Bonet, Maria Luisa; Levy, Jordi, SAT-based maxsat algorithms, Artif. Intell., 196, 77-105, (2013) · Zbl 1270.68265 |

[6] | Ansótegui, Carlos; Malitsky, Yuri; Sellmann, Meinolf, Maxsat by improved instance-specific algorithm configuration, (Proceedings of the 28th AAAI Conference on Artificial Intelligence, AAAI, Québec City, Québec, Canada, (2014)), 2594-2600 · Zbl 1352.68218 |

[7] | Argelich, Josep; Li, Chu Min; Manyà, Felip; Planes, Jordi, The maxsat evaluations 2010-2015 · Zbl 1159.68561 |

[8] | Balint, Adrian; Fröhlich, Andreas, Improving stochastic local search for SAT with a new probability distribution, (Proceedings of the 13th International Conference of Theory and Applications of Satisfiability Testing, SAT, Edinburgh, UK, (2010)), 10-15 · Zbl 1306.68150 |

[9] | Le Berre, Daniel; Parrain, Anne, The sat4j library, release 2.2, J. Satisf. Boolean Model. Comput., 7, 2-3, 59-64, (2010) |

[10] | Cai, Shaowei; Su, Kaile, Local search for Boolean satisfiability with configuration checking and subscore, Artif. Intell., 204, 75-98, (2013) · Zbl 1334.68200 |

[11] | Cai, Shaowei; Su, Kaile; Sattar, Abdul, Local search with edge weighting and configuration checking heuristics for minimum vertex cover, Artif. Intell., 175, 9-10, 1672-1696, (2011) · Zbl 1225.68242 |

[12] | Cai, Shaowei; Luo, Chuan; Thornton, John; Su, Kaile, Tailoring local search for partial maxsat, (Proceedings of the 28th AAAI Conference on Artificial Intelligence, AAAI, Québec City, Québec, Canada, (2014)), 2623-2629 |

[13] | Cai, Shaowei; Luo, Chuan; Su, Kaile, Ccanr: a configuration checking based local search solver for non-random satisfiability, (Proceedings of 18th International Conference of Theory and Applications of Satisfiability Testing, SAT, Austin, TX, USA, (2015)), 1-8 · Zbl 06512560 |

[14] | Cai, Shaowei, Balance between complexity and quality: local search for minimum vertex cover in massive graphs, (Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI, Buenos Aires, Argentina, (2015)), 747-753 |

[15] | Cha, Byungki; Iwama, Kazuo; Kambayashi, Yahiko; Miyazaki, Shuichi, Local search algorithms for partial maxsat, (Proceedings of the 14th National Conference on Artificial Intelligence, AAAI, Providence, Rhode Island, (1997)), 263-268 |

[16] | Davies, Jessica; Bacchus, Fahiem, Solving MAXSAT by solving a sequence of simpler SAT instances, (Proceedings of the 17th International Conference of Principles and Practice of Constraint Programming, CP, Perugia, Italy, (2011)), 225-239 |

[17] | Davies, Jessica; Cho, Jeremy; Bacchus, Fahiem, Using learnt clauses in maxsat, (Proceedings of the 16th International Conference Principles and Practice of Constraint Programming, CP, St. Andrews, Scotland, UK, (2010)), 176-190 |

[18] | Davies, Jessica, Solving maxsat by decoupling optimization and satisfaction, (2013), PhD thesis |

[19] | Fu, Zhaohui; Malik, Sharad, On solving the partial MAX-SAT problem, (Proceedings of the 9th International Conference of Theory and Applications of Satisfiability Testing, SAT, Seattle, WA, USA, (2006)), 252-265 · Zbl 1187.68540 |

[20] | Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L., Haplotype inference with pseudo-Boolean optimization, Ann. Oper. Res., 184, 1, 137-162, (2011) · Zbl 1215.92043 |

[21] | Hains, Doug; Whitley, Darrell; Howe, Adele E.; Chen, Wenxiang, Hyperplane initialized local search for MAXSAT, (Proceedings of Genetic and Evolutionary Computation Conference, GECCO, Amsterdam, The Netherlands, (2013)), 805-812 |

[22] | Heras, Federico; Bañeres, David, The impact of MAX-SAT resolution-based preprocessors on local search solvers, J. Satisf. Boolean Model. Comput., 7, 2-3, 89-126, (2010) |

[23] | Heras, Federico; Larrosa, Javier; Oliveras, Albert, Minimaxsat: an efficient weighted MAX-SAT solver, J. Artif. Intell. Res., 31, 1-32, (2008) · Zbl 1183.68578 |

[24] | Heule, Marijn J. H.; Schaub, Torsten, What’s hot in the SAT and ASP competitions, (Proceedings of the 29th AAAI Conference on Artificial Intelligence, AAAI, Austin, Texas, USA, (2015)), 4322-4323 |

[25] | Hoos, Holger H.; Stützle, Thomas, Stochastic local search: foundations & applications, (2005), Elsevier/Morgan Kaufmann · Zbl 1126.68032 |

[26] | Hoos, Holger H., On the run-time behaviour of stochastic local search algorithms for SAT, (Proceedings of the 16th National Conference on Artificial Intelligence, AAAI, Orlando, Florida, USA, (1999)), 661-666 |

[27] | Hutter, Frank; Tompkins, Dave A. D.; Hoos, Holger H., Scaling and probabilistic smoothing: efficient dynamic local search for SAT, (Proceedings of the 8th International Conference of Principles and Practice of Constraint Programming, CP, Ithaca, NY, USA, (2002), Springer), 233-248 |

[28] | Hutter, Frank; Hoos, Holger H.; Stützle, Thomas, Efficient stochastic local search for MPE solving, (Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI, Edinburgh, Scotland, UK, (2005)), 169-174 |

[29] | Hutter, Frank; Hoos, Holger H.; Leyton-Brown, Kevin; Stützle, Thomas, Paramils: an automatic algorithm configuration framework, J. Artif. Intell. Res., 36, 267-306, (2009) · Zbl 1192.68831 |

[30] | Hutter, Frank; Hoos, Holger H.; Leyton-Brown, Kevin, Sequential model-based optimization for general algorithm configuration, (Proceedings of the 5th International Conference of Learning and Intelligent Optimization, LION, Rome, Italy, (2011)), 507-523 |

[31] | Jiang, Yuejun; Kautz, Henry; Selman, Bart, 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)) |

[32] | Kask, K.; Dechter, R., Stochastic local search for Bayesian networks, (Proceedings of the 7th International Workshop on Artificial Intelligence and Statistics, AISTATS, Fort Lauderdale, Florida, US, (1999)) · Zbl 0971.68035 |

[33] | Koshimura, Miyuki; Zhang, Tong; Fujita, Hiroshi; Hasegawa, Ryuzo, Qmaxsat: a partial MAX-SAT solver, J. Satisf. Boolean Model. Comput., 8, 1/2, 95-100, (2012) · Zbl 1331.68209 |

[34] | Li, Chu Min; Li, Yu, Satisfying versus falsifying in local search for satisfiability - (poster presentation), (Cimatti, Alessandro; Sebastiani, Roberto, Proceedings of the 15th International Conference of Theory and Applications of Satisfiability Testing, SAT, Trento, Italy, (2012)), 477-478 |

[35] | Li, Chu Min; Manyà, Felip; Planes, Jordi, New inference rules for MAX-SAT, J. Artif. Intell. Res., 30, 321-359, (2007) · Zbl 1182.68254 |

[36] | Li, Chu Min; Manyà, Felip; Mohamedou, Nouredine Ould; Planes, Jordi, Exploiting cycle structures in MAX-SAT, (Proceedings of the 12th International Conference of Theory and Applications of Satisfiability Testing, SAT, Swansea, UK, (2009)), 467-480 · Zbl 1247.68256 |

[37] | Lin, Han; Su, Kaile; Li, Chu Min, Within-problem learning for efficient lower bound computation in MAX-SAT solving, (Proceedings of the 23rd AAAI Conference on Artificial Intelligence, AAAI, Chicago, Illinois, USA, (2008)), 351-356 |

[38] | Luo, Chuan; Cai, Shaowei; Wu, Wei; Jie, Zhong; Su, Kaile, CCLS: an efficient local search algorithm for weighted maximum satisfiability, IEEE Trans. Comput., 64, 7, 1830-1843, (2015) · Zbl 1360.68786 |

[39] | Mann, Zoltán Ádám, Typical-case complexity and the SAT competitions, (Proceedings of the 5th Pragmatics of SAT Workshop, POS@SAT, Vienna, Austria, (2014)), 72-87 |

[40] | Martins, Ruben; Joshi, Saurabh; Manquinho, Vasco M.; Lynce, Inês, Incremental cardinality constraints for maxsat, (Proceedings of the 20th International Conference of Principles and Practice of Constraint Programming, CP, Lyon, France, (2014)), 531-548 |

[41] | Martins, Ruben; Manquinho, Vasco M.; Lynce, Inês, Open-WBO: a modular maxsat solver, (Proceedings of the 17th International Conference of Theory and Applications of Satisfiability Testing, Vienna, Austria, (2014)), 438-445 · Zbl 1423.68461 |

[42] | Mengshoel, Ole J.; Wilkins, David C.; Roth, Dan, Initialization and restart in stochastic local search: computing a most probable explanation in Bayesian networks, IEEE Trans. Knowl. Data Eng., 23, 2, 235-247, (2011) · Zbl 1213.68582 |

[43] | Morgado, António; Heras, Federico; Liffiton, Mark H.; Planes, Jordi; Marques-Silva, Joao, Iterative and core-guided maxsat solving: a survey and assessment, Constraints, 18, 4, 478-534, (2013) · Zbl 1317.90199 |

[44] | Morgado, António; Dodaro, Carmine; Marques-Silva, Joao, Core-guided maxsat with soft cardinality constraints, (Proceedings of the 20th International Conference of Principles and Practice of Constraint Programming, CP, Lyon, France, (2014)), 564-573 |

[45] | Narodytska, Nina; Bacchus, Fahiem, Maximum satisfiability using core-guided maxsat resolution, (Proceedings of the 28th AAAI Conference on Artificial Intelligence, AAAI, Québec City, Québec, Canada, (2014)), 2717-2723 · Zbl 1423.68432 |

[46] | Nghia Pham, Duc; Thornton, John; Gretton, Charles; Sattar, Abdul, Advances in local search for satisfiability, (Proceedings of the 20th Australian Joint Conference on Artificial Intelligence, AI, Gold Coast, Australia, (2007), Springer), 213-222 |

[47] | Roussel, Olivier, Controlling a solver execution with the runsolver tool, J. Satisf. Boolean Model. Comput., 7, 4, 139-144, (2011) · Zbl 1331.68210 |

[48] | Sakai, Masahiro, Scip-maxsat |

[49] | Smyth, Kevin; Hoos, Holger H.; Stützle, Thomas, Iterated robust tabu search for MAX-SAT, (Proceedings of the 16th Canadian Conference on AI, Halifax, Canada, (2003)), 129-144 |

[50] | Thornton, John; Sattar, Abdul, Dynamic constraint weighting for over-constrained problems, (Proceedings of the 5th Pacific Rim International Conference on Artificial Intelligence, PRICAI, Singapore, (1998)), 377-388 |

[51] | Thornton, John; Bain, Stuart; Sattar, Abdul; Pham, Duc Nghia, A two level local search for MAX-SAT problems with hard and soft constraints, (Proceedings of the 15th Australian Joint Conference on Artificial Intelligence, AI, Canberra, Australia, (2002)), 603-614 · Zbl 1032.68753 |

[52] | Thornton, John; Nghia Pham, Duc; Bain, Stuart; Ferreira, Valnir, Additive versus multiplicative clause weighting for SAT, (Proceedings of the 19th National Conference on Artificial Intelligence, AAAI, San Jose, California, USA, (2004), AAAI Press/The MIT Press), 191-196 |

[53] | Tompkins, Dave A. D.; Hoos, Holger H., UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT & MAX-SAT, (Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT, Vancouver, BC, Canada, (2004)), 37-46 · Zbl 1122.68620 |

[54] | Whitley, Darrell; Howe, Adele E.; Hains, Doug, Greedy or not? best improving versus first improving stochastic local search for MAXSAT, (Proceedings of the 27th AAAI Conference on Artificial Intelligence, AAAI, Bellevue, Washington, USA, (2013)), 940-946 |

[55] | Zilberstein, Shlomo, Using anytime algorithms in intelligent systems, AI Mag., 17, 3, 73-83, (1996) |

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.