Chuan Luo

TACAS Conference 2026 Conference Paper

SMT(LIA) Sampling with High Diversity

• Yong Lai
• Junjie Li
• Chuan Luo

AAAI Conference 2025 Conference Paper

Better Understandings and Configurations in MaxSAT Stochastic Local Search Solvers via Anytime Performance Analysis

• Furong Ye
• Chuan Luo
• Shaowei Cai

Though numerous solvers have been proposed for the MaxSAT problem, and the benchmark environment such as MaxSAT Evaluations provides a platform for the comparison of the state-of-the-art solvers, existing assessments were usually evaluated based on the quality, e.g., fitness, of the best-found solutions obtained within a given running time budget. However, concerning solely the final obtained solutions regarding specific time budgets may restrict us from comprehending the behavior of the solvers along the convergence process. This paper demonstrates that Empirical Cumulative Distribution Functions can be used to compare MaxSAT stochastic local search solvers' anytime performance across multiple problem instances and various time budgets. The assessment reveals distinctions in solvers' performance and displays that the (dis)advantages of solvers adjust along different running times. This work also exhibits that the quantitative and high variance assessment of anytime performance can guide machines, i.e., automatic configurators, to search for better parameter settings. Our experimental results show that the hyperparameter optimization tool, i.e., SMAC, can achieve better parameter settings of solvers when using the anytime performance as the cost function, compared to using the metrics based on the fitness of the best-found solutions.

NeurIPS Conference 2025 Conference Paper

Beyond Node-Centric Modeling: Sketching Signed Networks with Simplicial Complexes

• Wei Wu
• Xuan Tan
• Yan Peng
• Ling Chen
• Fangfang Li
• Chuan Luo

Signed networks can reflect more complex connections through positive and negative edges, and cost-effective signed network sketching can significantly benefit an important link sign prediction task in the era of big data. Existing signed network embedding algorithms mainly learn node representation in the Graph Neural Network (GNN) framework with the balance theory. However, the node-wise representation learning methods either limit the representational power because they primarily rely on node pairwise relationship in the network, or suffer from severe efficiency issues. Recent research has explored simplicial complexes to capture higher-order interactions and integrated them into GNN frameworks. Motivated by that, we propose EdgeSketch+, a simple and effective edge embedding algorithm beyond traditional node-centric modeling that directly represents edges as low-dimensional vectors without transitioning from node embeddings. The proposed approach maintains a good balance between accuracy and efficiency by exploiting the Locality Sensitive Hashing (LSH) technique to swiftly capture the higher-order information derived from the simplicial complex in a manner of no learning processes. Experiments show that EdgeSketch+ matches state-of-the-art accuracy while significantly reducing runtime, achieving speedups of up to $546. 07\times$ compared to GNN-based methods.

EAAI Journal 2025 Journal Article

Non-convex regularized robust multimodal feature selection via self-representation learning for Alzheimer’s disease diagnosis

• Xi Guo
• Hongmei Chen
• Biao Xiang
• Zhong Yuan
• Chuan Luo
• Shi-Jinn Horng
• Tianrui Li

Multimodal neuroimaging data fusion has become a key research direction in Alzheimer’s Disease (AD) diagnosis. However, existing methods face challenges such as (1) Limited robustness against outliers and noise, which hampers effective feature selection; (2) Limitations of conventional convex approximation methods, such as the ℓ 2, 1 norm, in approximating the ideal ℓ 2, 0 norm, making it challenging to capture sparse structures accurately; (3) Inadequate modeling of feature correlations, leading to missed identification of synergistic feature groups. To address these issues, this study proposes a Non-Convex Regularized Robust Multimodal Feature Selection method via Self-Representation Learning for Alzheimer’s Disease diagnosis (NCRRFS). Specifically, self-representation learning is employed to model the error terms of anomalous samples, enabling the adaptive detection and correction of abnormal data, thereby enhancing the robustness of the model. Furthermore, an ℓ 2, γ norm row sparsity constraint based on the Smoothly Clipped Absolute Deviation (SCAD) function is designed to more accurately approximate the ℓ 2, 0 norm. Additionally, a graph-structured regularization based on Pearson correlation promotes the selection of synergistic feature groups. Extensive experimental results demonstrate the effectiveness and superiority of the proposed method in the Alzheimer’s disease classification task.

EAAI Journal 2024 Journal Article

