article

A multilevel memetic algorithm for large sat-encoded problems

Author:

Noureddine BouhmalaAuthors Info & Claims

Evolutionary Computation, Volume 20, Issue 4

Pages 641 - 664

https://doi.org/10.1162/EVCO_a_00078

Published: 01 December 2012 Publication History

Abstract

Many researchers have focused on the satisfiability problem and on many of its variants due to its applicability in many areas of artificial intelligence. This NP-complete problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. In this work, we introduce a memetic algorithm that makes use of the multilevel paradigm. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward toward the solution of the original problem, using a solution from a previous level as a starting solution at the next level. Results comparing the memetic with and without the multilevel paradigm are presented using problem instances drawn from real industrial hardware designs.

References

[1]

Barnard, S. T., and Simon, H. D. (1994). A fast multilevel implementation of recursive spectral bisection for partitioning unstructured problems. Concurrency: Practice and Experience, 6(2):101-117.

[2]

Blum, C., and Roli, A. (2003). Metaheuristics in combinatorial optimization: Overview and conceptual comparison. ACM Computing Surveys, 35(3):268-308.

[3]

Boughaci, D., Benhamou, B., and Drias, H. (2008). Scatter search and genetic algorithms for MAX-SAT problems. Journal of Mathematical Modelling and Algorithms, 7(2):101-124.

[4]

Boughaci, D., and Drias, H. (2005). Efficient and experimental meta-heuristics for MAX-SAT problems. In Lecture Notes in Computer Science, Vol. 3503 (pp. 501-512). Berlin: Springer-Verlag.

[5]

Clark, E. M., Emerson, E. A., and Sista,A. P. (1996).Automatic verification of finite state on current systems using temporal logic specifications.ACMTransactions on Programming Languages and Systems, 8:244-263.

[6]

Cook, S. A. (1971). The complexity of theorem-proving procedures. In Proceedings of the Third ACM Symposium on Theory of Computing, pp. 151-158.

[7]

Gary, M. R., and Johnson, D. S. (1979). Computers and intractability: A guide to the theory of NP-completeness. New York:W.H. Freeman.

[8]

Gent, L. P., and Walsh, T. (1993). Towards an understanding of hill-climbing procedures for SAT. In Proceedings of AAAI '93, pp. 28-33.

[9]

Gent, I., and Walsh, T. (1995). Unsatisfied variables in local search. In J. Hallam (Ed.), Hybrid problems, hybrid solutions (pp. 73-85). Amsterdam: IOS Press.

[10]

Glover, F. (1989). Tabu search--Part 1. ORSA Journal on Computing, 1(3):190-206.

[11]

Goldberg, E., and Novikov, Y. (2002). BerkMin: A Fast and Robust SAT-solver. Proceedings of the Conference on Design, Automation and Test in Europe Conference and Exhibition, p. 142.

[12]

Gottleib, J., Marchiori, E., and Rossi, C. (2002). Evolutionary algorithms for the satisfiability problem. Evolutionary Computation, 10(1):35-50.

[13]

Granmo, O. C., and Bouhmala, N. (2007). Solving the satisfiability problem using finite learning automata. International Journal of Computer Science and Applications, 4(3):15-29.

[14]

Hadany, R., and Harel, D. (1999). A multi-scale algorithm for drawing graphs nicely. Weizmann Institute, Faculty of Mathematics and Computer Science (Tech. Rep. No. CS99-01).

[15]

Hansen, P., and Jaumand, B. (1990). Algorithms for the maximum satisfiability problem. Computing, 44:279-303.

[16]

Hendrickson, B., and Leland, R. (1995).Amultilevel algorithm for partitioning graphs. In S. Karin (Ed.), Proceedings of the Supercomputing '95 Conference.

[17]

Hoos, H. (1999). On the run-time behavior of stochastic local search algorithms for SAT. In Proceedings of AAAI-99, pp. 661-666.

[18]

Hoos, H. (2002). An adaptive noise mechanism for WalkSAT. In Proceedings of the Eighteenth National Conference in Artificial Intelligence (AAAI-02), pp. 655-660.

[19]

