NuDist: An Efficient Local Search Algorithm for (Weighted) Partial MaxSAT

The Computer Journal, 2019.

Cited by: 0|Bibtex|Views36|
Keywords:
Best from Multiple Selections’maxsat problemoptimization versioncomplete solverlocal searchMore(16+)
Weibo:
MaxSAT Evaluations 2017, our experimental results show that NuDist significantly outperforms previous state-of-the-art local search algorithms

Abstract:

Maximum satisfiability (MaxSAT) is the optimization version of the satisfiability (SAT). Partial MaxSAT (PMS) generalizes SAT and MaxSAT by introducing hard and soft clauses, while Weighted PMS (WPMS) is the weighted version of PMS where each soft clause has a weight. These two problems have many important real-world applications. Local s...More

Code:

Data:

Introduction
  • Maximum satisfiability (MaxSAT) is an optimization version of the famous satisfiability (SAT) problem.
  • SAT problem concerns whether an assignment exists such that all clauses in the CNF formula are satisfied, while the MaxSAT problem is to seek out an assignment that maximizes the number of satisfied clauses in the CNF formula.
  • Weighted PMS (WPMS) is a weighted version of PMS, where each soft clause is associated with a weight, and the goal is to seek out an assignment that satisfied all hard clauses and maximizes the total weight of satisfied soft clauses.
  • The focus of this paper is on developing efficient local search algorithms for solving PMS and WPMS problems
Highlights
  • Maximum satisfiability (MaxSAT) is an optimization version of the famous satisfiability (SAT) problem
  • SAT problem concerns whether an assignment exists such that all clauses in the conjunctive normal form (CNF) formula are satisfied, while the MaxSAT problem is to seek out an assignment that maximizes the number of satisfied clauses in the CNF formula
  • We proposed an efficient algorithm for solving Partial MaxSAT (PMS) and Weighted PMS (WPMS)
  • MaxSAT Evaluations (MSE) 2017, our experimental results show that NuDist significantly outperforms previous state-of-the-art local search algorithms
  • NuDist significantly improves the performance of local search on industrial benchmarks and narrows the gap between the performance of local search and complete solvers
  • Experiment results shows that NuDist is complementary to state-ofthe-art complete solvers on crafted and industrial (W)PMS benchmarks
Results
  • Results on

    PMS_Random benchmark: the three local search solvers have similar performance on PMS_Random benchmark, NuDist is slightly worse.
  • PMS_Crafted benchmark: seen from Table 3, for the 678 instances of PMS_Crafted benchmark, NuDist finds the best solution for 516 of them, while this number is 455 and 494 for Dist and DeciDist, respectively.
  • This indicates an obvious improvement.
Conclusion
  • CONCLUSIONS AND FUTURE WORK

    In this work, the authors proposed an efficient algorithm for solving PMS and WPMS.
  • On a broad range of benchmarks, including all benchmarks of PMS and WPMS problems from MSE and MSE 2017, the experimental results show that NuDist significantly outperforms previous state-of-the-art local search algorithms.
  • Experiment results shows that NuDist is complementary to state-ofthe-art complete solvers on crafted and industrial (W)PMS benchmarks.
  • The authors would like to further improve local search for (W)PMS by using other powerful algorithmic techniques, such as the ‘Unit Propagation’ strategy
Summary
  • Introduction:

    Maximum satisfiability (MaxSAT) is an optimization version of the famous satisfiability (SAT) problem.
  • SAT problem concerns whether an assignment exists such that all clauses in the CNF formula are satisfied, while the MaxSAT problem is to seek out an assignment that maximizes the number of satisfied clauses in the CNF formula.
  • Weighted PMS (WPMS) is a weighted version of PMS, where each soft clause is associated with a weight, and the goal is to seek out an assignment that satisfied all hard clauses and maximizes the total weight of satisfied soft clauses.
  • The focus of this paper is on developing efficient local search algorithms for solving PMS and WPMS problems
  • Objectives:

    The authors aim to design a more efficient local search algorithm for both PMS and WPMS, improving the performance on crafted and industrial benchmarks.
  • Results:

    Results on

    PMS_Random benchmark: the three local search solvers have similar performance on PMS_Random benchmark, NuDist is slightly worse.
  • PMS_Crafted benchmark: seen from Table 3, for the 678 instances of PMS_Crafted benchmark, NuDist finds the best solution for 516 of them, while this number is 455 and 494 for Dist and DeciDist, respectively.
  • This indicates an obvious improvement.
  • Conclusion:

    CONCLUSIONS AND FUTURE WORK

    In this work, the authors proposed an efficient algorithm for solving PMS and WPMS.
  • On a broad range of benchmarks, including all benchmarks of PMS and WPMS problems from MSE and MSE 2017, the experimental results show that NuDist significantly outperforms previous state-of-the-art local search algorithms.
  • Experiment results shows that NuDist is complementary to state-ofthe-art complete solvers on crafted and industrial (W)PMS benchmarks.
  • The authors would like to further improve local search for (W)PMS by using other powerful algorithmic techniques, such as the ‘Unit Propagation’ strategy