LEFMIFS: Label enhancement and fuzzy mutual information for robust multilabel feature selection

• Tengyu Yin
• Hongmei Chen
• Zhong Yuan
• Binbin Sang
• Shi-Jinn Horng
• Tianrui Li
• Chuan Luo

Feature selection is one of the quite important preprocessing steps in multilabel learning. However, multilabel feature selection is facing big challenges due to high-dimensional and noise-contaminated data. In addition, most existing multilabel feature selection methods mainly center around the assumption of uniform label distribution. Meanwhile, the difference in significance of the labels associated with the sample is ubiquitous in many real-world applications. Motivated by these, this paper proposes a robust multilabel feature selection algorithm in which label enhancement is embedded into feature selection. Firstly, based on exploring dual-space identifying information, the data distribution of natural neighbors is further discussed, and the original logical label is enhanced to the label distribution form. Furthermore, a robust multilabel β -precision fuzzy rough sets model (ML β PFRS) is constructed. Combining the algebraic view with the information view in ML β PFRS defines a novel multilabel fuzzy entropy, and some properties and relationships are discussed. What’s more, an objective evaluation function is designed to estimate the quality of the features. Finally, a label enhancement and fuzzy mutual information-based robust multilabel feature selection algorithm is proposed. The extensive experiments performed on thirteen publicly available datasets demonstrate that compared with some advanced algorithms, LEFMIFS is not only for obtaining the feature subset with better classification performance but also for maintaining good robustness.

AAAI Conference 2023 Short Paper

Feature Decomposition for Reducing Negative Transfer: A Novel Multi-Task Learning Method for Recommender System (Student Abstract)

• Jie Zhou
• Qian Yu
• Chuan Luo
• Jing Zhang

We propose a novel multi-task learning method termed Feature Decomposition Network (FDN). The key idea of the proposed FDN is to reduce the phenomenon of feature redundancy by explicitly decomposing features into task-specific features and task-shared features with carefully designed constraints. Experimental results show that our proposed FDN can outperform the state-of-the-art (SOTA) methods by a noticeable margin on Ali-CCP.

AAAI Conference 2023 Conference Paper

NuWLS: Improving Local Search for (Weighted) Partial MaxSAT by New Weighting Techniques

• Yi Chu
• Shaowei Cai
• Chuan Luo

Maximum Satisfiability (MaxSAT) is a prototypical constraint optimization problem, and its generalized version is the (Weighted) Partial MaxSAT problem, denoted as (W)PMS, which deals with hard and soft clauses. Considerable progress has been made on stochastic local search (SLS) algorithms for solving (W)PMS, which mainly focus on clause weighting techniques. In this work, we identify two issues of existing clause weighting techniques for (W)PMS, and propose two ideas correspondingly. First, we observe that the initial values of soft clause weights have a big effect on the performance of the SLS solver for solving (W)PMS, and propose a weight initialization method. Second, we propose a new clause weighting scheme that for the first time employs different conditions for updating hard and soft clause weights. Based on these two ideas, we develop a new SLS solver for (W)PMS named NuWLS. Through extensive experiments, NuWLS performs much better than existing SLS solvers on all 6 benchmarks from the incomplete tracks of MaxSAT Evaluations (MSEs) 2019, 2020, and 2021. In terms of the number of winning instances, NuWLS outperforms state-of-the-art SAT-based incomplete solvers on all the 6 benchmarks. More encouragingly, a hybrid solver that combines NuWLS and an SAT-based solver won all four categories in the incomplete track of the MaxSAT Evaluation 2022.

IJCAI Conference 2022 Conference Paper

T-SMOTE: Temporal-oriented Synthetic Minority Oversampling Technique for Imbalanced Time Series Classification

• Pu Zhao
• Chuan Luo
• Bo Qiao
• Lu Wang
• Saravan Rajmohan
• Qingwei Lin
• Dongmei Zhang

Time series classification is a popular and important topic in machine learning, and it suffers from the class imbalance problem in many real-world applications. In this paper, to address the class imbalance problem, we propose a novel and practical oversampling method named T-SMOTE, which can make full use of the temporal information of time-series data. In particular, for each sample of minority class, T-SMOTE generates multiple samples that are close to class border. Then, based on those samples near class border, T-SMOTE synthesizes more samples. Finally, a weighted sampling method is called on both generated samples near class border and synthetic samples. Extensive experiments on a diverse set of both univariate and multivariate time-series datasets demonstrate that T-SMOTE consistently outperforms the current state-of-the-art methods on imbalanced time series classification. More encouragingly, our empirical evaluations show that T-SMOTE performs better in the scenario of early prediction, an important application scenario in industry, which indicates that T-SMOTE could bring benefits in practice.

