SpringerLink
Log in

Stochastic local search for Partial Max-SAT: an experimental evaluation

  • Published:
Artificial Intelligence Review Aims and scope Submit manuscript

Abstract

Stochastic local search (SLS) methods are heuristic-based algorithms that have gained in popularity for their efficiency and robustness when solving very large and complex problems from various areas of artificial intelligence. This study aims to gain insights into SLS methods for solving the Partial Max-SAT (PMSAT) problem. The PMSAT is an NP-Hard problem, an optimization variant of the Propositional Boolean Satisfiability (SAT) problem, that has importance in theory and practice. Many real-world problems including timetabling, scheduling, planning, routing, and software debugging can be reduced to the PMSAT problem. Modern PMSAT solvers are able to solve practical instances with hundreds of thousands to millions of variables and clauses. However, performance of PMSAT solvers are still limited for solving some benchmark instances. In this paper, we present, investigate, and analyze state-of-the-art SLS methods for solving the PMSAT problem. An experimental evaluation is presented based on the MAX-SAT evaluations from 2014 to 2019. The results of this evaluation study show that the currently best performing SLS methods for the PMSAT problem fall into three categories: distinction-based, configuration checking-based, and dynamic local search methods. Very good performance was reported for the dynamic local search based method. The paper gives a detailed picture of the performance of SLS solvers for the PMSAT problem, aims to improve our understanding of their capabilities and limitations, and identifies future research directions.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Germany)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. HS-Greedy—Max-SAT 2016—http://www.maxsat.udl.cat/16/solvers/index.html.

  2. Dist1—Max-SAT 2015—http://www.maxsat.udl.cat/15/solvers/index.html.

  3. Dist2— Max-SAT 2015-—http://www.maxsat.udl.cat/15/solvers/index.html.

  4. Dist-r—Max-SAT 2016—http://www.maxsat.udl.cat/16/solvers/index.html.

  5. http://www.maxsat.udl.cat/16/solvers/11/hsgreedyDescription.pdf-201605200523.

  6. http://www.maxsat.udl.cat/15/solvers/readme_.

  7. http://www.maxsat.udl.cat/15/solvers/readme__.

  8. http://www.maxsat.udl.cat/16/solvers/7/descriptionforDist-r-201605131003.

  9. CCMPA—Max-SAT 2014—http://www.maxsat.udl.cat/14/results-incomplete/index.html.

  10. SC2016—Max-SAT 2016—http://www.maxsat.udl.cat/16/solvers/6/README.txt-201603260957.

  11. Ramp—Max-SAT 2016—Fan et al. http://www.maxsat.udl.cat/16/solvers/11/RampDescription.pdf-201604151325.

  12. https://maxsat-evaluations.github.io/2017/mse17-talk.pdf-https://maxsat-evaluations.github.io/2018/mse18-talk.pdf - https://maxsat-evaluations.github.io/2019/mse19-talk.pdf.

