[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Using the method of conditional expectations to supply an improved starting point for CCLS

  • Published:
Journal of Combinatorial Optimization Aims and scope Submit manuscript

Abstract

This paper proposes to combine the method of conditional expectations (MOCE, also known as Johnson’s Algorithm) with the state-of-the-art heuristic configuration checking local search (CCLS), to solve maximum satisfiability (Max Sat) instances. First, MOCE is used to find an outstanding assignment, and then CCLS explores the solution space, starting at this assignment. This combined heuristic, which we call MOCE–CCLS, is shown to provide a significant improvement over each of its parts: MOCE and CCLS. An additional contribution of this paper is the results of a comprehensive comparative evaluation of MOCE–CCLS versus CCLS on various benchmarks. On random benchmarks, the combined heuristic reduces the number of unsatisfied clauses by up to tens of percents. On Max Sat 2016 and 2021 public competition benchmarks, which include crafted and industrial instances also, MOCE–CCLS outperforms CCLS as well. To provide an empirical basis to the above result, this work further explores the correlation between the quality of initial assignments provided to CCLS and that of the corresponding final assignments. Empirical results show that the correlation is significant and long-lasting. Thus, under practical time constraints, the quality of the initial assignment is crucial to the performance of local search heuristics.

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
£29.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 (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

References

  • Abramé A, Habet D, Toumi D (2017) Improving configuration checking for satisfiable random k-SAT instances. Ann Math Artif Intell 79(1):5–24

    Article  MathSciNet  MATH  Google Scholar 

  • Achlioptas D (2009) Random satisfiability. Handb Satisf 185:245

    Google Scholar 

  • Achlioptas D, Peres Y (2004) The threshold for random k-SAT is \(2^{k} \text{ log } 2 - O(k)\). J Am Math Soc 17(4):947–973

    Article  MATH  Google Scholar 

  • Angel E, Zissimopoulos V (2000) On the classification of NP-complete problems in terms of their correlation coefficient. Discrete Appl Math 99(1):261–277

    Article  MathSciNet  MATH  Google Scholar 

  • Angel E, Zissimopoulos V (2001) On the landscape ruggedness of the quadratic assignment problem. Theoret Comput Sci 263(1):159–172

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  • Ansótegui C, Bonet ML, Levy J (2009) Solving (weighted) partial MaxSAT through satisfiability testing. In: International conference on theory and applications of satisfiability testing. Springer, pp 427–440

  • Ansótegui, C, Bonet ML, Gabas J, Levy J (2012) Improving SAT-based weighted MaxSAT solvers. In: International conference on principles and practice of constraint programming. Springer, pp 86– 101

  • Argelich J, Li CM, Manyà F, Planes J (2020) MaxSat evaluations. https://maxsat-evaluations.github.io/

  • Ausiello G, Crescenzi P, Gambosi G, Kann V, M-Spaccamela A, Protasi M (2003) Complexity and approximation: combinatorial optimization problems and their approximability properties, 2nd edn. Springer, New York

    MATH  Google Scholar 

  • Avellaneda F (2020) A short description of the solver EvalMaxSAT. MaxSAT Eval 2020:8

    Google Scholar 

  • Berend D, Twitto Y (2020) Effect of initial assignment on local search performance for Max Sat. In: Proceedings of the 18th international symposium on experimental algorithms (SEA 2020), vol 160. Leibniz international proceedings in informatics (LIPIcs), pp 8:1– 8:14

  • Berend D, Twitto Y (2016) The normalized autocorrelation length of random Max r-Sat converges in probability to (1 \(-\) 1/2\(^{r})\)/r”. In: The 19th international conference on theory and applications of satisfiability testing (SAT 2016). Springer, pp 60–76

  • Berg J, Korhonen T, Järvisalo M (2017) Loandra: PMRES extended with preprocessing entering MaxSAT evaluation 2017. MaxSAT Eval 2017:13

    Google Scholar 

  • Biere A, Heule M, van Maaren H (2009) Handbook of satisfiability, vol 185. IOS Press, Amsterdam

    MATH  Google Scholar 

  • de Boer P-T, Kroese DP, Mannor S, Rubinstein RY (2005) A tutorial on the cross-entropy method. Ann Oper Res 134(1):19–67

    Article  MathSciNet  MATH  Google Scholar 

  • Bouhmala N (2019) A Kernighan-Lin inspired algorithm for MAX-SAT. Sci China Inf Sci 62(11):1–3

    Article  Google Scholar 

  • Cai S, Jie Z, Su K (2015) An effective variable selection heuristic in SLS for weighted Max-2-SAT. J Heuristics 21(3):433–456

    Article  Google Scholar 

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

    Article  MATH  Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

  • Cai S, Luo C, Thornton J, Su K (2014) Tailoring local search for Partial MaxSAT. In: Proceedings of the 28th AAAI conference on artificial intelligence. AAAI’14. AAAI Press, Québec City, Québec, pp 2623–2629

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

  • Chen J, Kanj IA (2004) Improved exact algorithms for Max-Sat. Discrete Appl Math 142(1–3):17–27

    Article  MathSciNet  MATH  Google Scholar 

  • Chen R, Santhanam R (2015) Improved algorithms for sparse MAXSAT and MAX-k-CSP. In: Proceedings of the 18th international conference on theory and applications of satisfiability testing (SAT 2015). Springer, pp 33–45

  • Chicano F, Luque G, Alba E (2012) Autocorrelation measures for the quadratic assignment problem. Appl Math Lett 25(4):698–705

    Article  MathSciNet  MATH  Google Scholar 

  • Chicano F, Luque G, Alba E (2013) Problem understanding through landscape theory. In: Proceedings of the 15th annual conference companion on genetic and evolutionary computation. ACM, pp 1055– 1062

  • Chvátal V, Reed B (1992) Mick gets some (the odds are on his side) (satisfiability). In: Proceedings of the 33rd annual symposium on foundations of computer science. IEEE, pp 620–627

  • Coja-Oghlan A (2014) The asymptotic k-SAT threshold. In: Proceedings of the 46th annual ACM symposium on theory of computing. ACM, pp 804–813

  • Coppersmith D, Gamarnik D, Hajiaghayi M, Sorkin GB (2004) Random MAX SAT, random MAX CUT, and their phase transitions. Random Struct Algorithms 24(4):502–545

    Article  MathSciNet  MATH  Google Scholar 

  • Costello KP, Shapira A, Tetali P (2011) Randomized greedy: new variants of some classic approximation algorithms. In: Proceedings of the 22nd annual ACM-SIAM symposium on Discrete Algorithms. Society for Industrial and Applied Mathematics, pp 647–655

  • Crawford JM, Auton LD (1996) Experimental results on the crossover point in random 3-SAT. Artif Intell 81(1–2):31–57

    Article  MathSciNet  Google Scholar 

  • Davies J (2013) Solving MaxSAT by decoupling optimization and satisfaction. PhD thesis. University of Toronto

  • Davies J, Bacchus F (2011) Solving MAXSAT by solving a sequence of simpler SAT instances. In: Proceedings of the 17th international conference on principles and practice of constraint programming. Springer, pp 225–239

  • Den Besten M, Stützle T, Dorigo M (2001) Design of iterated local search algorithms. In: Workshops on applications of evolutionary computation. Springer, pp 441–451

  • Ding J, Sly A, Sun N (2015) Proof of the satisfiability conjecture for large k. In Proceedings of the 47th annual ACM symposium on theory of computing (STOC’15), pp 59–68

  • Dong X, Chen P, Huang H, Nowak M (2013) A multi-restart iterated local search algorithm for the Permutation Flow Shop problem minimizing total flow time. Comput Oper Res 40(2):627–632

    Article  MATH  Google Scholar 

  • Erdös P, Selfridge JL (1973) On a combinatorial game. J Comb Theory Ser A 14(3):298–301

    Article  MATH  Google Scholar 

  • Fontana W, Stadler PF, Bornberg-Bauer EG, Griesmacher T, Hofacker IL, Tacker M, Tarazona P, Weinberger ED, Schuster P (1993) RNA folding and combinatory landscapes. Phys Rev E 47(3):2083–2099

    Article  Google Scholar 

  • Franco J, Paull M (1983) Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Appl Math 5(1):77–87

    Article  MathSciNet  MATH  Google Scholar 

  • Friedgut E, Bourgain J (1999) Sharp thresholds of graph properties, and the k-SAT problem. J Am Math Soc 12(4):1017–1054

    Article  MathSciNet  MATH  Google Scholar 

  • Goldberg DE (1988) Genetic algorithms and Walsh functions: a gentle introduction. Department of Mechanical Engineering, University of Alabama, Clearinghouse for Genetic Algorithms

  • Guerreiro AP, Terra-Neves M, Lynce I, Figueira JR, Manquinho V (2019) Constraint-based techniques in stochastic local search MaxSAT solving. In: International conference on principles and practice of constraint programming. Springer, pp 232–250

  • Gutin G, Punnen AP (2006) The traveling salesman problem and its variations. Springer, New York

    MATH  Google Scholar 

  • Gutin G, Yeo A (2002) Polynomial approximation algorithms for the TSP and the QAP with a factorial domination number. Discrete Appl Math 119(1–2):107–116

    Article  MathSciNet  MATH  Google Scholar 

  • Hains D, Whitley D, Howe A, Chen W (2013) Hyperplane initialized local search for MAXSAT. In Proceedings of the 15th annual conference on genetic and evolutionary computation, pp 805–812

  • Halderman JA, Schoen SD, Heninger N, Clarkson W, Paul W, Calandrino JA, Feldman AJ, Appelbaum J, Felten EW (2009) Lest we remember: cold-boot attacks on encryption keys. Commun ACM 52(5):91–98

    Article  Google Scholar 

  • Håstad J (2001) Some optimal inapproximability results. J ACM (JACM) 48(4):798–859

    Article  MathSciNet  MATH  Google Scholar 

  • Heckendorn RB, Rana S, Whitley D (1999) Polynomial time summary statistics for a generalization of MAXSAT. In: Proceedings of the 11th annual conference on genetic and evolutionary computation. Morgan Kaufmann, pp 281–288

  • Heninger NA (2011) Error correction and the cryptographic key. PhD thesis. Princeton University

  • Heras F, Larrosa J, Oliveras A (2008) MiniMaxSAT: an efficient weighted Max-SAT solver. J Artif Intell Res (JAIR) 31:1–32

    Article  MathSciNet  MATH  Google Scholar 

  • Hoos HH, Smyth K, Stützle T (2004) Search space features underlying the performance of stochastic local search algorithms for MAXSAT. In: Proceedings of the 8th international conference on parallel problem solving from nature (PPSN VIII). Springer, pp 51–60

  • Hoos HH, Stützle T (2004) Stochastic local search: foundations and applications. Elsevier, New York

    MATH  Google Scholar 

  • Kamal AA (2012) Cryptanalysis and secure implementation of modern cryptographic algorithms. PhD thesis. Concordia University

  • Kamal AA, Youssef AM (2010) Applications of SAT solvers to AES key recovery from decayed key schedule images. In: Proceedings of the 4th international conference on emerging security information, systems and technologies. IEEE, pp 216–220

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

    MathSciNet  MATH  Google Scholar 

  • Le Berre D, Parrain A (2010) The Sat4j library, release 2.2. J Satisf Boolean Model Comput 7(2–3):59–64

    Google Scholar 

  • Li CM, Manyà F (2009) MaxSAT, hard and soft constraints. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185. IOS Press, Amsterdam, pp 613–631

    Google Scholar 

  • Li CM, Manya F, Planes J (2007) New inference rules for Max-SAT. J Artif Intell Res 30:321–359

    Article  MathSciNet  MATH  Google Scholar 

  • Li W, Xu C, Yang Y, Chen J, Wang J (2022) A refined branching algorithm for the maximum satisfiability problem. Algorithmica 84(4):982–1006

    Article  MathSciNet  MATH  Google Scholar 

  • Liao X (2013) Maximum satisfiability approach to game theory and network security. PhD thesis. Kyushu University

  • 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. IEEE, pp 284–291

  • Lourenço HR, Martin OC, Stützle T (2019) Iterated local search: framework and applications. In Handbook of metaheuristics. Springer, pp 129–168

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

    Article  MathSciNet  MATH  Google Scholar 

  • Luo C, Cai S, Su K, Wu W (2014) 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, Su K (2013) Focused random walk with configuration checking and break minimum for satisfiability. In: International conference on principles and practice of constraint programming. Springer, pp 481–496

  • Malan KM, Engelbrecht AP (2013) A survey of techniques for characterising fitness landscapes and some possible ways forward. Inf Sci 241:148–163

    Article  Google Scholar 

  • Martin OC, Otto SW (1996) Combining simulated annealing with local search heuristics. Ann Oper Res 63(1):57–75

    Article  MATH  Google Scholar 

  • Mertens S, Mézard M, Zecchina R (2006) Threshold values of random K-SAT from the cavity method. Random Struct Algorithms 28(3):340–373

    Article  MathSciNet  MATH  Google Scholar 

  • Merz P, Freisleben B (1999) Fitness landscapes and memetic algorithm design. In: Corne D, Dorigo M, Glover F, Dasgupta D, Moscato P, Poli R, Price KV (eds) New ideas in optimization. McGraw-Hill, London, pp 245–260

    Google Scholar 

  • Mézard M, Parisi G, Zecchina R (2002) Analytic and algorithmic solution of random satisfiability problems. Science 297(5582):812–815

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  • Nadel A (2019) TT-Open-WBO-Inc: tuning polarity and variable selection for anytime SAT-based optimization. In: Proceedings of the MaxSAT evaluations

  • Narodytska N, Bacchus F (2014) Maximum Satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th AAAI conference on artificial intelligence. AAAI Press, pp 2717–2723

  • Niedermeier R, Rossmanith P (2000) New upper bounds for maximum satisfiability. J Algorithms 36(1):63–88

    Article  MathSciNet  MATH  Google Scholar 

  • Pankratov D, Borodin A (2010) On the relative merits of simple local search methods for the MAX-SAT problem. In: Proceedings of the 13th international conference on theory and applications of satisfiability testing (SAT 2010). SAT’10. Springer, pp 223–236

  • Paxian T, Reimer S, Becker B (2018) Pacose: an iterative SAT-based MaxSAT solver. MaxSAT Eval 2018:20

    Google Scholar 

  • Pipatsrisawat K, Darwiche A (2007) Clone: solving weighted Max-SAT in a reduced search space. In: Australasian joint conference on artificial intelligence. Springer, pp 223–233

  • Poloczek M (2011) Bounds on greedy algorithms for MAX SAT. In Proceedings of the 19th European symposium on algorithms. ESA’11. Springer, pp 37–48

  • Poloczek M, Williamson DP (2016) An experimental evaluation of fast approximation algorithms for the maximum satisfiability problem. In: International symposium on experimental algorithms. Springer, pp 246–261

  • Poloczek M, Schnitger G, Williamson DP, Van Zuylen A (2017) Greedy algorithms for the maximum satisfiability problem: simple algorithms and inapproximability bounds. SIAM J Comput 46(3):1029–1061

    Article  MathSciNet  MATH  Google Scholar 

  • Prügel-Bennett A, Tayarani-Najaran M-H (2012) Maximum satisfiability: anatomy of the fitness landscape for a hard combinatorial optimization problem. IEEE Trans Evol Comput 16(3):319–338

    Article  Google Scholar 

  • Qasem M, Prügel-Bennett A (2010) Learning the large-scale structure of the MAX-SAT landscape using populations. IEEE Trans Evol Comput 14(4):518–529

    Article  Google Scholar 

  • Selman B, Kautz HA, Cohen B (1996) Local search strategies for satisfiability testing. In: DIMACS series in discrete mathematics and theoretical computer science, pp 521–532

  • Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: Proceedings of the 12th national conference on artificial intelligence, vol 1. American Association for Artificial Intelligence, pp 337–343

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

  • Smyth K, Hoos HH, Stützle T (2003) Iterated robust tabu search for MAX-SAT. In: Conference of the Canadian society for computational studies of intelligence. Springer, pp 129–144

  • Stadler P (2002) Fitness landscapes. In: Lässig M, Valleriani A (eds) Biological evolution and statistical physics. Springer, New York, pp 183–204

    Chapter  Google Scholar 

  • Sun Grid Engine (SGE) QuickStart (2020) http://star.mit.edu/cluster/docs/0.93.3/guides/sge.html

  • Sutton AM, Whitley LD, Howe AE (2009) A polynomial time computation of the exact correlation structure of k-satisfiability landscapes. In: proceedings of the 11th annual conference on genetic and evolutionary computation. ACM, pp 365–372

  • Tompkins DA, Hoos HH (2005) UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAXSAT. In: Proceedings of the 8th international conference on theory and applications of satisfiability testing. Springer, pp 306–320

  • Xiao M (2022) An exact MaxSAT algorithm: further observations and further improvements. Preprint, accepted to IJCAI

  • Yannakakis M (1994) On the approximation of maximum satisfiability. J Algorithms 17(3):475–502

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We thank Shaowei Cai for providing us access to the original authors’ implementation of the CCLS solver used in Max Sat Evaluation 2016, and André Abramé for providing us access to the abrame-habet benchmark used (partially) in that evaluation. We thank Gregory Gutin for his helpful comments on this paper. We also thank the anonymous referees for their useful comments and beneficial suggestions. This research was partially supported by the Milken Families Foundation Chair in Mathematics and by the Israeli Council for Higher Education (CHE) via Data Science Research Center, Ben-Gurion University of the Negev.

Author information

Authors and Affiliations

  1. Departments of Mathematics and of Computer Science, Ben-Gurion University, 84105, Beer Sheva, Israel

    Daniel Berend

  2. Department of Computer Science, Jerusalem College of Technology, 91160, Jerusalem, Israel

    Shahar Golan

  3. Department of Software Engineering, Shamoon College of Engineering, 8410802, Beer Sheva, Israel

    Yochai Twitto

Authors
  1. Daniel Berend
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shahar Golan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yochai Twitto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yochai Twitto.

Additional information

Publisher's Note

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

A preliminary version (Berend and Twitto 2020) of this work has been presented at the 18th International Symposium on Experimental Algorithms (SEA 2020). The contribution of this elaborated paper is mainly on the practical solving side. We performed a comprehensive empirical evaluation of the combined solver MOCE–CCLS on all the benchmarks from the Max Sat Evaluation of 2016 and 2021 to assess and establish its usability as a state-of-the-art solver for Max Sat.

Rights and permissions

Springer Nature or its licensor holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Berend, D., Golan, S. & Twitto, Y. Using the method of conditional expectations to supply an improved starting point for CCLS. J Comb Optim 44, 3711–3734 (2022). https://doi.org/10.1007/s10878-022-00907-5

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10878-022-00907-5

Keywords

Search

Navigation