IJCAI Conference 2021 Conference Paper

A Runtime Analysis of Typical Decomposition Approaches in MOEA/D Framework for Many-objective Optimization Problems

• Zhengxin Huang
• Yuren Zhou
• Chuan Luo
• Qingwei Lin

Decomposition approach is an important component in multi-objective evolutionary algorithm based on decomposition (MOEA/D), which is a popular method for handing many-objective optimization problems (MaOPs). This paper presents a theoretical analysis on the convergence ability of using the typical weighted sum (WS), Tchebycheff (TCH) or penalty-based boundary intersection (PBI) approach in a basic MOEA/D for solving two benchmark MaOPs. The results show that using WS, the algorithm can always find an optimal solution for any subproblem in polynomial expected runtime. In contrast, the algorithm needs at least exponential expected runtime for some subproblems if using TCH or PBI. Moreover, our analyses discover an obvious shortcoming of using WS, that is, the optimal solutions of different subproblems are easily corresponding to the same solution. In addition, this analysis indicates that if using PBI, a small value of the penalty parameter is a good choice for faster converging to the Pareto front, but it may lose the diversity. This study reveals some optimization behaviors of using three typical decomposition approaches in the well-known MOEA/D framework for solving MaOPs.

NeurIPS Conference 2021 Conference Paper

A Surrogate Objective Framework for Prediction+Programming with Soft Constraints

• Kai Yan
• Jie Yan
• Chuan Luo
• Liting Chen
• Qingwei Lin
• Dongmei Zhang

Prediction+optimization is a common real-world paradigm where we have to predict problem parameters before solving the optimization problem. However, the criteria by which the prediction model is trained are often inconsistent with the goal of the downstream optimization problem. Recently, decision-focused prediction approaches, such as SPO+ and direct optimization, have been proposed to fill this gap. However, they cannot directly handle the soft constraints with the max operator required in many real-world objectives. This paper proposes a novel analytically differentiable surrogate objective framework for real-world linear and semi-definite negative quadratic programming problems with soft linear and non-negative hard constraints. This framework gives the theoretical bounds on constraints’ multipliers, and derives the closed-form solution with respect to predictive parameters and thus gradients for any variable in the problem. We evaluate our method in three applications extended with soft constraints: synthetic linear programming, portfolio optimization, and resource provisioning, demonstrating that our method outperforms traditional two-staged methods and other decision-focused approaches

JBHI Journal 2021 Journal Article

Attention-Guided Deep Neural Network With Multi-Scale Feature Fusion for Liver Vessel Segmentation

• Qingsen Yan
• Bo Wang
• Wei Zhang
• Chuan Luo
• Wei Xu
• Zhengqing Xu
• Yanning Zhang
• Qinfeng Shi

Liver vessel segmentation is fast becoming a key instrument in the diagnosis and surgical planning of liver diseases. In clinical practice, liver vessels are normally manual annotated by clinicians on each slice of CT images, which is extremely laborious. Several deep learning methods exist for liver vessel segmentation, however, promoting the performance of segmentation remains a major challenge due to the large variations and complex structure of liver vessels. Previous methods mainly using existing UNet architecture, but not all features of the encoder are useful for segmentation and some even cause interferences. To overcome this problem, we propose a novel deep neural network for liver vessel segmentation, called LVSNet, which employs special designs to obtain the accurate structure of the liver vessel. Specifically, we design Attention-Guided Concatenation (AGC) module to adaptively select the useful context features from low-level features guided by high-level features. The proposed AGC module focuses on capturing rich complemented information to obtain more details. In addition, we introduce an innovative multi-scale fusion block by constructing hierarchical residual-like connections within one single residual block, which is of great importance for effectively linking the local blood vessel fragments together. Furthermore, we construct a new dataset containing 40 thin thickness cases (0. 625 mm) which consist of CT volumes and annotated vessels. To evaluate the effectiveness of the method with minor vessels, we also propose an automatic stratification method to split major and minor liver vessels. Extensive experimental results demonstrate that the proposed LVSNet outperforms previous methods on liver vessel segmentation datasets. Additionally, we conduct a series of ablation studies that comprehensively support the superiority of the underlying concepts.

