From Decimation to Local Search and Back: A New Approach to MaxSAT

Maximum Satisfiability (MaxSAT) is an important NP-hard combinatorial optimization problem with many applications and MaxSAT solving has attracted much interest. This work proposes a new incomplete approach to MaxSAT. We propose a novel decimation algorithm for MaxSAT, and then combine it with a local search algorithm. Our approach works by interleaving between the decimation algorithm and the local search algorithm, with useful information passed between them. Experiments show that our solver DeciLS achieves state of the art performance on all unweighted benchmarks from the MaxSAT Evaluation 2016. Moreover, compared to SAT-based MaxSAT solvers which dominate industrial benchmarks for years, it performs better on industrial benchmarks and significantly better on application formulas from SAT Competition. We also extend this approach to (Weighted) Partial MaxSAT, and the resulting solvers significantly improve local search solvers on crafted and industrial benchmarks, and are complementary (better on WPMS crafted benchmarks) to SAT-based solvers.

Download Full-text

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

The Computer Journal ◽

10.1093/comjnl/bxz063 ◽

2019 ◽

Vol 63 (9) ◽

pp. 1321-1337

Author(s):

Zhendong Lei ◽

Shaowei Cai

Keyword(s):

Local Search ◽

State Of The Art ◽

Search Algorithm ◽

Local Search Algorithm ◽

Significant Progress ◽

Weighted Version ◽

Maximum Satisfiability ◽

Real World Applications ◽

Better Than ◽

Made In

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 search is a popular method for solving (W)PMS. Recently, significant progress has been made in this direction by tailoring local search for (W)PMS, and a representative algorithm is the Dist algorithm. In this paper, we propose two ideas to improve Dist, including a clause-weighting scheme and a variable-selection heuristic. The resulting algorithm is called NuDist. Extensive experiments on PMS and WPMS benchmarks from the MaxSAT Evaluations (MSE) 2016 and 2017 show that NuDist significantly outperforms state-of-the-art local search solvers and performs better than state-of-the-art complete solvers including Open-WBO and WPM3 on MSE 2017 benchmarks. Also, empirical analyses confirm the effectiveness of the proposed ideas.

Download Full-text

CCEHC: An Efficient Local Search Algorithm for Weighted Partial Maximum Satisfiability (Extended Abstract)

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2017/716 ◽

2017 ◽

Cited By ~ 1

Author(s):

Chuan Luo ◽

Shaowei Cai ◽

Kaile Su ◽

Wenxuan Huang

Keyword(s):

Local Search ◽

State Of The Art ◽

Search Algorithm ◽

Stochastic Local Search ◽

Local Search Algorithm ◽

Maximum Satisfiability ◽

Biased Random Walk ◽

Configuration Checking ◽

Significant Generalization ◽

Max Sat

Weighted partial maximum satisfiability (WPMS) is a significant generalization of maximum satisfiability (MAX-SAT), with many important applications. Recently, breakthroughs have been made on stochastic local search (SLS) for weighted MAX-SAT and (unweighted) partial MAX-SAT (PMS). However, the performance of SLS for WPMS lags far behind. In this work, we present a new SLS algorithm named CCEHC for WPMS. CCEHC is mainly based on a heuristic emphasizing hard clauses, which has three components: a variable selection mechanism focusing on configuration checking based only on hard clauses, a weighting scheme for hard clauses, and a biased random walk component. Experiments show that CCEHC significantly outperforms its state-of-the-art SLS competitors. Experiments comparing CCEHC with a state-of-the-art complete solver indicate the effectiveness of CCEHC on a number of application WPMS instances.

Download Full-text

GASAT: A Genetic Local Search Algorithm for the Satisfiability Problem

Evolutionary Computation ◽

10.1162/evco.2006.14.2.223 ◽

2006 ◽

Vol 14 (2) ◽

pp. 223-253 ◽

Cited By ~ 48

Author(s):

Frédéric Lardeux ◽

Frédéric Saubion ◽

Jin-Kao Hao

Keyword(s):

Tabu Search ◽