Tables
  • Table1: Parameter settings of local search solvers on all PMS benchmarks
  • Table2: Parameter settings of local search solvers on all WPMS benchmarks
  • Table3: Experimental results of NuDist and state-of-the-art local search solvers on all PMS benchmarks
  • Table4: Detailed results of comparing NuDist with local search solvers on PMS_Crafted benchmark
  • Table5: Detailed results of comparing NuDist with local search solvers on PMS_Industrial benchmark
  • Table6: Detailed results of comparing NuDist with local search solvers on PMS_2017 benchmark
  • Table7: Experimental results of NuDist and state-of-the-art local search solvers on all WPMS benchmarks
  • Table8: Detailed results of comparing NuDist with local search solvers on WPMS_Crafted benchmark
  • Table9: Detailed results of comparing NuDist with local search solvers on WPMS_Industrial benchmark
  • Table10: Detailed results of comparing NuDist with local search solvers on WPMS_2017 benchmark
  • Table11: Experimental results of NuDist and state-of-the-art SAT-based solvers on the all PMS and WPMS benchmarks
  • Table12: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on PMS_Crafted benchmark
  • Table13: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on PMS_Industrial benchmark
  • Table14: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on PMS_2017 benchmark
  • Table15: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on WPMS_Crafted benchmark
  • Table16: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on WPMS_Industrial benchmark
  • Table17: Detailed results of comparing NuDist with state-of-the-art SAT-based solvers on WPMS_2017 benchmark
  • Table18: Experimental results of NuDist and its alternative versions on all benchmarks
Download tables as Excel
Funding
  • Youth Innovation Promotion Association, Chinese Academy of Sciences (2017150 to S.C.).