AAAI Conference 2021 Conference Paper

Correlation-Aware Heuristic Search for Intelligent Virtual Machine Provisioning in Cloud Systems

• Chuan Luo
• Bo Qiao
• Wenqian Xing
• Xin Chen
• Pu Zhao
• Chao Du
• Randolph Yao
• Hongyu Zhang

The optimization of resource is crucial for the operation of public cloud systems such as Microsoft Azure, as well as servers dedicated to the workloads of large customers such as Microsoft 365. Those optimization tasks often need to take unknown parameters into consideration and can be formulated as Prediction+Optimization problems. This paper proposes a new Prediction+Optimization method named Correlation-Aware Heuristic Search (CAHS) that is capable of accounting for the uncertainty in unknown parameters and delivering effective solutions to difficult optimization problems. We apply this method to solving the predictive virtual machine (VM) provisioning (PreVMP) problem, where the VM provisioning plans are optimized based on the predicted demands of different VM types, to ensure rapid provisions upon customers’ requests and to pursue high resource utilization. Unlike the current state-of-the-art PreVMP approaches that assume independence among the demands for different VM types, CAHS incorporates demand correlation when conducting prediction and optimization in a novel and effective way. Our experiments on two public benchmarks and one industrial benchmark demonstrate that CAHS can achieve better performance than its nine state-of-the-art competitors. CAHS has been successfully deployed in Microsoft Azure and significantly improved its performance. The main ideas of CAHS have also been leveraged to improve the efficiency and the reliability of the cloud services provided by Microsoft 365.

IJCAI Conference 2021 Conference Paper

Predictive Job Scheduling under Uncertain Constraints in Cloud Computing

• Hang Dong
• Boshi Wang
• Bo Qiao
• Wenqian Xing
• Chuan Luo
• Si Qin
• Qingwei Lin
• Dongmei Zhang

Capacity management has always been a great challenge for cloud platforms due to massive, heterogeneous on-demand instances running at different times. To better plan the capacity for the whole platform, a class of cloud computing instances have been released to collect computing demands beforehand. To use such instances, users are allowed to submit jobs to run for a pre-specified uninterrupted duration in a flexible range of time in the future with a discount compared to the normal on-demand instances. Proactively scheduling those pre-collected job requests considering the capacity status over the platform can greatly help balance the computing workloads along time. In this work, we formulate the scheduling problem for these pre-collected job requests under uncertain available capacity as a Prediction + Optimization problem with uncertainty in constraints, and propose an effective algorithm called Controlling under Uncertain Constraints (CUC), where the predicted capacity guides the optimization of job scheduling and job scheduling results are leveraged to improve the prediction of capacity through Bayesian optimization. The proposed formulation and solution are commonly applicable for proactively scheduling problems in cloud computing. Our extensive experiments on three public, industrial datasets shows that CUC has great potential for supporting high reliability in cloud platforms.

AAAI Conference 2021 Conference Paper

PULNS: Positive-Unlabeled Learning with Effective Negative Sample Selector

• Chuan Luo
• Pu Zhao
• Chen Chen
• Bo Qiao
• Chao Du
• Hongyu Zhang
• Wei Wu
• Shaowei Cai

Positive-unlabeled learning (PU learning) is an important case of binary classification where the training data only contains positive and unlabeled samples. The current stateof-the-art approach for PU learning is the cost-sensitive approach, which casts PU learning as a cost-sensitive classification problem and relies on unbiased risk estimator for correcting the bias introduced by the unlabeled samples. However, this approach requires the knowledge of class prior and is subject to the potential label noise. In this paper, we propose a novel PU learning approach dubbed PULNS, equipped with an effective negative sample selector, which is optimized by reinforcement learning. Our PULNS approach employs an effective negative sample selector as the agent responsible for selecting negative samples from the unlabeled data. While the selected, likely negative samples can be used to improve the classifier, the performance of classifier is also used as the reward to improve the selector through the REINFORCE algorithm. By alternating the updates of the selector and the classifier, the performance of both is improved. Extensive experimental studies on 7 real-world application benchmarks demonstrate that PULNS consistently outperforms the current state-of-the-art methods in PU learning, and our experimental results also confirm the effectiveness of the negative sample selector underlying PULNS.