Local Search ◽

Hybrid Algorithm ◽

State Of The Art ◽

Search Algorithm ◽

Satisfiability Problem ◽

Local Search Algorithm ◽

Overall Performance ◽

Genetic Local Search ◽

Search Stage

This paper presents GASAT, a hybrid algorithm for the satisfiability problem (SAT). The main feature of GASAT is that it includes a recombination stage based on a specific crossover and a tabu search stage. We have conducted experiments to evaluate the different components of GASAT and to compare its overall performance with state-of-the-art SAT algorithms. These experiments show that GASAT provides very competitive results.

Download Full-text

Solving the Set Packing Problem via a Maximum Weighted Independent Set Heuristic

Mathematical Problems in Engineering ◽

10.1155/2020/3050714 ◽

2020 ◽

Vol 2020 ◽

pp. 1-11

Author(s):

Ruizhi Li ◽

Yupan Wang ◽

Shuli Hu ◽

Jianhua Jiang ◽

Dantong Ouyang ◽

...

Keyword(s):

Combinatorial Optimization ◽

Optimization Problem ◽

State Of The Art ◽

Independent Set ◽

Packing Problem ◽

Combinatorial Optimization Problem ◽

Set Packing ◽

Benchmark Instances ◽

Set Packing Problem

The set packing problem (SPP) is a significant NP-hard combinatorial optimization problem with extensive applications. In this paper, we encode the set packing problem as the maximum weighted independent set (MWIS) problem and solve the encoded problem with an efficient algorithm designed to the MWIS problem. We compare the independent set-based method with the state-of-the-art algorithms for the set packing problem on the 64 standard benchmark instances. The experimental results show that the independent set-based method is superior to the existing algorithms in terms of the quality of the solutions and running time obtained the solutions.

Download Full-text

NuMVC: An Efficient Local Search Algorithm for Minimum Vertex Cover

Journal of Artificial Intelligence Research ◽

10.1613/jair.3907 ◽

2013 ◽

Vol 46 ◽

pp. 687-716 ◽

Cited By ~ 45

Author(s):

S. Cai ◽

K. Su ◽

C. Luo ◽

A. Sattar

Keyword(s):

Local Search ◽

Heuristic Algorithms ◽

State Of The Art ◽

Search Algorithm ◽

Vertex Cover ◽

Experimental Studies ◽

Maximum Clique ◽

Local Search Algorithm ◽

Two Stage ◽

Edge Weighting

The Minimum Vertex Cover (MVC) problem is a prominent NP-hard combinatorial optimization problem of great importance in both theory and application. Local search has proved successful for this problem. However, there are two main drawbacks in state-of-the-art MVC local search algorithms. First, they select a pair of vertices to exchange simultaneously, which is time-consuming. Secondly, although using edge weighting techniques to diversify the search, these algorithms lack mechanisms for decreasing the weights. To address these issues, we propose two new strategies: two-stage exchange and edge weighting with forgetting. The two-stage exchange strategy selects two vertices to exchange separately and performs the exchange in two stages. The strategy of edge weighting with forgetting not only increases weights of uncovered edges, but also decreases some weights for each edge periodically. These two strategies are used in designing a new MVC local search algorithm, which is referred to as NuMVC. We conduct extensive experimental studies on the standard benchmarks, namely DIMACS and BHOSLIB. The experiment comparing NuMVC with state-of-the-art heuristic algorithms show that NuMVC is at least competitive with the nearest competitor namely PLS on the DIMACS benchmark, and clearly dominates all competitors on the BHOSLIB benchmark. Also, experimental results indicate that NuMVC finds an optimal solution much faster than the current best exact algorithm for Maximum Clique on random instances as well as some structured ones. Moreover, we study the effectiveness of the two strategies and the run-time behaviour through experimental analysis.

Download Full-text

Maximum Satisfiability: Anatomy of the Fitness Landscape for a Hard Combinatorial Optimization Problem

IEEE Transactions on Evolutionary Computation ◽

10.1109/tevc.2011.2163638 ◽

2012 ◽