Reference
  • Argelich, J., Li, C.M., Manyà, F. and Planes, J. (2011) Analyzing the Instances of the Maxsat Evaluation. In Sakallah, K.A. and Simon, L. (eds.), Theory and Applications of Satisfiability Testing— SAT 2011, Berlin, Heidelberg, pp. 360–361.
    Google ScholarLocate open access versionFindings
  • Liao, X., Koshimura, M., Fujita, H. and Hasegawa, R. (2012) Solving the Coalition Structure Generation Problem With Maxsat. IEEE Int. Conf. on Tools With Artificial Intelligence, Athens, Greece, pp. 910–915.
    Google ScholarFindings
  • Demirovic, E. and Musliu, N. (2017) Maxsat-based large neighborhood search for high school timetabling. Comput. Oper. Res., 78, 172–180.
    Google ScholarLocate open access versionFindings
  • Demirovic, E., Musliu, N. and Winter, F. (2019) Modeling and solving staff scheduling with partial weighted maxsat. Ann. Oper. Res., 275, 79–99.
    Google ScholarLocate open access versionFindings
  • Fu, Z. and Malik, S. (2006) On Solving the Partial MAX-SAT Problem. Proc. of the 9th Int. Conf. of Theory and Applications of Satisfiability Testing (SAT), Seattle, WA, USA, pp. 252–265.
    Google ScholarLocate open access versionFindings
  • Berre, D.L. and Parrain, A. (2010) The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7, 59–64.
    Google ScholarLocate open access versionFindings
  • Davies, J. and Bacchus, F. (2011) Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. Proc. of the 17th Int. Conf. of Principles and Practice of Constraint Programming (CP), Perugia, Italy, pp. 225–239.
    Google ScholarLocate open access versionFindings
  • Koshimura, M., Zhang, T., Fujita, H. and Hasegawa, R. (2012) Qmaxsat: a partial max-SAT solver. J. Satisf. Boolean Model. Comput, 8, 95–100.
    Google ScholarLocate open access versionFindings
  • Ansótegui, C., Bonet, M.L. and Levy, J. (2013) SAT-based MaxSAT algorithms. Artif. Intell., 196, 77–105.
    Google ScholarLocate open access versionFindings
  • Morgado, A., Heras, F., Liffiton, M.H., Planes, J. and Marques-Silva, J. (2013) Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints, 18, 478–534.
    Google ScholarLocate open access versionFindings
  • Martins, R., Joshi, S., Manquinho, V.M. and Lynce, I. (2014) Incremental Cardinality Constraints for Maxsat. Proc. of the 20th Int. Conf. of Principles and Practice of Constraint Programming (CP), Lyon, France, pp. 531–548.
    Google ScholarLocate open access versionFindings
  • Narodytska, N. and Bacchus, F. (2014) Maximum Satisfiability Using Core-Guided MaxSAT Resolution. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI), Québec City, Québec, Canada, pp. 2717–2723.
    Google ScholarLocate open access versionFindings
  • Ansótegui, C. and Gabàs, J. (2017) WPM3: an (in)complete algorithm for weighted partial maxsat. Artif. Intell., 250, 37–57.
    Google ScholarLocate open access versionFindings
  • Cha, B., Iwama, K., Kambayashi, Y. and Miyazaki, S. (1997) Local Search Algorithms for Partial MAXSAT. Proc. of the 14th National Conf. on Artificial Intelligence (AAAI), Providence, Rhode Island, pp. 263–268.
    Google ScholarLocate open access versionFindings
  • Luo, C., Cai, S., Wu, W., Jie, Z. and Su, K. (2015) CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. Comput., 64, 1830–1843.
    Google ScholarLocate open access versionFindings
  • Thornton, J. and Sattar, A. (1998) Dynamic Constraint Weighting for Over-Constrained Problems. Proc. of the 5th Pacific Rim Int. Conf. on Artificial Intelligence (PRICAI), Singapore, pp. 377–388.
    Google ScholarLocate open access versionFindings
  • Thornton, J., Bain, S., Sattar, A. and Pham, D.N. (2002) A Two Level Local Search for MAX-SAT Problems With Hard and Soft Constraints. Proc. of the 15th Australian Joint Conf. on Artificial Intelligence (AI), Canberra, Australia, pp. 603–614.
    Google ScholarLocate open access versionFindings
  • Cai, S., Luo, C., Thornton, J. and Su, K. (2014) Tailoring Local Search for Partial MaxSAT. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI), Québec City, Québec, Canada, pp. 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., Luo, C. and Zhang, H. (2017) From Decimation to Local Search and Back: A New Approach to Maxsat. Proc. of the Twenty-Sixth Int. Joint Conf. on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19–25, 2017, pp. 571–577.
    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
  • Chu, Y., Luo, C., Huang, W., You, H. and Fan, D. (2017) Hard Neighboring Variables Based Configuration Checking in Stochastic Local Search for Weighted Partial Maximum Satisfiability. 29th IEEE Int. Conf. on Tools With Artificial Intelligence, ICTAI 2017, Boston, MA, USA, November 6-8, 2017, pp. 139–146.
    Google ScholarFindings
  • Cai, S. (2015) Balance Between Complexity and Quality: Local Search for Minimum Vertex Cover in Massive Graphs. Proc. of the Twenty-Fourth Int. Joint Conf. on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pp. 747–753.
    Google ScholarLocate open access versionFindings
  • Thornton, J., Pham, D.N., Bain, S. and Ferreira, V. Jr. (2004) Additive Versus Multiplicative Clause Weighting for SAT. Proc. of the 19th National Conf. on Artificial Intelligence (AAAI), San Jose, California, USA, pp. 191–196. AAAI Press/The MIT Press.
    Google ScholarLocate open access versionFindings
  • Lei, Z. and Cai, S. (2018) Solving (Weighted) Partial Maxsat by Dynamic Local Search for SAT. Proc. of the Twenty-Seventh Int. Joint Conf. on Artificial Intelligence, IJCAI 2018, July 13–19, 2018, Stockholm, Sweden, pp. 1346–1352.
    Google ScholarLocate open access versionFindings
  • Martins, R., Manquinho, V.M. and Lynce, I. (2014) Open-WBO: A Modular MaxSAT Solver. Proc. of the 17th Int. Conf. of Theory and Applications of Satisfiability Testing, Vienna, Austria, pp. 438–445.
    Google ScholarLocate open access versionFindings
  • Davies, J. (2013). Solving MaxSAT by decoupling optimization and satisfaction. PhD Thesis, University of Toronto.
    Google ScholarFindings
Your rating :
0

 

Tags
Comments