IJCAI Conference 2020 Conference Paper

Extended Conjunctive Normal Form and An Efficient Algorithm for Cardinality Constraints

• Zhendong Lei
• Shaowei Cai
• Chuan Luo

Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) are two basic and important constraint problems with many important applications. SAT and MaxSAT are expressed in CNF, which is difficult to deal with cardinality constraints. In this paper, we introduce Extended Conjunctive Normal Form (ECNF), which expresses cardinality constraints straightforward and does not need auxiliary variables or clauses. Then, we develop a simple and efficient local search solver LS-ECNF with a well designed scoring function under ECNF. We also develop a generalized Unit Propagation (UP) based algorithm to generate the initial solution for local search. We encode instances from Nurse Rostering and Discrete Tomography Problems into CNF with three different cardinality constraint encodings and ECNF respectively. Experimental results show that LS-ECNF has much better performance than state of the art MaxSAT, SAT, Pseudo-Boolean and ILP solvers, which indicates solving cardinality constraints with ECNF is promising.

IJCAI Conference 2020 Conference Paper

Intelligent Virtual Machine Provisioning in Cloud Computing

• Chuan Luo
• Bo Qiao
• Xin Chen
• Pu Zhao
• Randolph Yao
• Hongyu Zhang
• Wei Wu
• Andrew Zhou

Virtual machine (VM) provisioning is a common and critical problem in cloud computing. In industrial cloud platforms, there are a huge number of VMs provisioned per day. Due to the complexity and resource constraints, it needs to be carefully optimized to make cloud platforms effectively utilize the resources. Moreover, in practice, provisioning a VM from scratch requires fairly long time, which would degrade the customer experience. Hence, it is advisable to provision VMs ahead for upcoming demands. In this work, we formulate the practical scenario as the predictive VM provisioning (PreVMP) problem, where upcoming demands are unknown and need to be predicted in advance, and then the VM provisioning plan is optimized based on the predicted demands. Further, we propose Uncertainty-Aware Heuristic Search (UAHS) for solving the PreVMP problem. UAHS first models the prediction uncertainty, and then utilizes the prediction uncertainty in optimization. Moreover, UAHS leverages Bayesian optimization to interact prediction and optimization to improve its practical performance. Extensive experiments show that UAHS performs much better than state-of-the-art competitors on two public datasets and an industrial dataset. UAHS has been successfully applied in Microsoft Azure and brought practical benefits in real-world applications.

IJCAI Conference 2020 Conference Paper

Two-goal Local Search and Inference Rules for Minimum Dominating Set

• Shaowei Cai
• Wenying Hou
• Yiyuan Wang
• Chuan Luo
• Qingwei Lin

Minimum dominating set (MinDS) is a canonical NP-hard combinatorial optimization problem with applications. For large and hard instances one must resort to heuristic approaches to obtain good solutions within reasonable time. This paper develops an efficient local search algorithm for MinDS, which has two main ideas. The first one is a novel local search framework, while the second is a construction procedure with inference rules. Our algorithm named FastDS is evaluated on 4 standard benchmarks and 3 massive graphs benchmarks. FastDS obtains the best performance for almost all benchmarks, and obtains better solutions than state-of-the-art algorithms on massive graphs.

IJCAI Conference 2019 Conference Paper

Local Search with Efficient Automatic Configuration for Minimum Vertex Cover

• Chuan Luo
• Holger H. Hoos
• Shaowei Cai
• Qingwei Lin
• Hongyu Zhang
• Dongmei Zhang

Minimum vertex cover (MinVC) is a prominent NP-hard problem in artificial intelligence, with considerable importance in applications. Local search solvers define the state of the art in solving MinVC. However, there is no single MinVC solver that works best across all types of MinVC instances, and finding the most suitable solver for a given application poses considerable challenges. In this work, we present a new local search framework for MinVC called MetaVC, which is highly parametric and incorporates many effective local search techniques. Using an automatic algorithm configurator, the performance of MetaVC can be optimized for particular types of MinVC instances. Through extensive experiments, we demonstrate that MetaVC significantly outperforms previous solvers on medium-size hard MinVC instances, and shows competitive performance on large MinVC instances. We further introduce a neural-network-based approach for enhancing the automatic configuration process, by identifying and terminating unpromising configuration runs. Our results demonstrate that MetaVC, when automatically configured using this method, can achieve improvements in the best known solutions for 16 large MinVC instances.