Vol 16 (3) ◽

pp. 319-338 ◽

Cited By ~ 27

Author(s):

Adam Prugel-Bennett ◽

Mohammad-Hassan Tayarani-Najaran

Keyword(s):

Combinatorial Optimization ◽

Optimization Problem ◽

Fitness Landscape ◽

Combinatorial Optimization Problem ◽

Maximum Satisfiability

Download Full-text

Implementasi Metode Tabu Search Dalam Penjadwalan Menggunakan Analisa Pieces

INFORMAL: Informatics Journal ◽

10.19184/isj.v6i2.23811 ◽

2021 ◽

Vol 6 (2) ◽

pp. 62

Author(s):

Made Suci Ariantini ◽

Ayu Manik Dirgayusari

Keyword(s):

Combinatorial Optimization ◽

Tabu Search ◽

Local Search ◽

Optimization Problem ◽

Search Method ◽

Combinatorial Optimization Problem ◽

Microsoft Excel ◽

Long Time ◽

The Subject ◽

Tabu Search Method

Nowadays, Scheduling subjects is one of the first steps for starting the teaching and learning process in educational institutions. To do so, The role of teachers and school staff is very important and not easy because it takes a long time to compile it. SMK PGRI 4 Denpasar is one of the schools located in the city of Denpasar which is located on Jalan Kebo Iwa No 8, Padangsambian Kaja, Denpasar, Bali. It is a vocational high school that has a tourism expertise and computer engineering study program. Based on current results of observations and interviews, the process of making the subject schedules that run at SMK PGRI 4 Denpasar is still being done using Microsoft Excel, this has resulted in frequent errors in managing schedules such as conflicting schedule and it takes a long time to correct it. Tabu Search is an optimization method based on local search, where the search process moves from one solution to the next by selecting the best solution which is not classified as a prohibited solution. It is a combinatorial optimization problem-solving method that is incorporated into local search methods. This method aims to streamline the process of finding the best solution of a large-scale (np-hard) combinatorial optimization problem. Tabu search method to optimize the process of making the subject schedule and combined using PIECES analysis (Performance, Information, Economic, Control, Efficiency, Services). From this analysis, several problems will be obtained, which in the end can be identified clearly and more specifically, so that we can conclude some suggestions that will help in designing a new and better system. The Tabu Search method can be used to optimize the process of making the subject schedules at SMK PGRI 4 Denpasar, so that the scheduling process will be more easier than using Microsoft Excel.

Download Full-text

An Interactive Regret-Based Genetic Algorithm for Solving Multi-Objective Combinatorial Optimization Problems

Proceedings of the AAAI Conference on Artificial Intelligence ◽

10.1609/aaai.v34i03.5612 ◽

2020 ◽

Vol 34 (03) ◽

pp. 2335-2342

Author(s):

Nawal Benabbou ◽

Cassandre Leroy ◽

Thibaut Lust

Keyword(s):

Combinatorial Optimization ◽

Optimization Problem ◽

Optimization Problems ◽

Optimal Solution ◽

Computation Time ◽

Preference Elicitation ◽

Combinatorial Optimization Problem ◽

New Approach ◽

Multi Objective ◽

Combinatorial Optimization Problems

We propose a new approach consisting in combining genetic algorithms and regret-based incremental preference elicitation for solving multi-objective combinatorial optimization problems with unknown preferences. For the purpose of elicitation, we assume that the decision maker's preferences can be represented by a parameterized scalarizing function but the parameters are initially not known. Instead, the parameter imprecision is progressively reduced by asking preference queries to the decision maker during the search to help identify the best solutions within a population. Our algorithm, called RIGA, can be applied to any multi-objective combinatorial optimization problem provided that the scalarizing function is linear in its parameters and that a (near-)optimal solution can be efficiently determined when preferences are known. Moreover, RIGA runs in polynomial time while asking no more than a polynomial number of queries. For the multi-objective traveling salesman problem, we provide numerical results showing its practical efficiency in terms of number of queries, computation time and gap to optimality.

Download Full-text