Solving Set Cover and Dominating Set via Maximum Satisfiability

AAAI, pp. 1569-1576, 2020.

Cited by: 2|Bibtex|Views43|Links
Keywords:
real worldset covering problemOperations Researchlogical languageinitial solutionMore(16+)
Weibo:
Experiments result showed that our algorithm is better than all state of the art algorithms for Set Covering Problem, Dominating Set Problem and Maximum Satisfiability

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
Download tables as Excel
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.
    Google ScholarLocate open access versionFindings
  • Ansotegui, C.; Bonet, M. L.; and Levy, J. 2013. Sat-based maxsat algorithms. Artif. Intell. 196:77–105.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Beasley, J. E., and Chu, P. 1996. A genetic algorithm for the set covering problem. European Journal of Operational Research 94(2):392–404.
    Google ScholarLocate open access versionFindings
  • Beasley, J. E. 1990. Or-library: distributing test problems by electronic mail. Journal of the operational research society 41(11):1069–1072.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Cai, S.; Luo, C.; Lin, J.; and Su, K. 2016. New local search methods for partial maxsat. Artif. Intell. 240:1–18.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Caprara, A.; Fischetti, M.; Toth, P.; Vigo, D.; and Guida, P. L. 1997. Algorithms for railway crew management. Math. Program. 79:125–141.
    Google ScholarLocate open access versionFindings
  • Caprara, A.; Toth, P.; and Fischetti, M. 2000. Algorithms for the set covering problem. Annals OR 98(1-4):353–371.
    Google ScholarLocate open access versionFindings
  • Chalupa, D. 2018. An order-based algorithm for minimum dominating set with application in graph mining. Inf. Sci. 426:101–116.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Proceedings, 225–239.
    Google ScholarLocate open access versionFindings
  • Demirovic, E., and Musliu, N. 2017. Maxsat-based large neighborhood search for high school timetabling. Computers & OR 78:172– 180.
    Google ScholarFindings
  • Demirovic, E.; Musliu, N.; and Winter, F. 2019. Modeling and solving staff scheduling with partial weighted maxsat. Annals OR 275(1):79–99.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Jovanovic; Raka; Milan; and Dana. 2010. Ant colony optimization applied to minimum weight dominating set problem. Plant Physiology 146(3):173–176.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • Proceedings, 438–445.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments