An iterative path-breaking approach with mutation and restart strategies for the MAX-SAT problem

DOI10.1016/J.COR.2018.12.005zbMATH Open1458.68205arXiv1808.03611OpenAlexW2887749339MaRDI QIDQ1725596FDOQ1725596

Authors: Zhenxing Xu, Kun He, Chu-Min Li 

Publication date: 14 February 2019

Published in: Computers \& Operations Research (Search for Journal in Brave)

Abstract: Although Path-Relinking is an effective local search method for many combinatorial optimization problems, its application is not straightforward in solving the MAX-SAT, an optimization variant of the satisfiability problem (SAT) that has many real-world applications and has gained more and more attention in academy and industry. Indeed, it was not used in any recent competitive MAX-SAT algorithms in our knowledge. In this paper, we propose a new local search algorithm called IPBMR for the MAX-SAT, that remedies the drawbacks of the Path-Relinking method by using a careful combination of three components: a new strategy named Path-Breaking to avoid unpromising regions of the search space when generating trajectories between two elite solutions; a weak and a strong mutation strategies, together with restarts, to diversify the search; and stochastic path generating steps to avoid premature local optimum solutions. We then present experimental results to show that IPBMR outperforms two of the best state-of-the-art MAX-SAT solvers, and an empirical investigation to identify and explain the effect of the three components in IPBMR.

Full work available at URL: https://arxiv.org/abs/1808.03611

Recommendations

• Cooperative parallel SAT local search with path relinking
• GRASP with path relinking for the weighted MAXSAT problem
• Experimental and Efficient Algorithms
• On the Relative Merits of Simple Local Search Methods for the MAX-SAT Problem
• Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability

zbMATH Keywords

combinatorial optimizationlocal searchmutationmaximum satisfiabilitypath-breaking

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Approximation methods and heuristics in mathematical programming (90C59) Combinatorial optimization (90C27) Computational aspects of satisfiability (68R07)

Cites Work

• Theory and Applications of Satisfiability Testing
• Local search for Boolean satisfiability with configuration checking and subscore
• CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability
• Fundamentals of scatter search and path relinking
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• The community structure of SAT formulas
• The first and second Max-SAT evaluations
• New inference rules for Max-SAT
• Local search with edge weighting and configuration checking heuristics for minimum vertex cover
• GRASP with path relinking for the weighted MAXSAT problem
• Theory and Applications of Satisfiability Testing
• Genetic Algorithms and the Optimal Allocation of Trials
• Improving configuration checking for satisfiable random \(k\)-SAT instances
• Exploiting subproblem optimization in SAT-based maxsat algorithms
• Title not available (Why is that?)
• WPM3: an (in)complete algorithm for weighted partial MaxSAT
• A path-relinking algorithm for the multi-mode resource-constrained project scheduling problem

Cited In (1)

• Improved local search for the minimum weight dominating set problem in massive graphs by using a deep optimization mechanism

Uses Software

• UBCSAT
• Scatter Search
• CCASat
• CCLS
• WPM3

This page was built for publication: An iterative path-breaking approach with mutation and restart strategies for the MAX-SAT problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1725596)