Hutter, F., Tompkins, D., and Hoos, H. (2002). Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In Proceedings of the Eighth International Conference of the Principles and Practice of Constraint Programming (CP '02), pp. 233-248.

[20]

Ishtaiwi, A., Thornton, J., Sattar, A., and Pham, D. N. (2005). Neighborhood clause weight redistribution in local search for SAT. In Proceedings of the Eleventh International Conference on Principles and Practice Programming (CP-05). Lecture Notes in Computer Science, Vol. 3709 (pp. 772-776). Berlin: Springer-Verlag.

[21]

Jin-Kao, H., Lardeux, F., and Saubion, F. (2003). Evolutionary computing for the satisfiability problem. In Applications of evolutionary computing. Lecture Notes in Computer Science, Vol. 2611 (pp. 258-267). Berlin: Springer-Verlag.

[22]

Karypis, G., and Kumar, V. (1998a). A fast and high quality multilevel scheme for partitioning irregular graphs. SIAM Journal on Scientific Computing, 20(1):359-392.

[23]

Karypis, G., and Kumar, V. (1998b). Multilevel k-way partitioning scheme for irregular graphs. Journal of Parallel and Distributed Computing, 48(1):96-129.

[24]

Khudabukhsh, A. R., Xu, L., Hoos, H. H., and Leyton-Brown, K. (2009). SATenstein: Automatically building local search SAT solvers from components. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI-09). www.aaai.org/ocs/index.php/IJCAI/IJCAI-09/paper/view/657

[25]

Lardeux, F., Saubion, F., and Jin-Kao, H. (2006). GASAT: A genetic local search algorithm for the satisfiability problem. Evolutionary Computation, 14(2):223-253.

[26]

Li, C. M., and Huang, W. Q. (2005). Diversification and determinism in local search for satisfiability. In Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT-05). Lecture Notes in Computer Science, Vol. 3569 (pp. 158-172). Berlin: Springer-Verlag.

[27]

Li, C. M., Wei, W., and Zhang, H. (2007). Combining adaptive noise and look-ahead in local search for SAT. In Proceedings of the Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT-07). Lecture Notes in Computer Science, Vol. 4501 (pp. 121-133). Berlin: Springer-Verlag.

[28]

Lozano., M., and Martinez, C. G. (2010). Hybrid metaheuristics with evolutionary algorithms specializing in intensification and diversification: Overview and progress report. Computers and Operations Research, 37:481-497.

[29]

Mahajan, Y., Fu, Z., and Malik, S. (2004). Zchaff2004: An efficient SAT solver. In Proceedings of SAT 2004.

[30]

McAllester, D., Selman, B., and Kautz, H. (1997). Evidence for invariants in local search. In Proceedings of AAAI '97, pp. 321-326.

[31]

Moscato, P. A. (1989). On evolution search, optimization, genetic algorithms and martial arts: Towards memetic algorithms. Caltech Concurrent Computation Program, Pasadena, CA. (Tech. Rep. No. C3P 826)

[32]

Patterson, D. J., and Kautz, H. (2001). Auto-WalkSAT: A self-tuning implementation of WalkSAT. Electronic Notes on Discrete Mathematics, 9.

[33]

Prestwich, S. (2005). Random walk with continuously smoothed variable weights. In Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT-05). Lecture Notes in Computer Science, Vol. 3569 (pp. 203-215). Berlin: Springer-Verlag.

[34]

Schuurmans, D., and Southey, F. (2000). Local search characteristics of incompleteSAT procedures. In Proceedings of AAAI-2000, pp. 297-302.

[35]

Schuurmans, D., Southey, F., and Holte, R. C. (2001). The exponentiated sub-gradient algorithm for heuristic Boolean programming. In Proceedings of IJCAI-01, pp. 334-341.

[36]

Selman, B., and Kautz, H. A. (1993). Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In R. Bajcsy (Ed.), Proceedings of the International Joint Conference on Artificial Intelligence, pp. 290-295.

[37]

Selman, B., Kautz, H. A., and Cohen, B. (1994). Noise strategies for improving local search. In Proceedings of AAAI '94, pp. 337-343.

[38]

Selman, B., Levesque, H., and Mitchell, D. (1992). A new method for solving hard satisfiability problems. In Proceedings of AAA '92, pp. 440-446.

[39]

Spears, W. (1995). Adapting crossover in evolutionary algorithms. In Proceedings of the Fourth Annual Conference on Evolutionary Programming, pp. 367-384.

[40]

Thornton, J., Pham, D. N., Bain, S., and Ferreira, V. (2004). Additive versus multiplicative clause weighting for SAT. In Proceedings of the Nineteenth National Conference of Artificial Intelligence (AAAI-04), pp. 191-196.

[41]

Vrajitoru, D. (1999). Genetic programming operators applied to genetic algorithms. In Proceedings of the Genetic and Evolutionary Computation Conference, pp. 686-693.

[42]

Walshaw, C. (2001a). A multilevel approach to the graph colouring problem. University of Greenwich, School of Computing and Mathematical Sciences, London. (Tech. Rep. No. 01/IM/69)

[43]

Walshaw, C. (2001b). A multilevel Lin-Kerninghan-Helsgaun algorithm for the traveling salesman problem. (Tech. Rep. No. 01/IM/80)

[44]

Walshaw, C. (2002). A multilevel approach to the traveling salesman problem. Operations Research, 50(5):862-877.

