Solving Set Cover and Dominating Set via Maximum Satisfiability
AAAI, pp. 1569-1576, 2020.
Keywords:
Weibo:
Abstract:
The Set Covering Problem (SCP) and Dominating Set Problem (DSP) are NP-hard and have many real world applications. SCP and DSP can be encoded into Maximum Satisfiability (MaxSAT) naturally and the resulting instances share a special structure. In this paper, we develop an efficient local search solver for MaxSAT instances of this kind. Ou...More
Code:
Data:
Introduction
- Many combinatorial optimization problems that arise in the real world are difficult to solve partly because they present computational challenges.
- This paper is concerned with developing a practical algorithm to solve two optimization problems modelled in a particular logical language, Maximum Satisfiability (MaxSAT).
- MaxSAT is an optimization version of SAT, and its most general form contains both hard clauses and weighted soft clauses
- Such a MaxSAT problem is referred to as weighted Partial MaxSAT (WPMS), where the goal is to find an assignment that satisfies all the hard clauses and maximize the total weight of satisfied soft clauses
Highlights
- Many combinatorial optimization problems that arise in the real world are difficult to solve partly because they present computational challenges
- We propose a weighted Partial MaxSAT (WPMS) solver to solve two closely related NP hard combinatorial optimization problems of importance, namely Set Cover Problem (SCP) and Dominating Set Problem (DSP)
- We propose a CC strategy that is tailored for WPMS instances from Set Covering Problem (SCP) and DSP
- We designed a local search algorithm tailored for such instances
- Experiments result showed that our algorithm is better than all state of the art algorithms for SCP, DSP and Maximum Satisfiability (MaxSAT)
- DomSAT performs significantly better than all the competitors
- The strong results show that exploiting the features of the instances from specific domains in MaxSAT solving would lead to more effective solvers
Results
- Experiment Results on SCP instances
In this subsection, the authors compare DomSAT with state of the art solvers on SCP benchmarks. - Rail instances are large scale industrial instances ( > 10000 variables) and are considered difficult to solve.
- Experiment results on these instances are presented in Table 3.
- For 130 instances, DomSAT find the best solution for 124 of them while this number is only 18, 2, 6, 0 for FastWMDS, SATLike, Loandra and Open-wbo respectively
- These results show the strong.
- The authors can see that, without reduction procedure, the algorithm is still much better than other solvers
Conclusion
- The authors formulated SCP and DSP into weighted Partial Maximum Satisfiability and proposed several reduction rules to simplify these MaxSAT instances.
- Experiments result showed that the algorithm is better than all state of the art algorithms for SCP, DSP and MaxSAT.
- The strong results show that exploiting the features of the instances from specific domains in MaxSAT solving would lead to more effective solvers.
- The authors would like to explore features of other combinatorial optimization problems to design MaxSAT solvers for them
Summary
Introduction:
Many combinatorial optimization problems that arise in the real world are difficult to solve partly because they present computational challenges.- This paper is concerned with developing a practical algorithm to solve two optimization problems modelled in a particular logical language, Maximum Satisfiability (MaxSAT).
- MaxSAT is an optimization version of SAT, and its most general form contains both hard clauses and weighted soft clauses
- Such a MaxSAT problem is referred to as weighted Partial MaxSAT (WPMS), where the goal is to find an assignment that satisfies all the hard clauses and maximize the total weight of satisfied soft clauses
Objectives:
Exploitation Mode: If α is not feasible, the authors aim to get a feasible assignment while at the same time try to keep soft cost as small as possible.Results:
Experiment Results on SCP instances
In this subsection, the authors compare DomSAT with state of the art solvers on SCP benchmarks.- Rail instances are large scale industrial instances ( > 10000 variables) and are considered difficult to solve.
- Experiment results on these instances are presented in Table 3.
- For 130 instances, DomSAT find the best solution for 124 of them while this number is only 18, 2, 6, 0 for FastWMDS, SATLike, Loandra and Open-wbo respectively
- These results show the strong.
- The authors can see that, without reduction procedure, the algorithm is still much better than other solvers
Conclusion:
The authors formulated SCP and DSP into weighted Partial Maximum Satisfiability and proposed several reduction rules to simplify these MaxSAT instances.- Experiments result showed that the algorithm is better than all state of the art algorithms for SCP, DSP and MaxSAT.
- The strong results show that exploiting the features of the instances from specific domains in MaxSAT solving would lead to more effective solvers.
- The authors would like to explore features of other combinatorial optimization problems to design MaxSAT solvers for them
Tables
- Table1: Results on unweighted Set Cover Problem
- Table2: Summary Results on random weighted SCP instances
- Table3: Results on industrial weighted SCP instances
- Table4: Summary Results on DSP benchmarks
Funding
- This work is supported by Youth Innovation Promotion Association, Chinese Academy of Sciences (No.2017150)
Reference
- Ansotegui, C., and Gabas, J. 2017. WPM3: an (in)complete algorithm for weighted partial maxsat. Artif. Intell. 250:37–57.
- Ansotegui, C.; Bonet, M. L.; and Levy, J. 2013. Sat-based maxsat algorithms. Artif. Intell. 196:77–105.
- Aoun, B.; Boutaba, R.; Iraqi, Y.; and Kenward, G. W. 2006. Gateway placement optimization in wireless mesh networks with qos constraints. IEEE Journal on Selected Areas in Communications 24(11):2127–2136.
- Bautista, J., and Pereira, J. 2006. Modeling the problem of locating collection areas for urban waste management. an application to the metropolitan area of barcelona. Omega 34(6):617–629.
- Beasley, J. E., and Chu, P. 1996. A genetic algorithm for the set covering problem. European Journal of Operational Research 94(2):392–404.
- Beasley, J. E. 1990. Or-library: distributing test problems by electronic mail. Journal of the operational research society 41(11):1069–1072.
- Cai, S., and Su, K. 2011. Local search with configuration checking for SAT. In IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, FL, USA, November 7-9, 2011, 59–66.
- Cai, S.; Luo, C.; Thornton, J.; and Su, K. 2014. Tailoring local search for partial maxsat. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Quebec City, Quebec, Canada., 2623–2629.
- Cai, S.; Luo, C.; Lin, J.; and Su, K. 2016. New local search methods for partial maxsat. Artif. Intell. 240:1–18.
- Cai, S. 2015. Balance between complexity and quality: Local search for minimum vertex cover in massive graphs. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, 747–753.
- Caprara, A.; Fischetti, M.; Toth, P.; Vigo, D.; and Guida, P. L. 1997. Algorithms for railway crew management. Math. Program. 79:125–141.
- Caprara, A.; Toth, P.; and Fischetti, M. 2000. Algorithms for the set covering problem. Annals OR 98(1-4):353–371.
- Chalupa, D. 2018. An order-based algorithm for minimum dominating set with application in graph mining. Inf. Sci. 426:101–116.
- Davies, J., and Bacchus, F. 2011. Solving MAXSAT by solving a sequence of simpler SAT instances. In Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011.
- Proceedings, 225–239.
- Demirovic, E., and Musliu, N. 2017. Maxsat-based large neighborhood search for high school timetabling. Computers & OR 78:172– 180.
- Demirovic, E.; Musliu, N.; and Winter, F. 2019. Modeling and solving staff scheduling with partial weighted maxsat. Annals OR 275(1):79–99.
- Fulkerson, D.; Nemhauser, G. L.; and Trotter, L. 1974. Two computationally difficult set covering problems that arise in computing the 1-width of incidence matrices of steiner triple systems. In Approaches to integer programming. 72–81.
- Gao, C.; Weise, T.; and Li, J. 2014. A weighting-based local search heuristic algorithm for the set covering problem. In Proceedings of the IEEE Congress on Evolutionary Computation, CEC 2014, Beijing, China, July 6-11, 2014, 826–831.
- Hedetniemi, S. M.; Hedetniemi, S. T.; Jacobs, D. P.; and Srimani, P. K. 2003. Self-stabilizing algorithms for minimal dominating sets and maximal independent sets. Computers & Mathematics with Applications 46(5-6):805–811.
- Jacobs, L. W., and Brusco, M. J. 1995. Note: A local-search heuristic for large set-covering problems. Naval Research Logistics (NRL) 42(7):1129–1140.
- Jiang, H.; Li, C.; Liu, Y.; and Manya, F. 2018. A two-stage maxsat reasoning approach for the maximum weight clique problem. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, 1338–1346.
- Jovanovic; Raka; Milan; and Dana. 2010. Ant colony optimization applied to minimum weight dominating set problem. Plant Physiology 146(3):173–176.
- Lei, Z., and Cai, S. 2018. Solving (weighted) partial maxsat by dynamic local search for SAT. In Proceedings of the TwentySeventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., 1346–1352.
- Luo, C.; Cai, S.; Su, K.; and Huang, W. 2017. CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artif. Intell. 243:26–44.
- Martins, R.; Manquinho, V. M.; and Lynce, I. 2014. Open-wbo: A modular maxsat solver,. In Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014.
- Proceedings, 438–445.
- Narodytska, N., and Bacchus, F. 2014. Maximum satisfiability using core-guided maxsat resolution. In Proceedings of the TwentyEighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Quebec City, Quebec, Canada., 2717–2723.
- Nitash, C. G., and Singh, A. 2014. An artificial bee colony algorithm for minimum weight dominating set. In 2014 IEEE Symposium on Swarm Intelligence, SIS 2014, Orlando, FL, USA, December 9-12, 2014, 313–319.
- Shen, C., and Li, T. 2010. Multi-document summarization via the minimum dominating set. In Proceedings of the 23rd international conference on computational linguistics, 984–992.
- Wang, Y.; Cai, S.; Chen, J.; and Yin, M. 2018. A fast local search algorithm for minimum weight dominating set problem on massive graphs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 1319, 2018, Stockholm, Sweden., 1514–1522.
Tags
Comments