References

  • Abio I, Deters M, Nieuwenhuis R, Stuckey PJ (2011) Reducing chaos in SAT-like search: finding solutions close to a given one. In: Sakallah KA, Simon L (eds) theory and applications of satisfiability testing - SAT 2011. Lecture Notes in Computer Science. Springer, Berlin Heidelberg, pp 273–286

  • Abrame A, Habet D (2012) Inference rules in local search for max-SAT. In: 2012 IEEE 24th international conference on tools with artificial intelligence, vol 1, pp 207–214

  • Achlioptas D, Gomes C, Kautz H, Selman B (2000) Generating satisfiable problem instances. In: Proceedings of the seventeenth national conference on artificial intelligence (AAAI-00)

  • Alouneh S, Abed S, Al Shayeji MH, Mesleh R (2018) A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artif Intell Rev 52:2575–2601

    Google Scholar 

  • Ansotegui C, Bonet ML, Levy J (2013) SAT-based MaxSAT algorithms. Artif Intell 196:77–105

    MathSciNet  MATH  Google Scholar 

  • Ansotegui C, Didier F, Gabas J (2015) Exploiting the structure of unsatisfiable cores in MaxSAT. In: IJCAI

  • Ansotegui C, Bacchus F, Jarvisalo M, Martins R (2017) MaxSAT evaluation 2017: solver and benchmark descriptions. Department of Computer Science, University of Helsinki, B-2017-2:1–41

  • Ansotegui C, Heymann B, Pon J, Sellmann M, Tierney K (2019) Hyper-reactive tabu search for MaxSAT. In: Battiti,R, Brunato M, Kotsireas I, Pardalos PM (eds) Learning and intelligent optimization, Lecture Notes in Computer Science. Springer International Publishing, Cham, pp 309–325

  • Argelich J (NA) Random partial max-sat generator

  • Argelich J, Lynce I, Marques-Silva J (2009) On solving boolean multilevel optimization problems. In :Proceedings of the 21st international jont conference on artifical intelligence, IJCAI’09. Morgan Kaufmann Publishers Inc. event-place: Pasadena, California, USA, pp 393–398

  • Argelich J, Cabiscol A, Lynce I, Manya F (2010) New insights into encodings from MaxCSP into partial MaxSAT. In: 2010 40th IEEE international symposium on multiple-valued logic, pp 46–52

  • Bacchus F, Jarvisalo MJ, Martins R (2018) MaxSAT evaluation 2018: solver and benchmark descriptions. Department of Computer Science, University of Helsinki, B-2018-2:47

  • Balint A, Frohlich A (2010) Improving stochastic local search for SAT with a new probability distribution. In: Strichman O, Szeider S (eds) Theory and applications of satisfiability testing-SAT 2010, number 6175 in Lecture Notes in Computer Science. Springer, Berlin, pp 10–15

    Google Scholar 

  • Balint A, Schoning U (2012) Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti A, Sebastiani R (eds) Theory and applications of satisfiability testing-SAT 2012. Lecture Notes in Computer Science. Springer, Berlin, pp 16–29

  • Battiti R, Protasi M (1997) Reactive search, a history-sensitive heuristic for MAX-SAT. J Exp Algorithmics, p 2

  • Battiti R, Protasi M (1998) Approximate algorithms and heuristics for MAX-SAT. In: Du D-Z, Pardalos PM (eds) Handbook of combinatorial optimization. Springer, New York, pp 77–148

    Google Scholar 

  • Battiti R, Tecchiolli G (1994) The reactive tabu search. ORSA J Comput 6(2):126–140

    MATH  Google Scholar 

  • Bensana E, Lemaitre M, Verfaillie G (1999) Earth observation satellite management. Constraints 4(3):293–299

    MATH  Google Scholar 

  • Berg J, Jarvisalo M (2013) Optimal correlation clustering via MaxSAT. In: 2013 IEEE 13th international conference on data mining workshops, pp 750–757

  • Berg J, Jarvisalo M, (2014) SAT-based approaches to treewidth computation: an evaluation. In: 2014 IEEE 26th international conference on tools with artificial intelligence, pp 328–335

  • Berg J, Jarvisalo M, Malone B (2014) Learning optimal bounded treewidth bayesian networks via maximum satisfiability. In: Kaski, S, Corander J (eds) Proceedings of the seventeenth international conference on artificial intelligence and statistics, volume 33 of proceedings of machine learning research. PMLR. Citation Key: inproceedings, pp 86–95

  • Bian Z, Chudak F, Macready W, Roy A, Sebastiani R, Varotti S (2018) Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report. In: Dixon C, Finger M (eds) Frontiers of combining systems, Lecture Notes in Computer Science. Springer, Cham, pp 153–171

  • Biere A (2014) Yet another local search solver and lingeling and friends entering the SAT competition 2014. In: Proceedings of SAT competition 2014: solver and benchmark descriptions, B-2014-2:39–40

  • Bouhmala N (2019) Combining simulated annealing with local search heuristic for MAX-SAT. J Heuristics 25(1):47–69

    Google Scholar 

  • Cai S (2015) Balance between complexity and quality: local search for minimum vertex cover in massive graphs. In: JCAI’15 Proceedings of the 24th international conference on artificial intelligence. AAAI Press, pp 747–753

  • Cai S, Su K (2011) Local search with configuration checking for SAT. In: 2011 IEEE 23rd international conference on tools with artificial intelligence, pp 59–66

  • Cai S, Su K (2012) Configuration checking with aspiration in local search for SAT. In: Twenty-sixth AAAI conference on artificial intelligence

  • Cai S, Su K (2013a) Comprehensive score: Towards efficient local search for SAT with long clauses. In: Proceedings of the twenty-third international joint conference on artificial intelligence, IJCAI ’13. AAAI Press, pp 489–495

  • Cai S, Su K (2013b) Local search for boolean satisfiability with configuration checking and subscore. Artif Intell 204:75–98

    MATH  Google Scholar 

  • Cai S, Su K, Sattar A (2011a) Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif Intell 175(9):1672–1696

    MathSciNet  MATH  Google Scholar 

  • Cai S, Su K, Sattar A (2011b) A new local search strategy for SAT

  • Cai S, Luo C, Thornton J, Su K (2014) Tailoring local search for partial MaxSAT. In: Proceedings of the twenty-eighth AAAI conference on artificial intelligence, AAAI\(\acute{1}\)4. AAAI Press, pp 2623–2629

  • Cai S, Luo C, Su K (2015) CCAnr: a configuration checking based local search solver for non-random satisfiability. In: Heule, M, Weaver, S (eds), Theory and applications of satisfiability testing–SAT 2015, volume 9340 in Lecture Notes in Computer Science. Springer, pp 1–8

  • Cai S, Luo C, Lin J, Su K (2016) New local search methods for partial MaxSAT. Artif Intell 240:1–18

    MathSciNet  MATH  Google Scholar 

  • Cai S, Luo C, Zhang H (2017) From decimation to local search and back: a new approach to MaxSAT. In: Proceedings of the twenty-sixth international joint conference on artificial intelligence, IJCAI-17, pp 571–577

  • Cha B, Iwama K, Kambayashi Y, Miyazaki S (1997) Local search algorithms for partial MAXSAT. In: AAAI/IAAI, pp 263–268

  • Chen Y, Safarpour S, Veneris A, Marques-Silva J (2009) Spatial and temporal design debug using partial MaxSAT. In: Proceedings of the 19th ACM Great Lakes symposium on VLSI, GLSVLSI \(\acute{0}\)9. ACM, pp 345–350

  • Chen Y, Safarpour S, Marques-Silva J, Veneris A (2010) Automated design debugging with maximum satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 29(11):1804–1817

    Google Scholar 

  • Chu Y, Luo C, Huang W, You H, Fan D (2017) Hard neighboring variables based configuration checking in stochastic local search for weighted partial maximum satisfiability. In: 2017 IEEE 29th international conference on tools with artificial intelligence (ICTAI). IEEE, pp 139–146

  • Coja-Oghlan A (2011) On belief propagation guided decimation for random k-SAT. In: Proceedings of the twenty-second annual ACM-SIAM symposium on discrete algorithms, pp 957–966

  • Cook SA (1971) The complexity of theorem-proving procedures. In: Proceedings of the third annual ACM symposium on theory of computing, STOC \(\acute{7}\)1. ACM, pp 151–158

  • Cormen TH, Leiserson CE, Rivest RL, Stein C (2001) Greedy algorithms. In: Introduction To algorithms. MIT Press, 3rd edition, Cambridge

  • Dang NTT, De Causmaecker P (2016) Characterization of neighborhood behaviours in a multi-neighborhood local search algorithm. Artif Intell, p 13

  • Demirovic E, Musliu N (2014) Modeling high school timetabling as partial weighted maxSAT. In: LaSh 2014: the 4th workshop on logic and search (a SAT/ICLP workshop at FLoC) (2014)

  • Demirovic E, Stuckey P (2018) Local-style search in the linear maxsat algorithm: a computational study of solution-based phase saving. In: Pragmatics of SAT workshop

  • Demirovic E, Musliu N, Winter F (2017) Modeling and solving staff scheduling with partial weighted maxSAT. Ann Oper Res

  • Desrosiers J, Jaumard B, Stan M (1993) Tabu search and a quadratic relaxation for the satisfiability problem

  • Festa P, Pardalos PM, Pitsoulis LS, Resende MGC (2005) GRASP with path-relinking for the weighted maximum satisfiability problem. In: Nikoletseas SE (ed) experimental and efficient algorithms, lecture notes in computer science. Berlin, Heidelberg, pp 367–379

  • Frank H (2009) Automated configuration of algorithms for solving hard computational problems

  • Frohlich A, Biere A, Wintersteiger C, Hamadi Y (2015) Stochastic local search for satisfiability modulo theories. In: Proceedings of the twenty-ninth AAAI conference on artificial intelligence, AAAI’15. AAAI Press, pp 1136–1143

  • Fu Z, Malik S (2006) On solving the partial MAX-SAT problem. In: Biere A, Gomes CP (eds) Theory and applications of satisfiability testing—SAT 2006, number 4121 in Lecture Notes in Computer Science. Springer, Berlin, pp 252–265

    Google Scholar 

  • Gableske O, Heule MJH (2011) EagleUP: solving random 3-SAT using SLS with unit propagation. In: Sakallah KA, Simon L (eds) Theory and applications of satisfiability testing—SAT 2011. Lecture Notes in Computer Science. Springer, Berlin, pp 367–368

  • Gamarnik D, Sudan M (2014) Performance of the survey propagation-guided decimation algorithm for the random NAE-k-SAT problem. ar**v:1402.0052

  • Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman & Co, Norton

    MATH  Google Scholar 

  • Gent IP, Walsh T (1993) Towards an understanding of hill-climbing procedures for SAT. In: Proceedings of the eleventh national conference on artificial intelligence, AAAI\(\acute{9}\)3. AAAI Press, pp 28–33

  • Graca A, Lynce I, Marques-Silva J, Oliveira AL (2012) Efficient and accurate haplotype inference by combining parsimony and pedigree information. In: Horimoto K, Nakatsui M, Popov N (eds) Algebraic and numeric biology. Lecture Notes in Computer Science. Springer, Berlin, pp 38–56

  • Grastien A, Anbulagan A (2013) Diagnosis of discrete event systems using satisfiability algorithms: a theoretical and empirical study. IEEE Trans Autom Control 58(12):3070–3083

    MathSciNet  MATH  Google Scholar 

  • GroBmann P, Holldobler S, Manthey N, Nachtigall K, Opitz J, Steinke P (2012) Solving periodic event scheduling problems with SAT. In: Jiang H, Ding W, Ali M, Wu X (eds) Advanced Research in applied artificial intelligence. Lecture Notes in Computer Science. Springer, Heidelberg, pp 166–175

  • Gu J (1992) Efficient local search for very large-scale satisfiability problems. SIGART Bull 3(1):8–12

    Google Scholar 

  • Hansen P, Jaumard B (1990) Algorithms for the maximum satisfiability problem. Computing 44(4):279–303

    MathSciNet  MATH  Google Scholar 

  • Hansen P, Mladenovic N (2014) Variable neighborhood search. In: Burke EK, Kendall G (eds) Search methodologies. Springer, New York, pp 313–337

    Google Scholar 

  • He D, Choi A, Pipatsrisawat K, Darwiche A, Eskin E (2010) Optimal algorithms for haplotype assembly from whole-genome sequence data. Bioinformatics 26(12):i183–i190

    Google Scholar 

  • Heras F, Larrosa J, de Givry S, Schiex T (2008) 2006 and 2007 max-SAT evaluations: contributed instances. J Satisf Boolean Model Comput 4:239–250

    MATH  Google Scholar 

  • Hoos HH (2012) Automated algorithm configuration and parameter tuning. In: Hamadi Y, Monfroy E, Saubion F (eds) Autonomous search. Springer, Berlin, pp 37–71

    Google Scholar 

  • Hoos HH, Stutzle T (2000) Local search algorithms for SAT: an empirical evaluation. J Auton Reason 24(4):421–481

    MATH  Google Scholar 

  • Hoos HH, Stutzle T (2015) Stochastic local search algorithms: an overview. In: Kacprzyk J, Pedrycz W (eds) Springer Handbook of Computational Intelligence. Springer, Berlin, pp 1085–1105

    Google Scholar 

  • Horbach A, Bartsch T, Briskorn D (2012) Using a SAT-solver to schedule sports leagues. J Sched 15(1):117–125

    Google Scholar 

  • Hsiao P-C, Chiang T-C, Fu L-C (2012) A VNS-based hyper-heuristic with adaptive computational budget of local search. In: 2012 IEEE congress on evolutionary computation, pp 1–8

  • Hutter F, Tompkins DAD, Hoos HH (2002) Scaling and probabilistic smoothing: efficient dynamic local search for SAT. In: Hentenryck PV (ed) Principles and practice of constraint programming—CP 2002, number 2470 in Lecture Notes in Computer Science. Springer, Berlin, pp 233–248

    Google Scholar 

  • Hutter F, Hoos HH, Leyton-Brown K, Stutzle T (2009) ParamILS: an automatic algorithm configuration framework. J Artif Int Res 36(1):267–306

    MATH  Google Scholar 

  • Hutter F, Hoos HH, Leyton-Brown K (2011) Sequential model-based optimization for general algorithm configuration. In: Coello CAC (ed) Learning and intelligent optimization. Lecture Notes in Computer Science. Springer, Berlin, pp 507–523

  • Hyttinen A, Eberhardt F, Jarvisalo M (2014) Constraint-based causal discovery: conflict resolution with answer set programming. In: UAI

  • Ignatiev A, Janota M, Marques-Silva J (2014) Towards efficient optimization in package management systems. In: Proceedings of the 36th international conference on software engineering, ICSE 2014. ACM Event-place: Hyderabad, India, pp 745–755

  • Ignatiev A, Morgado A, Marques-Silva J (2019) RC2: an efficient MaxSAT Solver. J Satisf Boolean Model Comput 11(1):53–64

    MathSciNet  Google Scholar 

  • Juma F, Hsu EI, McIlraith SA (2012) Preference-based planning via MaxSAT. In: Kosseim L, Inkpen D (eds) Advances in artificial intelligence. Lecture Notes in Computer Science. Springer, Berlin, pp 109–120

  • Kautz HA, Sabharwal A, Selman B (2009) Incomplete algorithms. In: Handbook of satisfiability, volume 185 of frontiers in artificial intelligence and applications. IOS Press, pp 185–203

  • Kernighan BW, Lin S (1970) An efficient heuristic procedure for partitioning graphs. Bell Syst Tech J 49(2):291–307

    MATH  Google Scholar 

  • Kilani Y, Bsoul M, Alsarhan A, Obeidat I (2012) Improving PAWS by the island confinement method. In: Rutkowski L, Korytkowski M, Scherer R, Tadeusiewicz R, Zadeh LA, Zurada JM (eds) Artificial intelligence and soft computing. Lecture Notes in Computer Science. Springer, Berlin Heidelberg, pp 662–670

  • Kirkpatrick S, Gelatt CD, Vecchi MP (1983) Optimization by simulated annealing. Science 220(4598):671–680

    MathSciNet  MATH  Google Scholar 

  • Koshimura M, Zhang T, Fujita H, Hasegawa R (2012) QMaxSAT: a partial max-SAT solver. J Satisf Boolean Model Comput 8:95–100

    MathSciNet  MATH  Google Scholar 

  • Kuegel A (2012) Improved exact solver for the weighted MAX-SAT problem. In Berre DL (ed) POS-10. Pragmatics of SAT, volume 8 of EPiC series in computing. EasyChair, pp 15–27

  • Laurent B, Hao J-K (2007) A study of neighborhood structures for the multiple depot vehicle scheduling problem. In: Stutzle T, Birattari M, Hoos H (eds) Engineering stochastic local search algorithms. designing, implementing and analyzing effective heuristics, Lecture Notes in Computer Science. Springer: Berlin, pp 197–201

  • Lei Z, Cai, S (2018) Solving (weighted) partial MaxSAT by dynamic local search for SAT. In: Proceedings of the twenty-seventh international joint conference on artificial intelligence, IJCAI-18. International joint conferences on artificial intelligence organization, pp 1346–1352

  • Leyton-Brown K, Pearson M, Shoham Y (2000) Towards a universal test suite for combinatorial auction algorithms. In: Proceedings of the 2Nd ACM conference on electronic commerce, EC ’00. ACM, pp 66–76

  • Li CM, Manya F, Mohamedou N, Planes J (2009) Exploiting cycle structures in max-SAT. In: Kullmann O (ed) Theory and applications of satisfiability testing—SAT 2009. Lecture Notes in Computer Science. Springer, Berlin, pp 467–480

  • Li CM, Manya F, Quan Z, Zhu Z (2010) Exact MinSAT solving. In: Strichman O, Szeider S (eds) Theory and applications of satisfiability testing—SAT 2010. Lecture Notes in Computer Science. Springer, Berlin, pp 363–368

  • Liao X, Zhang H, Koshimura M, Fujita H, Hasegawa R (2013) Using MaxSAT to correct errors in AES key schedule images. In: 2013 IEEE 25th international conference on tools with artificial intelligence, pp 284–291

  • Lopez-Ibanez M, Dubois-Lacoste J, Perez Caceres L, Birattari M, Stutzle T (2016) The irace package: iterated racing for automatic algorithm configuration. Oper Res Perspect 3:43–58

    MathSciNet  Google Scholar 

  • Luo C, Su K, Cai S (2012) Improving local search for random 3-SAT using quantitative configuration checking. ECAI 2012. Front Artif Intell Appl 242:570–575

    MATH  Google Scholar 

  • Luo C, Cai S, Wu W, Su K (2014) Double configuration checking in stochastic local search for satisfiability. In: Twenty-eighth AAAI conference on artificial intelligence

  • Luo C, Cai S, Su K, Wu W (2015a) Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybern 45(5):1028–1041

    Google Scholar 

  • Luo C, Cai S, Wu W, Jie Z, Su K (2015b) CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans Comput 64(7):1830–1843

    MathSciNet  MATH  Google Scholar 

  • Mangal R, Zhang X, Kamath A, Nori AV, Naik M (2016) Scaling relational inference using proofs and refutations. In: AAAI. Citation Key: Mangal2016ScalingRI

  • Luo C, Cai S, Su K, Huang W (2017) CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artif Intell 243:26–44

    MathSciNet  MATH  Google Scholar 

  • Manquinho V, Marques-Silva J, Planes J (2009) Algorithms for weighted boolean optimization. In: Kullmann O (ed) Theory and applications of satisfiability testing—SAT 2009. Lecture Notes in Computer Science. Springer, Berlin, pp 495–508

  • Marques-Silva J, Heras F, Janota M, Previti A, Belov A (2013) On computing minimal correction subsets. In: JCAI

  • Marti R, Pardalos PM, Resende MGC (2018) Local search. In: Handbook of heuristics. Springer

  • Martins R, Manquinho V, Lynce I (2014) Open-WBO: a modular MaxSAT solver. In: Sinz C, Egly U (eds) Theory and applications of satisfiability testing – SAT 2014, Lecture Notes in Computer Science. Springer, Cham, pp 438–445

  • MaxSAT (2017) Evaluation results. http://mse17.cs.helsinki.fi/rankings.html

  • MaxSAT (2018) Evaluation—history. https://maxsat-evaluations.github.io/2018/history.html

  • MaxSAT (2018) Evaluation benchmarks. https://maxsat-evaluations.github.io/2018/benchmarks.html

  • MaxSAT (2019) Evaluation benchmarks. https://maxsat-evaluations.github.io/2019/benchmarks.html

  • Mazure B, Sais L, Gregoire e (1997) Tabu search for SAT. In: Proceedings of the fourteenth national conference on artificial intelligence and ninth conference on innovative applications of artificial intelligence, AAAI\(\acute{9}\)7/IAAI\(\acute{9}\)7. AAAI Press, pp 281–285

  • McAllester D, Selman B, Kautz H (1997) Evidence for invariants in local search. In: Proceedings of the fourteenth national conference on artificial intelligence and ninth conference on innovative applications of artificial intelligence, AAAI\(\acute{9}\)7/IAAI\(\acute{9}\)7. AAAI Press, pp 321–326

  • Menai MEB, Al-Yahya TN (2013) A taxonomy of exact methods for partial max-SAT. J Comput Sci Technol 28(2):232–246

    MathSciNet  MATH  Google Scholar 

  • Metodi A, Stern R, Kalech M, Codish M (2014) A novel SAT-based approach to model based diagnosis. J Artif Int Res 51(1):377–411

    MathSciNet  MATH  Google Scholar 

  • Mills P, Tsang E (2000) Guided local search for solving SAT and weighted MAX-SAT problems. J Autom Reason 24(1):205–223

    MathSciNet  MATH  Google Scholar 

  • Miyazaki S, Iwama K, Kambayashi Y (1996) Database queries as combinatorial optimization problems. In: International symposium on cooperative database systems for advanced applications, pp 448–454

  • Morgado A, Heras F, Liffiton M, Planes J, Marques-Silva J (2013) Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4):478–534

    MathSciNet  MATH  Google Scholar 

  • Naji-Azimi Z, Toth P, Galli L (2010) An electromagnetism metaheuristic for the unicost set covering problem. Eur J Oper Res 205(2):290–300

    MathSciNet  MATH  Google Scholar 

  • Park JD (2002) Using weighted MAX-SAT engines to solve MPE. In: Eighteenth national conference on artificial intelligence. American Association for Artificial Intelligence, pp 682–687

  • Paturi R, Pudlak P, Saks ME, Zane F (2005) An improved exponential-time algorithm for k-SAT. J ACM 52(3):337–364

    MathSciNet  MATH  Google Scholar 

  • Pham DN, Thornton J, Gretton C, Sattar A (2008) Combining adaptive and dynamic local search for satisfiability. J Satisfi Boolean Model Comput 4:149–172

    MATH  Google Scholar 

  • Pipatsrisawat T, Akop P, Chavira M, Choi A, Darwiche A (2008) Solving weighted MaxSAT problems in a reduced search space: a performance analysis. JSAT 4:191–217

    MATH  Google Scholar 

  • Resende MGC, Pitsoulis LS, Pardalos PM (1997) Approximate solution of weighted MAX-SAT problems Using GRASP

  • Riefert A, Sauer M, Reddy S, Becker B (2015) Improving diagnosis resolution of a fault detection test set. In: 2015 IEEE 33rd VLSI test symposium (VTS), pp 1–6

  • Sauer M, Reimer S, Polian I, Schubert T, Becker B (2013) Provably optimal test cube generation using quantified boolean formula solving. In: 2013 18th Asia and South Pacific design automation conference (ASP-DAC), pp 533–539

  • Selman B, Kautz H (1993a) Domain-independent extensions to GSAT: solving large structured satisfiability problems. In: Proceedings of the 13th international joint conference on artifical intelligence—Volume 1, IJCAI’93. Morgan Kaufmann Publishers Inc, Chambery, France, pp 290–295

  • Selman B, Kautz HA (1993b) An empirical study of greedy local search for satisfiability testing

  • Selman B, Levesque H, Mitchell D (1992) A new method for solving hard satisfiability problems. In: Proceedings of the tenth national conference on artificial intelligence, AAAI\(\acute{9}\)2,. AAAI Press, pp 440–446

  • Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: Proceedings of the twelfth national conference on artificial intelligence (Vol. 1), AAAI \(\acute{9}\)4. American Association for Artificial Intelligence, pp 337–343

  • Selman B, Kautz H, Cohen B (1995) Local search strategies for satisfiability testing. Dimacs Series in discrete mathematics and theoretical computer science, pp 521–532

  • Selman B, Mitchell DG, Levesque HJ (1996) Generating hard satisfiability problems. Artif Intell 81(1):17–29

    MathSciNet  Google Scholar 

  • Sevaux M, Sorensen K, Pillay N (2018) Adaptive and multilevel metaheuristics. In: Marti R, Panos P, Resende MGC (eds) Handbook of heuristics. Springer, pp 1–19

  • Shen H, Zhang H (2004) Study of lower bound functions for MAX-2-SAT. In: Proceedings of the 19th national conference on artifical intelligence, AAAI’04. AAAI Press, pp 185–190

  • Spears WM (1993) Simulated annealing for hard satisfiability problems. In: Workshop. American Mathematical Society, pp 533–558

  • Steinmann O, Strohmaier A, Stutzle T (1997) Tabu search vs. random walk

  • Stojadinovic M (2014) Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems. In: Sullivan B (eds) Principles and practice of constraint programming, volume 8656. Springer, pp 886–902

  • Strickland DM, Barnes E, Sokol JS (2005) Optimal protein structure alignment using maximum cliques. Oper Res 53(3):389–402

    MathSciNet  MATH  Google Scholar 

  • Stutzle T, Hoos H, Roli A (2001) A review of the literature on local search algorithms for MAX-SAT

  • Taillard E (1993) Benchmarks for basic scheduling problems. Eur J Oper Res 64(2):278–285

    MathSciNet  MATH  Google Scholar 

  • Thornton J, Pham DN, Bain S, Ferreira V (2004) Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 19th national conference on artifical intelligence, AAAI\(\acute{0}\)4. AAAI Press, pp 191–196

  • Tompkins DAD, Hoos HH (2003) Scaling and probabilistic smoothing: dynamic local search for unweighted MAX-SAT. In: ** strategies in discrete lagrangian methods for solving hard satisfiability and maximum satisfiability problems. In: Proceedings of the sixteenth national conference on artificial intelligence and the eleventh innovative applications of artificial intelligence conference innovative applications of artificial intelligence, AAAI \(\acute{9}\)9/IAAI \(\acute{9}\)9. American Association for Artificial Intelligence, pp 673–678

  • Wu Z, Wah BW (2000) An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems. In: Proceedings of the seventeenth national conference on artificial intelligence and twelfth conference on innovative applications of artificial intelligence. AAAI Press, pp 310–315

  • Wu Q, Hao J-K, Glover F (2012) Multi-neighborhood tabu search for the maximum weight clique problem. Ann Oper Res 196(1):611–634

    MathSciNet  MATH  Google Scholar 

  • **aojuan L, Koshimura M, Fujita H, Hasegawa R (2012) Solving the coalition structure generation problem with MaxSAT. In: 2012 IEEE 24th international conference on tools with artificial intelligence. IEEE, pp 910–915

  • Xu H, Rutenbar RA, Sakallah K (2003) sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing. IEEE Trans Comput Aided Des Integr Circuits Syst 22(6):814–820

    Google Scholar 

  • Xu K, Boussemart F, Hemery F, Lecoutre C (2005) A simple model to generate hard satisfiable instances. In: Proceedings of the 19th international joint conference on artificial intelligence, IJCAI’05. Morgan Kaufmann Publishers Inc. Event-place: Edinburgh, Scotland, pp 337–342

  • Xu Z, He K, Li C-M (2019) An iterative path-breaking approach with mutation and restart strategies for the MAX-SAT problem. Comput Oper Res 104:49–58

    MathSciNet  MATH  Google Scholar 

  • Yagiura M, Ibaraki T (2001) Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: experimental evaluation. J Heuristics 7(5):423–442

    MATH  Google Scholar 

  • Zhang W, Rangan A, Looks M (2003) Backbone guided local search for maximum satisfiability. In: Proceedings of the 18th international joint conference on artificial intelligence, IJCAI\(\acute{0}\)3. Morgan Kaufmann Publishers Inc, pp 1179–1184

  • Zhang X, Mangal R, Grigore R, Naik M, Yang H (2014) On abstraction refinement for program analyses in datalog. In: Proceedings of the 35th ACM SIGPLAN conference on programming language design and implementation, PLDI ’14. ACM, pp 239–248

Download references

Acknowledgements

The authors would like to thank the Deanship of Scientific Research for funding and supporting this research through the initiative of DSR Graduate Student Research Support (GSR), King Saud University.

Author information

Authors and Affiliations

  1. Department of Computer Science, College of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia

    Haifa Hamad AlKasem & Mohamed El Bachir Menai

Authors
  1. Haifa Hamad AlKasem
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamed El Bachir Menai
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Haifa Hamad AlKasem or Mohamed El Bachir Menai.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

AlKasem, H.H., Menai, M.E.B. Stochastic local search for Partial Max-SAT: an experimental evaluation. Artif Intell Rev 54, 2525–2566 (2021). https://doi.org/10.1007/s10462-020-09908-4

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10462-020-09908-4

Keywords

Search

Navigation