IJCAI Conference 2017 Conference Paper

A Reduction based Method for Coloring Very Large Graphs

• Jinkun Lin
• Shaowei Cai
• Chuan Luo
• Kaile Su

The graph coloring problem (GCP) is one of the most studied NP hard problems and has numerous applications. Despite the practical importance of GCP, there are limited works in solving GCP for very large graphs. This paper explores techniques for solving GCP on very large real world graphs. We first propose a reduction rule for GCP, which is based on a novel concept called degree bounded independent set. The rule is iteratively executed by interleaving between lower bound computation and graph reduction. Based on this rule, we develop a novel method called FastColor, which also exploits fast clique and coloring heuristics. We carry out experiments to compare our method FastColor with two best algorithms for coloring large graphs we could find. Experiments on a broad range of real world large graphs show the superiority of our method. Additionally, our method maintains both upper bound and lower bound on the optimal solution, and thus it proves an optimal solution when the upper bound meets the lower bound. In our experiments, it proves the optimal solution for 97 out of 142 instances.

AIJ Journal 2017 Journal Article

CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability

• Chuan Luo
• Shaowei Cai
• Kaile Su
• Wenxuan Huang

Weighted maximum satisfiability and (unweighted) partial maximum satisfiability (PMS) are two significant generalizations of maximum satisfiability (MAX-SAT), and weighted partial maximum satisfiability (WPMS) is the combination of the two, with more important applications in practice. Recently, great breakthroughs have been made on stochastic local search (SLS) for weighted MAX-SAT and PMS, resulting in several state-of-the-art SLS algorithms CCLS, Dist and DistUP. However, compared to the great progress of SLS on weighted MAX-SAT and PMS, the performance of SLS on WPMS lags far behind. In this paper, we present a new SLS algorithm named CCEHC for WPMS. CCEHC employs an extended framework of CCLS with a heuristic emphasizing hard clauses, called EHC. With strong accents on hard clauses, EHC 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. Extensive experiments demonstrate that CCEHC significantly outperforms its state-of-the-art SLS competitors. Further experimental results on comparing CCEHC with a state-of-the-art complete solver show the effectiveness of CCEHC on a number of application WPMS instances, and indicate that CCEHC might be beneficial in practice. Also, empirical analyses confirm the effectiveness of each component underlying the EHC heuristic.

IJCAI Conference 2017 Conference Paper

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

• Chuan Luo
• Shaowei Cai
• Kaile Su
• Wenxuan Huang

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.

JAIR Journal 2017 Journal Article

Finding A Small Vertex Cover in Massive Sparse Graphs: Construct, Local Search, and Preprocess

• Shaowei Cai
• Jinkun Lin
• Chuan Luo

The problem of finding a minimum vertex cover (MinVC) in a graph is a well known NP-hard combinatorial optimization problem of great importance in theory and practice. Due to its NP-hardness, there has been much interest in developing heuristic algorithms for finding a small vertex cover in reasonable time. Previously, heuristic algorithms for MinVC have focused on solving graphs of relatively small size, and they are not suitable for solving massive graphs as they usually have high-complexity heuristics. This paper explores techniques for solving MinVC in very large scale real-world graphs, including a construction algorithm, a local search algorithm and a preprocessing algorithm. Both the construction and search algorithms are based on low-complexity heuristics, and we combine them to develop a heuristic algorithm for MinVC called FastVC. Experimental results on a broad range of real-world massive graphs show that, our algorithms are very fast and have better performance than previous heuristic algorithms for MinVC. We also develop a preprocessing algorithm to simplify graphs for MinVC algorithms. By applying the preprocessing algorithm to local search algorithms, we obtain two efficient MinVC solvers called NuMVC2+p and FastVC2+p, which show further improvement on the massive graphs.

IJCAI Conference 2017 Conference Paper

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

• Shaowei Cai
• Chuan Luo
• Haochen Zhang

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.

AIJ Journal 2016 Journal Article

New local search methods for partial MaxSAT

• Shaowei Cai
• Chuan Luo
• Jinkun Lin
• Kaile Su