[45]

Walshaw, C. (2003). A multilevel algorithm for forced-directed graph-drawing. Journal of Graph Algorithms and Applications, 7(3):253-285.

[46]

Walshaw, C., and Cross, M. (2000). Mesh partitioning: A multilevel balancing and refinement algorithm. SIAM Journal on Scientific Computing, 22(1):63-80.

[47]

Wu, Z., and Wah, B. (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 (AAAI-00), pp. 310-315.

Cited By

Omidvar MLi XYao X(2022)A Review of Population-Based Metaheuristics for Large-Scale Black-Box Global Optimization—Part IIEEE Transactions on Evolutionary Computation10.1109/TEVC.2021.313083826:5(802-822)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1109/TEVC.2021.3130838
Yazidi ABouhmala NGoodwin M(2020)A team of pursuit learning automata for solving deterministic optimization problemsApplied Intelligence10.1007/s10489-020-01657-950:9(2916-2931)Online publication date: 14-Apr-2020
https://dl.acm.org/doi/10.1007/s10489-020-01657-9
Bouhmala N(2019)Combining simulated annealing with local search heuristic for MAX-SATJournal of Heuristics10.1007/s10732-018-9386-925:1(47-69)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10732-018-9386-9
Show More Cited By

Index Terms

A multilevel memetic algorithm for large sat-encoded problems
1. Mathematics of computing
  1. Mathematical analysis
2. Theory of computation
  1. Design and analysis of algorithms
    1. Mathematical optimization

Recommendations

Properties of the satisfiability threshold of the strictly d-regular random (3,2s)-SAT problem
Abstract
A k-CNF (conjunctive normal form) formula is a regular (k, s)-CNF one if every variable occurs s times in the formula, where k ⩾ 2 and s > 0 are integers. Regular (3, s)-CNF formulas have some good structural properties, so carrying out a ... $\frac{}{}$ $\frac{}{}$
Memetic multilevel hypergraph partitioning
GECCO '18: Proceedings of the Genetic and Evolutionary Computation Conference

Hypergraph partitioning has a wide range of applications such as VLSI design or scientific computing. With focus on solution quality we develop the first multilevel memetic algorithm to tackle the problem. Key components of our contribution are new ...
Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Evolutionary Computation

Evolutionary Computation Volume 20, Issue 4

Winter 2012

180 pages

ISSN:1063-6560

EISSN:1530-9304

Issue’s Table of Contents

Publisher

MIT Press

Cambridge, MA, United States

Publication History

Published: 01 December 2012

Published in EVOL Volume 20, Issue 4

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
99
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Omidvar MLi XYao X(2022)A Review of Population-Based Metaheuristics for Large-Scale Black-Box Global Optimization—Part IIEEE Transactions on Evolutionary Computation10.1109/TEVC.2021.313083826:5(802-822)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1109/TEVC.2021.3130838
Yazidi ABouhmala NGoodwin M(2020)A team of pursuit learning automata for solving deterministic optimization problemsApplied Intelligence10.1007/s10489-020-01657-950:9(2916-2931)Online publication date: 14-Apr-2020
https://dl.acm.org/doi/10.1007/s10489-020-01657-9
Bouhmala N(2019)Combining simulated annealing with local search heuristic for MAX-SATJournal of Heuristics10.1007/s10732-018-9386-925:1(47-69)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10732-018-9386-9
Bouhmala N(2016)A variable neighbourhood search structure based-genetic algorithm for combinatorial optimisation problemsInternational Journal of Intelligent Systems Technologies and Applications10.1504/IJISTA.2016.07649415:2(127-146)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1504/IJISTA.2016.076494
Bouhmala N(2016)A multilevel genetic algorithm for the clustering problemInternational Journal of Information and Communication Technology10.1504/IJICT.2016.0776929:1(101-116)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1504/IJICT.2016.077692
Lian TLlave MGoodwin MBouhmala N(2015)Towards Multilevel Ant Colony Optimisation for the Euclidean Symmetric Traveling Salesman ProblemProceedings of the 28th International Conference on Current Approaches in Applied Artificial Intelligence - Volume 910110.1007/978-3-319-19066-2_22(222-231)Online publication date: 10-Jun-2015
https://dl.acm.org/doi/10.1007/978-3-319-19066-2_22
Djeffal MDrias H(2013)Multilevel Bee Swarm Optimization for Large Satisfiability Problem InstancesProceedings of the 14th International Conference on Intelligent Data Engineering and Automated Learning --- IDEAL 2013 - Volume 820610.1007/978-3-642-41278-3_72(594-602)Online publication date: 20-Oct-2013
https://dl.acm.org/doi/10.1007/978-3-642-41278-3_72

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents