scholarly journals Low-Rank Semidefinite Programming for the MAX2SAT Problem

2019 ◽  
Vol 33 ◽  
pp. 1641-1649
Author(s):  
Po-Wei Wang ◽  
J. Zico Kolter
Keyword(s):  
Semidefinite Programming ◽  
State Of The Art ◽  
Search Algorithm ◽  
Low Rank ◽  
Search Methods ◽  
Maximum Satisfiability ◽  
Satisfiability Problems ◽  
Theoretical Tool ◽  
Recent Approach ◽  
Programming Techniques

This paper proposes a new algorithm for solving MAX2SAT problems based on combining search methods with semidefinite programming approaches. Semidefinite programming techniques are well-known as a theoretical tool for approximating maximum satisfiability problems, but their application has traditionally been very limited by their speed and randomized nature. Our approach overcomes this difficult by using a recent approach to low-rank semidefinite programming, specialized to work in an incremental fashion suitable for use in an exact search algorithm. The method can be used both within complete or incomplete solver, and we demonstrate on a variety of problems from recent competitions. Our experiments show that the approach is faster (sometimes by orders of magnitude) than existing state-of-the-art complete and incomplete solvers, representing a substantial advance in search methods specialized for MAX2SAT problems.

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

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.

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

2017 ◽  
Author(s):  
Shaowei Cai ◽  
Chuan Luo ◽  
Haochen Zhang
Keyword(s):  
Combinatorial Optimization ◽  
Local Search ◽  
Optimization Problem ◽  
State Of The Art ◽  
Search Algorithm ◽  
Combinatorial Optimization Problem ◽  
Np Hard ◽  
Local Search Algorithm ◽  
Maximum Satisfiability ◽  
New Approach

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.

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

2017 ◽  
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.

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

2020 ◽  
Vol 176 (3-4) ◽  
pp. 271-297
Author(s):  
Mario Alviano ◽  
Carmine Dodaro
Keyword(s):  
State Of The Art ◽  
Answer Set Programming ◽  
Efficient Algorithms ◽  
Satisfiability Problem ◽  
Core Analysis ◽  
Stable Model ◽  
Maximum Satisfiability ◽  
Model Search ◽  
Unsatisfiable Core ◽  
Stable Models

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

Computing Robust Principal Components by A* Search

2018 ◽  
Vol 27 (07) ◽  
pp. 1860013 ◽  
Author(s):  
Swair Shah ◽  
Baokun He ◽  
Crystal Maung ◽  
Haim Schweitzer
Keyword(s):  
State Of The Art ◽  
Principal Component ◽  
Low Rank ◽  
A Algorithm ◽  
Running Time ◽  
Current State ◽  
Dimensionality Reduction Technique ◽  
Related Variant ◽  
Low Rank Representation ◽  
The Cost

Principal Component Analysis (PCA) is a classical dimensionality reduction technique that computes a low rank representation of the data. Recent studies have shown how to compute this low rank representation from most of the data, excluding a small amount of outlier data. We show how to convert this problem into graph search, and describe an algorithm that solves this problem optimally by applying a variant of the A* algorithm to search for the outliers. The results obtained by our algorithm are optimal in terms of accuracy, and are shown to be more accurate than results obtained by the current state-of-the- art algorithms which are shown not to be optimal. This comes at the cost of running time, which is typically slower than the current state of the art. We also describe a related variant of the A* algorithm that runs much faster than the optimal variant and produces a solution that is guaranteed to be near the optimal. This variant is shown experimentally to be more accurate than the current state-of-the-art and has a comparable running time.

scholarly journals GASAT: A Genetic Local Search Algorithm for the Satisfiability Problem

2006 ◽  
Vol 14 (2) ◽  
pp. 223-253 ◽  
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.

scholarly journals Low-Rank and Sparse Based Deep-Fusion Convolutional Neural Network for Crowd Counting

2017 ◽  
Vol 2017 ◽  
pp. 1-11 ◽  
Author(s):  
Siqi Tang ◽  
Zhisong Pan ◽  
Xingyu Zhou
Keyword(s):  
Neural Network ◽  
Convolutional Neural Network ◽  
State Of The Art ◽  
Regression Method ◽  
Low Rank ◽  
Counting Method ◽  
Direct Integral ◽  
Crowd Counting ◽  
Counting Methods ◽  
Density Map

This paper proposes an accurate crowd counting method based on convolutional neural network and low-rank and sparse structure. To this end, we firstly propose an effective deep-fusion convolutional neural network to promote the density map regression accuracy. Furthermore, we figure out that most of the existing CNN based crowd counting methods obtain overall counting by direct integral of estimated density map, which limits the accuracy of counting. Instead of direct integral, we adopt a regression method based on low-rank and sparse penalty to promote accuracy of the projection from density map to global counting. Experiments demonstrate the importance of such regression process on promoting the crowd counting performance. The proposed low-rank and sparse based deep-fusion convolutional neural network (LFCNN) outperforms existing crowd counting methods and achieves the state-of-the-art performance.

scholarly journals A Boosting Framework of Factorization Machine

2021 ◽  
pp. 2159036
Author(s):  
Jun Zhou ◽  
Longfei Li ◽  
Ziqi Liu ◽  
Chaochao Chen
Keyword(s):  
Large Scale ◽  
State Of The Art ◽  
Experimental Results ◽  
Low Rank ◽  
Inner Product ◽  
Adaptive Boosting ◽  
Rank Matrix ◽  
Factorization Machine ◽  
Fixed Rank ◽  
Low Rank Matrix

Recently, Factorization Machine (FM) has become more and more popular for recommendation systems due to its effectiveness in finding informative interactions between features. Usually, the weights for the interactions are learned as a low rank weight matrix, which is formulated as an inner product of two low rank matrices. This low rank matrix can help improve the generalization ability of Factorization Machine. However, to choose the rank properly, it usually needs to run the algorithm for many times using different ranks, which clearly is inefficient for some large-scale datasets. To alleviate this issue, we propose an Adaptive Boosting framework of Factorization Machine (AdaFM), which can adaptively search for proper ranks for different datasets without re-training. Instead of using a fixed rank for FM, the proposed algorithm will gradually increase its rank according to its performance until the performance does not grow. Extensive experiments are conducted to validate the proposed method on multiple large-scale datasets. The experimental results demonstrate that the proposed method can be more effective than the state-of-the-art Factorization Machines.

scholarly journals Low-rank exploitation in semidefinite programming for control

2011 ◽  
Vol 84 (12) ◽  
pp. 1975-1982 ◽  
Author(s):  
Rikard Falkeborn ◽  
Johan Löfberg ◽  
Anders Hansson
Keyword(s):  
Semidefinite Programming ◽  
Low Rank
Sign in / Sign up

Export Citation Format

Share Document