Maximum Satisfiability (MaxSAT) is the optimization version of the Satisfiability (SAT) problem. Partial Maximum Satisfiability (PMS) is a generalization of MaxSAT which involves hard and soft clauses and has important real world applications. Local search is a popular approach to solving SAT and MaxSAT and has witnessed great success in these two problems. However, unfortunately, local search algorithms for PMS do not benefit much from local search techniques for SAT and MaxSAT, mainly due to the fact that it contains both hard and soft clauses. This feature makes it more challenging to design efficient local search algorithms for PMS, which is likely the reason of the stagnation of this direction in more than one decade. In this paper, we propose a number of new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. The first three ideas, including weighting for hard clauses, separating hard and soft score, and a variable selection heuristic based on hard and soft score, are used to develop a local search algorithm for PMS called Dist. The fourth idea, which uses unit propagation with priority on hard unit clauses to generate the initial assignment, is used to improve Dist on industrial instances, leading to the DistUP algorithm. The effectiveness of our solvers and ideas is illustrated through experimental evaluations on all PMS benchmarks from the MaxSAT Evaluation 2014. According to our experimental results, Dist shows a significant improvement over previous local search solvers on all benchmarks. We also compare our solvers with state-of-the-art complete PMS solvers and a state-of-the-art portfolio solver, and the results show that our solvers have better performance in random and crafted instances but worse in industrial instances. The good performance of Dist has also been confirmed by the fact that Dist won all random and crafted categories of PMS and Weighted PMS in the incomplete solvers track of the MaxSAT Evaluation 2014.

AAAI Conference 2014 Conference Paper

Double Configuration Checking in Stochastic Local Search for Satisfiability

• Chuan Luo
• Shaowei Cai
• Wei Wu
• Kaile Su

Stochastic local search (SLS) algorithms have shown effectiveness on satisfiable instances of the Boolean satisfiability (SAT) problem. However, their performance is still unsatisfactory on random k-SAT at the phase transition, which is of significance and is one of the empirically hardest distributions of SAT instances. In this paper, we propose a new heuristic called DCCA, which combines two configuration checking (CC) strategies with different definitions of configuration in a novel way. We use the DCCA heuristic to design an efficient SLS solver for SAT dubbed DCCASat. The experiments show that the DCCASat solver significantly outperforms a number of state-of-the-art solvers on extensive random k-SAT benchmarks at the phase transition. Moreover, DCCASat shows good performance on structured benchmarks, and a combination of DCCASat with a complete solver achieves state-of-the-art performance on structured benchmarks.

AAAI Conference 2014 Conference Paper

Tailoring Local Search for Partial MaxSAT

• Shaowei Cai
• Chuan Luo
• John Thornton
• Kaile Su

Partial MaxSAT (PMS) is a generalization to SAT and MaxSAT. Many real world problems can be encoded into PMS in a more natural and compact way than SAT and MaxSAT. In this paper, we propose new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. We use these ideas to develop a local search PMS algorithm called Dist. Experimental results on PMS benchmarks from MaxSAT Evaluation 2013 show that Dist significantly outperforms state-of-the-art PMS algorithms, including both local search algorithms and complete ones, on random and crafted benchmarks. For the industrial benchmark, Dist dramatically outperforms previous local search algorithms and is comparable with complete algorithms.

AAAI Conference 2013 Conference Paper

Improving WalkSAT for Random k-Satisfiability Problem with k > 3

• Shaowei Cai
• Kaile Su
• Chuan Luo

Stochastic local search (SLS) algorithms are well known for their ability to efficiently find models of random instances of the Boolean satisfiablity (SAT) problem. One of the most famous SLS algorithms for SAT is WalkSAT, which is an initial algorithm that has wide influence among modern SLS algorithms. Recently, there has been increasing interest in WalkSAT, due to the discovery of its great power on large random 3-SAT instances. However, the performance of WalkSAT on random k-SAT instances with k > 3 lags far behind. Indeed, there have been few works in improving SLS algorithms for such instances. This work takes a large step towards this direction. We propose a novel concept namely multilevel make. Based on this concept, we design a scoring function called linear make, which is utilized to break ties in WalkSAT, leading to a new algorithm called WalkSATlm. Our experimental results on random 5- SAT and 7-SAT instances show that WalkSATlm improves WalkSAT by orders of magnitudes. Moreover, WalkSATlm significantly outperforms state-of-the-art SLS solvers on random 5-SAT instances, while competes well on random 7-SAT ones. Additionally, WalkSATlm performs very well on random instances from SAT Challenge 2012, indicating its robustness.