Abstract Satisfiability Modulo Theories (SMT) solvers are widely used in formal verification. In program analysis, users often encounter queries that differ only by simple syntactic mutations and are logically equivalent. These mutations typically include assertion reordering, symbol renaming, anti-symmetric relation inversion, and commutative operand reordering. However, such minor changes can cause runtimes to vary by orders of magnitude. This variability reduces the predictability required for industrial-scale verification and remains a critical challenge. This paper presents SMTStabilizer, a tool that improves the stability of SMT solvers via context-driven normalization. Since complete input normalization is as hard as the graph isomorphism problem, SMTStabilizer adopts an approximate normalization strategy to avoid the high cost of exact normalization. The framework converts formulas into a structured representation and propagates structural information across nodes, enabling each node to capture its surrounding context. Using this context information, SMTStabilizer derives a consistent ordering over subformulas. This process yields a nearly canonical form that remains consistent across isomorphic inputs. SMTStabilizer also leverages pruning techniques that exploit the syntactic structure of SMT formulas to reduce normalization time. Evaluation on millions of queries using Z3 and cvc5 shows that SMTStabilizer improves solver stability to over $$98\%$$ 98 % under 10 random mutations.

Abstract Combinational equivalence checking (CEC) remains a challenge EDA task in the formal verification of datapath circuits due to their complex arithmetic structures and the limited capability or scalability of SAT, BDD, and exact-simulation (ES) based techniques when used independently. This work presents FastLEC , a hybrid prover that unifies these three formal reasoning engines and introduces three strategies that substantially enhance verification efficiency. First, a regression-based engine-scheduling heuristic predicts solver effectiveness, enabling more accurate and balanced allocation of computational resources. Second, datapath-structure-aware partitioning strategies, along with a dynamic divide-and-conquer SAT prover, exploit the regularity of arithmetic designs while preserving completeness. Third, the memory overhead of ES is significantly reduced through address-reference-count tracking, and simulation is further accelerated through a GPU-enabled backend. FastLEC is evaluated across 368 datapath circuits. Using 32 CPU cores, it proves 5.07 $$\times $$ × more circuits than the widely used ABC &cec tool. Compared with the latest best datapath-oriented serial and parallel CEC provers, FastLEC outperforms them by 3.33 $$\times $$ × and 2.67 $$\times $$ × in PAR-2 time, demonstrating an improvement of 74 newly solved circuits. With the addition of a single GPU, it achieves a further 4.07 $$\times $$ × improvement. The prover also demonstrates excellent scalability.

Background: Conflict-Driven Clause Learning (CDCL) is a dominant framework for solving the Satisfiability problem (SAT). Modern CDCL solvers rely heavily on various heuristics, which significantly influence their performance. Established solvers such as MiniSat and Kissat typically incorporate multiple heuristics and therefore require substantial manual effort and domain expertise for fine-tuning in practice. Objectives: The emergence of Large Language Models (LLMs) offers a promising opportunity to automate SAT solver optimization. However, generating a complete CDCL solver from scratch using LLMs is impractical due to the complexity and large context volume of modern SAT solvers. To address this challenge, we propose AutoSAT, a framework that automatically optimizes heuristics within a CDCL solver, EasySAT. Our goal is to leverage LLMs to discover effective heuristic designs beyond conventional parameter tuning. Methods: Unlike traditional automated algorithm design approaches that mainly focus on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics for CDCL solvers. In this first attempt to leverage LLMs for SAT solver optimization, we integrate several search strategies, including the greedy hill climber and the (1 + 1) Evolutionary Algorithm, to guide LLMs in searching for better heuristics. Results: Experimental results demonstrate that LLMs can consistently enhance the performance of CDCL solvers. Empirically, AutoSAT outperforms MiniSat and its parameter-tuning variants on 12 of the 19 test datasets, and even surpasses the state-of-the-art hybrid solver Kissat and its parameter-tuning variants on 4 datasets. Conclusions: These results suggest that LLMs can serve as effective agents for automatically improving SAT solver heuristics. AutoSAT provides an initial step toward automated heuristic discovery for CDCL solvers, showing the potential of LLM-based methods to complement and reduce the manual expertise traditionally required in SAT solver design.

Combinational equivalence checking (CEC) is essential for verifying the correctness of circuit designs. With the growing complexity of circuits, effective verification techniques have become increasingly critical. Recently, a conjunctive normal form (CNF)-based approach, converting circuits to CNF for Boolean satisfiability (SAT) solvers, has shown competitive performance compared to state-of-the-art hybrid SAT sweeping approaches. The capability of this CNF-based approach depends on effective CNF conversion. This work presentsCirOPT, which is the first CNF conversion method using compiler optimization to equivalently simplify circuits. Extensive experiments are conducted on a broad range of real-world benchmarks, which are far more than the number of benchmarks typically used in empirical studies. The results reveal that, when paired with the state-of-the-art CNF SAT solverKissat,CirOPTconsiderably outperforms existing approaches in CEC.

Synthesizing circuits to achieve better PPA is crucial, particularly in datapath netlists with various arithmetic operators. The verification relies on the Combinational Equivalence Checking (CEC) techniques, checking the equivalence of two combinational circuits. Contemporary CEC tools commonly utilize SAT as the principal reasoning engine, employing a SAT-sweeping algorithm, which sequentially confirms the equivalence of internal pairs in topological order, merging verified equivalents to reduce the netlist’s scale. Nonetheless, datapath circuits frequently comprise pairs of nodes characterized by relatively limited transitive fan-in cones, yet these nodes display a pronounced density of XOR chains. This particular arrangement presents considerable obstacles for SAT solvers. To address this, exact probability-based simulation (EPS) provides an effective solution, but its high memory requirements limit its applicability. This article proposes a hybrid CEC prover, hybridCEC , and its parallel version, paraHCEC . Firstly, we decrease the memory requirements of the EPS method and integrate it into the SAT-sweeping framework. Secondly, we propose a dynamic engine selection heuristic for SAT and EPS, based on XOR chain density. Thirdly, we improve efficiency by identifying and reducing redundant engine calls by detecting regularity in the circuits. Finally, we parallelize the internal SAT and EPS engines, resulting in a highly efficient parallel CEC prover. Extensive experiments on industrial datapath circuit benchmarks demonstrate that our method significantly outperforms the state-of-the-art prover ABC “&cec”, achieving up to 100× speedups on 40% of instances and over 1000× speedups on 14%. Moreover, our 64-thread parallel version achieved an impressive 70× speedup, highlighting its scalability and effectiveness.

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.

In automatic test pattern generation (ATPG), SAT-based methods are typically used to complement structural approaches, especially for addressing hard-to-detect faults. However, as the size and complexity of circuits grow, SAT-based ATPG faces challenges like pattern inflation and excessive runtime, limiting its overall performance. The key problem lies in the fact that current mainstream SAT solvers perform complete assignments for all primary inputs of the fault’s transitive fanin cone without considering the detection of other faults, making test compaction extremely difficult and time consuming. In this paper, a novel SAT solver PA-MiniSat is proposed, which is capable of generating partial assignments for solving variables and significantly reduces the number of specified bits in test cubes. As an extension of MiniSat, it employs a full-literal watching technique and a circuit-adapted heuristic branching strategy, achieving overall improved performance in ATPG. Based on PA-MiniSat, a hybrid ATPG framework PastATPG is proposed for better test compaction, which tightly integrates structural algorithms with the SAT solver into the unified test compaction flow. Experimental results demonstrate that our method outperforms other SAT solvers in pattern compaction and, in some cases, even surpasses commercial ATPG tools in terms of speed. The code is available at https://github.com/sklp-eda-lab/PastATPG.

In modern digital circuit design, verifying the equivalence of arithmetic circuits is a significant and challenging task. This paper introduces a new circuit solver based on the Conflict-Driven Clause Learning (CDCL) algorithm, which integrates structural elimination techniques to reduce the number of variables and clauses while maintaining the circuit structure. Additionally, branching heuristics have been enhanced specifically for the structure of arithmetic circuits. Experimental results demonstrate that X-SAT significantly outperforms best previous circuit solver could be found on all benchmarks. Further, X-SAT performs better than the state-of-the-art CNF-based SAT solvers on complex arithmetic circuits, underscoring its significant potential in the field of circuit design verification.

Combinational Equivalence Checking (CEC) is a crucial technique in electronic design automation for verifying the functional equivalence of combinational circuits. Recently, combinational circuit design increasingly incorporates more complex arithmetic structures, commonly known as datapath circuits. However, existing state-of-the-art tools often exhibit subpar performance in solving datapath CEC problems. To further advance the exploration on datapath CEC process, this study introduces PDP-CEC (Parallel Dynamic Partitioning Combinational Equivalence Checking), a novel parallel CEC approach integrating circuit partitioning and dynamic task scheduling into the CEC process, enhancing the efficiency of CEC for datapath circuits. PDP-CEC introduces an innovative method for selecting critical nodes to split the search space of the CEC problem, facilitating the efficient generation of numerous independent subproblems. Meanwhile, a dynamic task scheduling strategy is implemented in PDP-CEC to ensure load balancing and prevent hard-to-solve subproblems from stalling the entire process. Compared to the most advanced tools such as ABC and HybridCEC, PDP-CEC significantly accelerates CEC process, achieving speedups ranging from $5.11 x$ to $125.27 x$, while effectively solving approximately three times more datapath CEC problems. With excellent scalability, PDP-CEC shows substantial improvements in combinational equivalence checking for datapath circuits, offering an efficient parallel approach to meet the demands of large-scale datapath CEC tasks.

IC3 and its variants are SAT-based model-checking methods that play a critical role in hardware verification. Efficient management of proof obligations, which track states that need to be proven unreachable, is essential for improving verification performance. This paper presents a novel approach that utilizes Critical Proof Obligations (CPOs) to improve proof obligation management. We propose two techniques, CPO-Driven UNSAT Core Generation and CPO-Driven Proof Obligation Propagation, to promote lemma propagation and frame refinement. Experimental results on HWMCC benchmarks demonstrate significant improvements in CPO discovery and lemma propagation, resulting in notable performance gains.

VeriSAT is the first modern SAT solver implemented entirely in synthesizable SystemVerilog, leveraging FPGA architecture for hardware acceleration. This paper introduces the design of VeriSAT, focusing on hardware-specific optimizations that significantly improve performance over traditional software-based solvers. By rethinking key SAT components for hardware, VeriSAT introduces custom data structures and parallelized processes to accelerate solving efficiency.Central to VeriSAT's architecture are hardware-optimized data structures. A linked-list based literal-watching mechanism, enhanced with cached watching literals, reduces latency in unit propagation. Additionally, a concurrent propagation tree enables simultaneous traversal for faster conflict detection. The solver's pipelined clause learning further boosts throughput, allowing rapid conflict analysis without compromising performance.Extensive benchmarking demonstrates that VeriSAT outperforms two other FPGA-based solvers, SAT-Hard and SAT-Accel, by a factor of 1044x and is 18x faster, respectively, on curated benchmark instances. Additionally, VeriSAT shows a 30x speedup over the popular CPU-based MiniSat solver for specific datasets, validating the effectiveness of our design optimizations.VeriSAT represents a significant leap forward in FPGA-based SAT solving, offering unprecedented efficiency through its hardware-tailored design. This work lays the foundation for future advancements in hardware-accelerated SAT solvers and paves the way for more scalable, high-performance solutions in both academic and industrial applications.

The maximum satisfiability problem (MaxSAT) is a crucial combinatorial optimization problem with widespread applications across various critical domains. This paper presents CASHWMaxSAT, an efficient core-guided MaxSAT solver based on two novel ideas. The first and most important idea is the introduction of an extended stratification technique that progressively focuses on solving high-weight soft clauses. Second, we integrate disjoint unsatisfiable cores with the goal of minimizing the unsatisfiable core, allowing the solver to learn multiple high-quality clauses in a single conflict analysis step. These innovations enable our MaxSAT solver to efficiently identify key constraints and reduce redundant reasoning, significantly enhancing solving efficiency. Experimental results on benchmarks from the complete weighted track of the MaxSAT Evaluations 2022-2024 demonstrate that the proposed methods lead to substantial improvements, with CASHWMaxSAT outperforming state-of-the-art MaxSAT solvers across all benchmarks. Additionally, it enabled us to achieve the top two positions in the exact weighted category of the MaxSAT Evaluation 2024.

Satisfiability Modulo Theories (SMT) plays a critical role in various software engineering applications, including program verification, symbolic execution, and automated test generation. Over the years, a wide range of SMT solvers has been developed, typically designed for general purposes or tailored to specific background theories, such as bit-vectors or nonlinear arithmetic. Due to the diversity and complexity of SMT instances, no single solver consistently outperforms others across all problem domains. This motivates the need for algorithm selection strategies that can adaptively choose solvers based on the characteristics of the instances.To overcome the limitations of single-solver selection, solving SMT as a scheduling problem, enabling a more fault-tolerant and effective use of multiple solvers in sequence. We model algorithm scheduling as a hyperparameter optimization problem, enabling efficient black-box search over solver sequences while treating the dataset as a whole, thus achieving globally optimized and robust scheduling strategies. The resulting scheduler called SMTgazer. To further enhance scheduling efficiency and solver performance, we propose two optimizations: leveraging unsupervised X-means clustering to create semantically coherent instance groups for localized model training, and augmenting the Bayesian optimization surrogate with boosting and bagging ensembles to improve generalization and mitigate overfitting, thereby yielding more reliable performance predictions for the sequential portfolio scheduler.Extensive experiments are conducted to evaluate the performance of SMTgazer, utilizing six SMT benchmarks derived from real-world applications. It shows that our approach consistently outperforms current state-of-the-art methods. Particularly, SMTgazer achieves a 44.65% reduction in PAR-2 score and 69.11% decrease in the number of unsolved instances, compared to the strongest competitor, Sibyl, demonstrating the effectiveness of formulating SMT algorithm scheduling as a hyperparameter optimization problem. We further analyze the generated scheduling sequences to uncover the design principles that explain the success of our method. Finally, we also empirically show that our approach is both robust and generalizable, and the proposed strategies are effective.

Pseudo-Boolean optimization (PBO) is usually used to model combinatorial optimization problems, especially for some real-world applications. Despite its significant importance in both theory and applications, the performance of current PBO solvers is still limited. This paper develops a novel local search algorithm for PBO, which has four main ideas. First, we design a new primary scoring function and a two-level selection strategy to evaluate all candidate variables. Second, we introduce a new weighting scheme to accurately guide the search process toward more promising directions. Third, we propose a novel deep optimization strategy to disturb some search processes. Fourth, an efficient solution space exploration mechanism is applied to help the algorithm jump out of local optimum. We conduct experiments on a broad range of public benchmarks, including three large-scale practical application benchmarks, two benchmarks from PB competitions, an integer linear programming optimization benchmark, a crafted combinatorial benchmark, and a combinatorial optimization knapsack benchmark to compare our proposed algorithm against twelve state-of-the-art competitors, including seven recently-proposed pure stochastic local search PBO solvers, a non-traditional stochastic local search combined with complete oracle, two complete PB solvers, and two mixed integer programming (MIP) solvers. Our proposed algorithm has been shown to perform best on these three real-world benchmarks. On the other five benchmarks, our algorithm shows competitive performance compared to state-of-the-art competitors, and it significantly outperforms all other local search algorithms, indicating that our algorithm greatly advances the state of the art in local search for solving PBO.

Minimizing the testing cost is crucial in the context of the design for test (DFT) flow. In our observation, the test patterns generated by commercial ATPG tools in test compression mode still contain redundancy. To tackle this obstacle, we propose a post-flow static test compaction method that utilizes a partial fault dictionary instead of a full fault dictionary, and leverages a dedicated Pure-MaxSAT solver to re-compact the test patterns generated by commercial ATPG tools. We also observe that commercial ATPG tools offer a more comprehensive selection of candidate patterns for compaction in the “n-detect” mode, leading to superior compaction efficacy. In experiments on ISCAS89, ITC99, and open-source RISC-V CPU benchmarks, our method achieves an average reduction of 21.58% and a maximum of 29.93% in test cycles evaluated by commercial tools while maintaining fault coverage. Furthermore, our approach demonstrates improved performance compared with existing methods.

Abstract Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers. With the development of computing resources, a promising direction to boost performance is parallel and even distributed SMT solving. We explore this potential in a divide-and-conquer view and propose a novel dynamic parallel framework with variable-level partitioning. To the best of our knowledge, this is the first attempt to perform variable-level partitioning for arithmetic theories. Moreover, we enhance the interval constraint propagation algorithm, coordinate it with Boolean propagation, and integrate it into our variable-level partitioning strategy. Our partitioning algorithm effectively capitalizes on propagation information, enabling efficient formula simplification and search space pruning. We apply our method to three state-of-the-art SMT solvers, namely CVC5, OpenSMT2, and Z3, resulting in efficient parallel SMT solvers. Experiments are carried out on benchmarks of linear and non-linear arithmetic over both real and integer variables, and our variable-level partitioning method shows substantial improvements over previous partitioning strategies and is particularly good at non-linear theories.

Integer linear programming (ILP) models a wide range of practical combinatorial optimization problems and significantly impacts industry and management sectors. This work proposes new characterizations of ILP with the concept of boundary solutions. Motivated by the new characterizations, we develop a new local search algorithm Local-ILP, which is efficient for solving general ILP validated on a large heterogeneous problem dataset. We propose a new local search framework that switches between three modes, namely Search, Improve, and Restore modes. Two new operators are proposed, namely the tight move and the lift move operators, which are associated with appropriate scoring functions. Different modes apply different operators to realize different search strategies and the algorithm switches between three modes according to the current search state. Putting these together, we develop a local search ILP solver called Local-ILP. Experiments conducted on the MIPLIB dataset show the effectiveness of our algorithm in solving large-scale hard ILP problems. In the aspect of finding a good feasible solution quickly, Local-ILP is competitive and complementary to the state-of-the-art commercial solver Gurobi and significantly outperforms the state-of-the-art non-commercial solver SCIP. Moreover, our algorithm establishes new records for 6 MIPLIB open instances. The theoretical analysis of our algorithm is also presented, which shows our algorithm could avoid visiting unnecessary regions.

Abstract MaxSAT modulo theories (MaxSMT) is an important generalization of Satisfiability modulo theories (SMT) with various applications. In this paper, we focus on MaxSMT with the background theory of Linear Integer Arithmetic, denoted as MaxSMT(LIA). We design the first local search algorithm for MaxSMT(LIA) called PairLS, based on the following novel ideas. A novel operator called pairwise operator is proposed for integer variables. It extends the original local search operator by simultaneously operating on two variables, enriching the search space. Moreover, a compensation-based picking heuristic is proposed to determine and distinguish the pairwise operations. Experiments are conducted to evaluate our algorithm on massive benchmarks. The results show that our solver is competitive with state-of-the-art MaxSMT solvers. Furthermore, we also apply the pairwise operation to enhance the local search algorithm of SMT, which shows its extensibility.

Satisfiability Modulo Theory (SMT) generalizes the propositional satisfiability problem (SAT) by extending support for various first-order background theories. In this paper, we focus on the SMT problems in Non-Linear Integer Arithmetic (NIA) theory, referred to as SMT(NIA), which has wide applications in software engineering. The dominant paradigm for SMT(NIA) is the CDCL(T) framework, while recently stochastic local search (SLS) has also shown its effectiveness. However, the cooperation between the two methods has not been studied yet. Motivated by the great success of the deep cooperation of CDCL and SLS for SAT, we propose a two-layer hybrid approach for SMT(NIA). The outer-layer interleaves between the inner-layer and an independent SLS solver. In the inner-layer, we take CDCL(T) as the main body, and design DCL(T)-guided SLS solver, which is invoked at branches corresponding to skeleton solutions and returns useful information to improve the branching heuristics of CDCL(T). We implement our ideas on top of the CDCL(T) tactic of Z3 with an SLS solver called LocalSMT, resulting in a hybrid solver dubbed HybridSMT. Extensive experiments are carried out on the standard SMT(NIA) benchmarks from SMT-LIB, where most of the instances are from real-world software engineering applications of termination and non-termination analysis. Experiment results show that HybridSMT significantly improves the CDCL(T) solver in Z3. Moreover, our solver can solve 10.36% more instances than the currently best SMT(NIA) solver, and is more efficient for software verification instances.

Contemporary systems of Guaranteed Delivery (GD) advertising work with two different stages, namely, the offline selling stage and the online serving stage. The former deals with contract allocation, and the latter fulfills the impression allocation of signed contracts. Existing work usually handles these two stages separately. For example, contracts are formulated offline without concerning practical situations in the online serving stage. Therefore, we address in this paper a bi-objective contract allocation for GD advertising, which maximizes the impressions, i.e., Ad resource assignments, allocated for the new incoming advertising orders, and at the same time, controls the balance in the inventories. Since the proposed problem is high dimensional and heavily constrained, we design an efficient local search that focuses on the two objectives alternatively. The experimental results indicate that our algorithm outperforms multi-objective evolutionary algorithms and Gurobi, the former of which is commonly applied for multi-objective optimization and the latter of which is a well-known competitive commercial tool.

Local search has been widely applied to solve the well-known (weighted) partial MaxSAT problem, significantly influencing many real-world applications. The main difficulty to overcome when designing a local search algorithm is that it can easily fall into local optima. Clause weighting is a beneficial technique that dynamically adjusts the landscape of search space to help the algorithm escape from local optima. Existing works tend to increase the weights of falsified clauses, and such strategies may result in an unpredictable landscape of search space during the optimization process. Therefore, in this paper, we propose a Unified Soft Clause Weighting Scheme called Unified-SW, which increases the weights of all soft clauses in feasible local optima, whether they are satisfied or not, while preserving the hierarchy among them. We implemented Unified-SW in a new local search solver called USW-LS. Experimental results demonstrate that USW-LS, outperforms the state-of-the-art local search solvers across benchmarks from anytime tracks of recent MaxSAT Evaluations. More promisingly, a hybrid solver combining USW-LS and TT-Open-WBO-Inc won all four categories in the anytime track of MaxSAT Evaluation 2023.

The set covering problem (SCP) is a fundamental NP-hard problem in computer science and has a broad range of important real-world applications. In practice, SCP instances transformed from real-world applications would be of large scale, so it is of significant importance to design effective heuristic algorithms, especially local search ones. However, there exist only few research works on developing local search algorithms for solving SCP. In this article, we propose a new local search algorithm for solving SCP, dubbed NuSC. In particular, NuSC introduces a new combined scoring function for subset selection, which combines different subset properties in an effective way and helps NuSC find more optimized solutions. Besides, NuSC incorporates a dynamic weighting scheme for elements, a tabu search strategy, and a novelty selection mechanism to further enhance its practical performance. In order to study the effectiveness and robustness of our proposed NuSC algorithm, we conduct extensive experiments to compare NuSC against many state-of-the-art competitors on various types of SCP instances. Our experimental results demonstrate that NuSC significantly outperforms its competitors on the majority of instances, indicating the superiority of NuSC. Also, our empirical evaluations confirm the effectiveness of each algorithmic technique underlying NuSC.

The paper presents an attempt to bridge the gap between machine learning and symbolic reasoning. We build graph neural networks (GNNs) to predict the solution of the Maximum Satisfiability (MaxSAT) problem, an optimization variant of SAT. Two closely related graph representations are adopted, and we prove their theoretical equivalence. We also show that GNNs can achieve attractive performance to solve hard MaxSAT problems in certain distributions even compared with state-of-the-art solvers through experimental evaluation.

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.

We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. Unlike existing solutions trained on random SAT instances with relatively weak supervision, we propose applying the knowledge of the well-developed electronic design automation (EDA) field for SAT solving. Specifically, we first resort to logic synthesis algorithms to pre-process SAT instances into optimized and-inverter graphs (AIGs). By doing so, the distribution diversity among various SAT instances can be dramatically reduced, which facilitates improving the generalization capability of the learned model. Next, we regard the distribution of SAT solutions being a product of conditional Bernoulli distributions. Based on this observation, we approximate the SAT solving procedure with a conditional generative model, leveraging a novel directed acyclic graph neural network (DAGNN) with two polarity prototypes for conditional SAT modeling. To effectively train the generative model, with the help of logic simulation tools, we obtain the probabilities of nodes in the AIG being logic ‘1’ as rich supervision. We conduct comprehensive experiments on various SAT problems. Our results show that, DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions, especially when generalized to SAT instances that are relatively large or with diverse distributions.

In the application of IC design for microprocessors, there are often demands for optimizing the implementation of datapath circuits, on which various arithmetic operations are performed. Combinational equivalence checking (CEC) plays an essential role in ensuring the correctness of design optimization. The most prevalent CEC algorithms are based on SAT sweeping, which utilizes SAT to prove the equivalence of the internal node pairs in topological order, and the equivalent nodes are merged. Datapath circuits usually contain equivalent pairs for which the transitive fan-in cones are small but have a high XOR chain density, and proving such node pairs is very difficult for SAT solvers. An exact probability-based simulation (EPS) is suitable for verifying such pairs, while this method is not suitable for pairs with many primary inputs due to the memory cost. We first reduce the memory cost of EPS and integrate it to improve the SAT sweeping method. Considering the complementary abilities of SAT and EPS, we design an engine selection heuristic to dynamically choose SAT or EPS in the sweeping process, according to XOR chain density. Our method is further improved by reducing unnecessary engine calls by detecting regularity. Experiments on a benchmark suite from industrial datapath circuits show that our method is much faster than the state-of-the-art CEC tool namely ABC ‘&cec’ on nearly all instances, and is more than 100× faster on 30% of the instances, 1000× faster on 12% of the instances.

The subgraph isomorphism problem (SIP) is a challenging problem with wide practical applications. In the last decade, despite being a theoretical hard problem, researchers design various algorithms for solving SIP. In this work, we propose three main heuristics and develop an improved exact algorithm for SIP. First, we design a probing search procedure to try whether the search procedure can successfully obtain a solution at first sight. Second, we design a novel matching ordering as a value-ordering heuristic, which uses some useful information obtained from the probing search procedure to preferentially select some promising target vertices. Third, we discuss the characteristics of different propagation methods in the context of SIP and present an adaptive propagation method to make a good balance between these methods. Experimental results on a broad range of real-world benchmarks show that our proposed algorithm performs better than state-of-the-art algorithms for the SIP.

The increasing demand for software customization has led to the development of highly configurable systems. Combinatorial interaction testing (CIT) is an effective method for testing these types of systems. The ultimate goal of CIT is to generate a test suite of acceptable size, called a t-wise covering array (CA), where t is the testing strength. Pairwise testing (i.e., CIT with t=2) is recognized to be the most widely-used CIT technique and has strong fault detection capability. In pairwise testing, the most important problem is pairwise CA generation (PCAG), which is to generate a pairwise CA (PCA) of minimum size. However, existing state-of-the-art PCAG algorithms suffer from the severe scalability challenge; that is, they cannot tackle large-scale PCAG instances effectively, resulting in PCAs of large sizes. To alleviate this challenge, in this paper we propose CAmpactor, a novel and effective local search algorithm for compacting given PCAs into smaller sizes. Extensive experiments on a large number of real-world, public PCAG instances show that the sizes of CAmpactor's generated PCAs are around 45% smaller than the sizes of PCAs constructed by existing state-of-the-art PCAG algorithms, indicating its superiority. Also, our evaluation confirms the generality of CAmpactor, since CAmpactor can reduce the sizes of PCAs generated by a variety of PCAG algorithms.

Satisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a formula with respect to certain background first-order theories. In this article, we focus on Satisfiablity Modulo Integer Arithmetic, which is referred to as SMT(IA), including both linear and non-linear integer arithmetic theories. Dominant approaches to SMT rely on calling a CDCL-based SAT solver, either in a lazy or eager flavour. Local search, a competitive approach to solving combinatorial problems including SAT, however, has not been well studied for SMT. We develop the first local-search algorithm for SMT(IA) by directly operating on variables, breaking through the traditional framework. We propose a local-search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for integer arithmetic, as well as a two-level operation selection heuristic. Putting these together, we develop a local search SMT(IA) solver called LocalSMT. Experiments are carried out to evaluate LocalSMT on benchmark sets from SMT-LIB. The results show that LocalSMT is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets from SMT-LIB.

The maximum k-club problem (MkCP) is an important clique relaxation problem with wide applications. Previous MkCP algorithms only work on small-scale instances and are not applicable for large-scale instances. For solving instances with different scales, this paper develops an efficient local search algorithm named NukCP for the MkCP which mainly includes two novel ideas. First, we propose a dynamic reduction strategy, which makes a good balance between the time efficiency and the precision effectiveness of the upper bound calculation. Second, a stratified threshold configuration checking strategy is designed by giving different priorities for the neighborhood in the different levels. Experiments on a broad range of different scale instances show that NukCP significantly outperforms the state-of-the-art MkCP algorithms on most instances.

Configuration checking (CC) has been confirmed to alleviate the cycling problem in local search for combinatorial optimization problems (COPs). When using CC heuristics in local search for graph problems, a critical concept is the configuration of the vertices. All existing CC variants employ either 1- or 2-level neighborhoods of a vertex as its configuration. Inspired by the idea that neighborhoods with different levels should have different contributions to solving COPs, we propose the probabilistic configuration (PC), which introduces probabilities for neighborhoods at different levels to consider the impact of neighborhoods of different levels on the CC strategy. Based on the concept of PC, we first propose probabilistic configuration checking (PCC), which can be developed in an automated and lightweight favor. We then apply PCC to two classic COPs which have been shown to achieve good results by using CC, and our preliminary results confirm that PCC improves the existing algorithms because PCC alleviates the cycling problem.

Abstract Satisfiability Modulo Linear Integer Arithmetic, SMT (LIA) for short, has significant applications in many domains. In this paper, we develop the first local search algorithm for SMT (LIA) by directly operating on variables, breaking through the traditional framework. We propose a local search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for LIA, and propose a two-level operation selection heuristic. Putting these together, we develop a local search SMT (LIA) solver called LS-LIA. Experiments are carried out to evaluate LS-LIA on benchmarks from SMTLIB and two benchmark sets generated from job shop scheduling and data race detection. The results show that LS-LIA is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets of LIA and IDL benchmarks from SMT-LIB. LS-LIA also solves Job Shop Scheduling benchmarks substantially faster than traditional complete SMT solvers.

Modern SAT solvers are based on a paradigm named conflict driven clause learning (CDCL), while local search is an important alternative. Although there have been attempts combining these two methods, this work proposes deeper cooperation techniques. First, we relax the CDCL framework by extending promising branches to complete assignments and calling a local search solver to search for a model nearby. More importantly, the local search assignments and the conflict frequency of variables in local search are exploited in the phase selection and branching heuristics of CDCL. We use our techniques to improve three typical CDCL solvers (glucose, MapleLCMDistChronoBT and Kissat). Experiments on benchmarks from the Main tracks of SAT Competitions 2017-2020 and a real world benchmark of spectrum allocation show that the techniques bring significant improvements, particularly on satisfiable instances. A resulting solver won the Main Track SAT category in SAT Competition 2020 and also performs very well on the spectrum allocation benchmark. As far as we know, this is the first work that meets the standard of the challenge ``Demonstrate the successful combination of stochastic search and systematic search techniques, by the creation of a new algorithm that outperforms the best previous examples of both approaches.'' (AAAI 1997) on standard application benchmarks.

Combinatorial interaction testing (CIT) is an effective paradigm for testing highly configurable systems, and its goal is to generate a t-wise covering array (CA) as a test suite, where t is the strength of testing. It is recognized that pairwise testing (i.e., CIT with t=2) is the most common CIT technique, and has high fault detection capability in practice. The problem of pairwise CA generation (PCAG), which is a core problem in pairwise testing, aims at generating a pairwise CA (i.e., 2-wise CA) of minimum size, subject to hard constraints. The PCAG problem is a hard combinatorial optimization problem, which urgently requires practical methods for generating pairwise CAs (PCAs) of small sizes. However, existing PCAG algorithms suffer from the severe scalability issue; that is, when solving large-scale PCAG instances, existing state-of-the-art PCAG algorithms usually cost a fairly long time to generate large PCAs, which would make the testing of highly configurable systems both ineffective and inefficient. In this paper, we propose a novel and effective sampling-based approach dubbed SamplingCA for solving the PCAG problem. SamplingCA first utilizes sampling techniques to obtain a small test suite that covers valid pairwise tuples as many as possible, and then adds a few more test cases into the test suite to ensure that all valid pairwise tuples are covered. Extensive experiments on 125 public PCAG instances show that our approach can generate much smaller PCAs than its state-of-the-art competitors, indicating the effectiveness of SamplingCA. Also, our experiments show that SamplingCA runs one to two orders of magnitude faster than its competitors, demonstrating the efficiency of SamplingCA. Our results confirm that SamplingCA is able to address the scalability issue and considerably pushes forward the state of the art in PCAG solving.

On practical applications, state-of-the-art SAT solvers dominantly use the conflict-driven clause learning (CDCL) paradigm. An alternative for satisfiable instances is local search solvers, which is more successful on random and hard combinatorial instances. Although there have been attempts to combine these methods in one framework, a tight integration which improves the state of the art on a broad set of application instances has been missing. We present a combination of techniques that achieves such an improvement. Our first contribution is to maximize in a local search fashion the assignment trail in CDCL, by sticking to and extending promising assignments via a technique called target phases. Second, we relax the CDCL framework by again extending promising branches to complete assignments while ignoring conflicts. These assignments are then used as starting point of local search which tries to find improved assignments with fewer unsatisfied clauses. Third, these improved assignments are imported back to the CDCL loop where they are used to determine the value assigned to decision variables. Finally, the conflict frequency of variables in local search can be exploited during variable selection in branching heuristics of CDCL. We implemented these techniques to improve three representative CDCL solvers (Glucose, MapleLcm DistChronoBT, and Kissat). Experiments on benchmarks from the main tracks of the last three SAT Competitions from 2019 to 2021 and an additional benchmark set from spectrum allocation show that the techniques bring significant improvements, particularly and not surprisingly, on satisfiable real-world application instances. We claim that these techniques were essential to the large increase in performance witnessed in the SAT Competition 2020 where Kissat and Relaxed LcmdCbDl NewTech were leading the field followed by CryptoMiniSAT-Ccnr, which also incorporated similar ideas.

The Clique Partitioning Problem (CPP) is essential in graph theory with a number of important applications. Due to its NP-hardness, efficient algorithms for solving this problem are very crucial for practical purposes, and simulated annealing is proved to be effective in state-of-the-art CPP algorithms. However, to make simulated annealing more efficient to solve large-scale CPPs, in this paper, we propose a new iterated simulated annealing algorithm. Several methods are proposed in our algorithm to improve simulated annealing. First, a new configuration checking strategy based on timestamp is presented and incorporated into simulated annealing to avoid search cycles. Afterwards, to enhance the local search ability of simulated annealing and speed up convergence, we combine our simulated annealing with a descent search method to solve the CPP. This method further improves solutions found by simulated annealing, and thus compensates for the local search effect. To further accelerate the convergence speed, we introduce a shrinking factor to decline initial temperature and then propose an iterated local search algorithm based on simulated annealing. Additionally, a restart strategy is adopted when the search procedure converges. Extensive experiments on benchmark instances of the CPP were carried out, and the results suggest that the proposed simulated annealing algorithm outperforms all the existing heuristic algorithms, including five state-of-the-art algorithms. Thus the best-known solutions for 34 instances out of 94 are updated. We also conduct comparative analyses of the proposed strategies and show their effectiveness.

The maximum quasi-clique problem (MQCP) is an important extension of maximum clique problem with wide applications. Recent heuristic MQCP algorithms can hardly solve large and hard graphs effectively. This paper develops an efficient local search algorithm named NuQClq for the MQCP, which has two main ideas. First, we propose a novel vertex selection strategy, which utilizes cumulative saturation information to be a selection criterion when the candidate vertices have equal values on the primary scoring function. Second, a variant of configuration checking named BoundedCC is designed by setting an upper bound for the threshold of forbidding strength. When the threshold value of vertex exceeds the upper bound, we reset its threshold value to increase the diversity of search process. Experiments on a broad range of classic benchmarks and sparse instances show that NuQClq significantly outperforms the state-of-the-art MQCP algorithms for most instances.

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.

Positive-unlabeled learning (PU learning) is an important case of binary classification where the training data only contains positive and unlabeled samples. The current state-of-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.

This work is dedicated to improving local search solvers for the Boolean satisfiability (SAT) problem on structured instances. We propose a construct-and-cut (CnC) algorithm based on unit propagation, which is used to produce initial assignments for local search. We integrate our CnC initialization procedure within several state-of-the-art local search SAT solvers, and obtain the improved solvers. Experiments are carried out with a benchmark encoded from a spectrum repacking project as well as benchmarks encoded from two important mathematical problems namely Boolean Pythagorean Triple and Schur Number Five. The experiments show that the CnC initialization improves the local search solvers, leading to better performance than state-of-the-art SAT solvers based on Conflict Driven Clause Learning (CDCL) solvers.

The minimum weighted connected dominating set (MWCDS) problem is an important variant of connected dominating set problems with wide applications, especially in heterogenous networks and gene regulatory networks. In the paper, we develop a nested local search algorithm called NestedLS for solving MWCDS on classic benchmarks and massive graphs. In this local search framework, we propose two novel ideas to make it effective by utilizing previous search information. First, we design the restart based smoothing mechanism as a diversification method to escape from local optimal. Second, we propose a novel inner-layer local search method to enlarge the candidate removal set, which can be modelled as an optimized version of spanning tree problem. Moreover, inner-layer local search method is a general method for maintaining the connectivity constraint when dealing with massive graphs. Experimental results show that NestedLS outperforms state-of-the-art meta-heuristic algorithms on most instances.

Combinatorial interaction testing (CIT) is an important technique for testing highly configurable software systems with demonstrated effectiveness in practice. The goal of CIT is to generate test cases covering the interactions of configuration options, under certain hard constraints. In this context, constrained covering arrays (CCAs) are frequently used as test cases in CIT. Constrained Covering Array Generation (CCAG) is an NP-hard combinatorial optimization problem, solving which requires an effective method for generating small CCAs. In particular, effectively solving t-way CCAG with t>=4 is even more challenging. Inspired by the success of automated algorithm configuration and automated algorithm selection in solving combinatorial optimization problems, in this paper, we investigate the efficacy of automated algorithm configuration and automated algorithm selection for the CCAG problem, and propose a novel, automated CCAG approach called AutoCCAG. Extensive experiments on public benchmarks show that AutoCCAG can find much smaller-sized CCAs than current state-of-the-art approaches, indicating the effectiveness of AutoCCAG. More encouragingly, to our best knowledge, our paper reports the first results for CCAG with a high coverage strength (i.e., 5-way CCAG) on public benchmarks. Our results demonstrate that AutoCCAG can bring considerable benefits in testing highly configurable software systems.

This paper explores techniques to quickly solve the maximum weight clique problem (MWCP) in very large scale sparse graphs. Due to their size, and the hardness of MWCP, it is infeasible to solve many of these graphs with exact algorithms. Although recent heuristic algorithms make progress in solving MWCP in large graphs, they still need considerable time to get a high-quality solution. In this work, we focus on solving MWCP for large sparse graphs within a short time limit. We propose a new method for MWCP which interleaves clique finding with data reduction rules. We propose novel ideas to make this process efficient, and develop an algorithm called FastWClq. Experiments on a broad range of large sparse graphs show that FastWClq finds better solutions than state-of-the-art algorithms while the running time of FastWClq is much shorter than the competitors for most instances. Further, FastWClq proves the optimality of its solutions for roughly half of the graphs, all with at least 105 vertices, with an average time of 21 seconds.

The minimum connected dominating set (MCDS) problem is an important extension of the minimum dominating set problem, with wide applications, especially in wireless networks. Most previous works focused on solving MCDS problem in graphs with relatively small size, mainly due to the complexity of maintaining connectivity. This paper explores techniques for solving MCDS problem in massive real-world graphs with wide practical importance. Firstly, we propose a local greedy construction method with reasoning rule called 1hopReason. Secondly and most importantly, a hybrid dynamic connectivity maintenance method (HDC+) is designed to switch alternately between a novel fast connectivity maintenance method based on spanning tree and its previous counterpart. Thirdly, we adopt a two-level vertex selection heuristic with a newly proposed scoring function called chronosafety to make the algorithm more considerate when selecting vertices. We design a new local search algorithm called FastCDS based on the three ideas. Experiments show that FastCDS significantly outperforms five state-of-the-art MCDS algorithms on both massive graphs and classic benchmarks.

The Maximum k-plex Problem is an important combinatorial optimization problem with increasingly wide applications. In this paper, we propose a novel strategy, named Dynamic-threshold Configuration Checking (DCC), to reduce the cycling problem of local search. Due to the complicated neighborhood relations, all the previous local search algorithms for this problem spend a large amount of time in identifying feasible neighbors in each step. To further improve the performance on dense and challenging instances, we propose Double-attributes Incremental Neighborhood Updating (DINU) scheme which reduces the worst-case time complexity per iteration from O(|V|⋅ΔG) to O(k · Δ‾G). Based on DCC strategy and DINU scheme, we develop a local search algorithm named DCCplex. According to the experiment result, DCCplex shows promising result on DIMACS and BHOSLIB benchmark as well as real-world massive graphs. Especially, DCCplex updates the lower bound of the maximum k-plex for most dense and challenging instances.

The Set Covering Problem (SCP) and Dominating Set Problem (DSP) are NP-hard and have many real world applications. SCP and DSP can be encoded into Maximum Satisfiability (MaxSAT) naturally and the resulting instances share a special structure. In this paper, we develop an efficient local search solver for MaxSAT instances of this kind. Our algorithm contains three phrase: construction, local search and recovery. In construction phrase, we simplify the instance by three reduction rules and construct an initial solution by a greedy heuristic. The initial solution is improved during the local search phrase, which exploits the feature of such instances in the scoring function and the variable selection heuristic. Finally, the corresponding solution of original instance is recovered in the recovery phrase. Experiment results on a broad range of large scale instances of SCP and DSP show that our algorithm significantly outperforms state of the art solvers for SCP, DSP and MaxSAT.

The weighted graph coloring problem (WGCP) is an important extension of the graph coloring problem (GCP) with wide applications. Compared to GCP, where numerous methods have been developed and even massive graphs with millions of vertices can be solved well, fewer works have been done for WGCP, and no solution is available for solving WGCP for massive graphs. This paper explores techniques for solving WGCP, including a lower bound and a reduction rule based on clique sampling, and a local search algorithm based on two selection rules and a new variant of configuration checking. This results in our algorithm RedLS (Reduction plus Local Search). Experiments are conducted to compare RedLS with the state-of-the-art algorithms on massive graphs as well as conventional benchmarks studied in previous works. RedLS exhibits very good performance and robustness. It significantly outperforms previous algorithms on all benchmarks.

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.

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.

The minimum connected dominating set (MCDS) problem is an important extension of the minimum dominating set problem, with wide applications, especially in wireless networks. Despite its practical importance, there are few works on solving MCDS for massive graphs, mainly due to the complexity of maintaining connectivity. In this paper, we propose two novel ideas, and develop a new local search algorithm for MCDS called NuCDS. First, a hybrid dynamic connectivity maintenance method is designed to switch alternately between a novel fast connectivity maintenance method based on spanning tree and its previous counterpart. Second, we define a new vertex property called \emph{safety} to make the algorithm more considerate when selecting vertices. Experiments show that NuCDS significantly outperforms the state-of-the-art MCDS algorithms on both massive graphs and classic benchmarks.

The Boolean satisfiability problem (SAT) is a famous NP-complete problem in computer science. An effective way for solving a satisfiable SAT problem is the stochastic local search (SLS). However, in this method, the initialization is assigned in a random manner, which impacts the effectiveness of SLS solvers. To address this problem, we propose NLocalSAT. NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network. We evaluated NLocalSAT on five SLS solvers (CCAnr, Sparrow, CPSparrow, YalSAT, and probSAT) with instances in the random track of SAT Competition 2018. The experimental results show that solvers with NLocalSAT achieve 27% ~ 62% improvement over the original SLS solvers.

In large-scale cloud systems, unplanned service interruptions and outages may cause severe degradation of service availability. Such incidents can occur in a bursty manner, which will deteriorate user satisfaction. Identifying incidents rapidly and accurately is critical to the operation and maintenance of a cloud system. In industrial practice, incidents are typically detected through analyzing the issue reports, which are generated over time by monitoring cloud services. Identifying incidents in a large number of issue reports is quite challenging. An issue report is typically multi-dimensional: it has many categorical attributes. It is difficult to identify a specific attribute combination that indicates an incident. Existing methods generally rely on pruning-based search, which is time-consuming given high-dimensional data, thus not practical to incident detection in large-scale cloud systems. In this paper, we propose MID (Multi-dimensional Incident Detection), a novel framework for identifying incidents from large-amount, multi-dimensional issue reports effectively and efficiently. Key to the MID design is encoding the problem into a combinatorial optimization problem. Then a specific-tailored meta-heuristic search method is designed, which can rapidly identify attribute combinations that indicate incidents. We evaluate MID with extensive experiments using both synthetic data and real-world data collected from a large-scale production cloud system. The experimental results show that MID significantly outperforms the current state-of-the-art methods in terms of effectiveness and efficiency. Additionally, MID has been successfully applied to Microsoft's cloud systems and helped greatly reduce manual maintenance effort.

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.

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.

Combinatorial interaction testing (CIT) is a popular approach to detecting faults in highly configurable software systems. The core task of CIT is to generate a small test suite called a t-way covering array (CA), where t is the covering strength. Many meta-heuristic algorithms have been proposed to solve the constrained covering array generating (CCAG) problem. A major drawback of existing algorithms is that they usually need considerable time to obtain a good-quality solution, which hinders the wider applications of such algorithms. We observe that the high time consumption of existing meta-heuristic algorithms for CCAG is mainly due to the procedure of score computation. In this work, we propose a much more efficient method for score computation. The score computation method is applied to a state-of-the-art algorithm TCA, showing significant improvements. The new score computation method opens a way to utilize algorithmic ideas relying on scores which were not affordable previously. We integrate a gradient descent search step to further improve the algorithm, leading to a new algorithm called FastCA. Experiments on a broad range of real-world benchmarks and synthetic benchmarks show that, FastCA significantly outperforms state-of-the-art algorithms for CCAG algorithms, in terms of both the size of obtained covering array and the run time.

The minimum weighted vertex cover (MWVC) problem is a well known combinatorial optimization problem with important applications. This paper introduces a novel local search algorithm called NuMWVC for MWVC based on three ideas. First, four reduction rules are introduced during the initial construction phase. Second, the configuration checking with aspiration is proposed to reduce cycling problem. Moreover, a self-adaptive vertex removing strategy is proposed to save time.

The minimum weight vertex cover (MWVC) problem is an important combinatorial optimization problem with various real-world applications. Due to its NP hardness, most works on solving MWVC focus on heuristic algorithms that can return a good quality solution in reasonable time. In this work, we propose two dynamic strategies that adjust the behavior of the algorithm during search, which are used to improve a state of the art local search for MWVC named FastWVC, resulting in two local search algorithms called DynWVC1 and DynWVC2. Previous MWVC algorithms are evaluated on graphs with random or hand crafted weights. In this work, we evaluate the algorithms on the vertex weighted graphs that obtained from an important real world problem, the map labeling problem. Experiments show that our algorithm obtains better results than previous algorithms for MWVC and maximum weight independent set (MWIS) on these real world instances. We also test our algorithms on massive graphs studied in previous works, and show significant improvements there.

Partial MaxSAT (PMS) generalizes SAT and MaxSAT by introducing hard clauses and soft clauses. PMS and Weighted PMS (WPMS) have many important real world applications. Local search is one popular method for solving (W)PMS. Recent studies on specialized local search for (W)PMS have led to significant improvements. But such specialized algorithms are complicated with the concepts tailored for hard and soft clauses. In this work, we propose a dynamic local search algorithm, which exploits the structure of (W)PMS by a carefully designed clause weighting scheme. Our solver SATLike adopts a local search framework for SAT and does not need any specialized concept for (W)PMS. Experiments on PMS and WPMS benchmarks from the MaxSAT Evaluations (MSE) 2016 and 2017 show that SATLike significantly outperforms state of the art local search solvers. Also, SATLike significantly narrows the gap between the performance of local search solvers and complete solvers on industrial benchmarks, and performs better than the complete solvers on the MSE2017 benchmarks.

The minimum weight dominating set (MWDS) problem is NP-hard and also important in many applications. Recent heuristic MWDS algorithms can hardly solve massive real world graphs effectively. In this paper, we design a fast local search algorithm called FastMWDS for the MWDS problem, which aims to obtain a good solution on massive graphs within a short time. In this novel local search framework, we propose two ideas to make it effective. Firstly, we design a new fast construction procedure with four reduction rules to cut down the size of massive graphs. Secondly, we propose the three-valued two-level configuration checking strategy to improve local search, which is interestingly a variant of configuration checking (CC) with two levels and multiple values. Experiment results on a broad range of massive real world graphs show that FastMWDS finds much better solutions than state of the art MWDS algorithms.

Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this article, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework as follows: (1) To prove the correctness of a parameterized protocol, our approach automatically discovers auxiliary invariants and the corresponding dependency relations among the discovered invariants and protocol rules from a small instance of the to-be-verified protocol, and (2) the discovered invariants and dependency graph are then automatically generalized into a parameterized form and sent to the theorem prover, Isabelle. As a side product, the final verification result of a protocol is provided by a formal and human-readable proof. Our approach has been successfully applied to a number of benchmarks, including snoopying-based and directory-based cache coherence protocols.

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.

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.

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.

The Minimum Weight Dominating Set (MWDS) problem is an important generalization of the Minimum Dominating Set (MDS) problem with extensive applications. This paper proposes a new local search algorithm for the MWDS problem, which is based on two new ideas. The first idea is a heuristic called two-level configuration checking (CC2), which is a new variant of a recent powerful configuration checking strategy (CC) for effectively avoiding the recent search paths. The second idea is a novel scoring function based on the frequency of being uncovered of vertices. Our algorithm is called CC2FS, according to the names of the two ideas. The experimental results show that, CC2FS performs much better than some state-of-the-art algorithms in terms of solution quality on a broad range of MWDS benchmarks.

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.

The Minimum Weight Dominating Set (MWDS) problem is an important generalization of the Minimum Dominating Set (MDS) problem with extensive applications. This paper proposes a new local search algorithm for the MWDS problem, which is based on two new ideas. The first idea is a heuristic called two-level configuration checking (CC2), which is a new variant of a recent powerful configuration checking strategy (CC) for effectively avoiding the recent search paths. The second idea is a novel scoring function based on the frequency of being uncovered of vertices. Our algorithm is called CC2FS, according to the names of the two ideas. The experimental results show that, CC2FS performs much better than some state-of-the-art algorithms in terms of solution quality on a broad range of MWDS benchmarks.

The Maximum Weight Clique problem (MWCP) is an important generalization of the Maximum Clique problem with wide applications. This paper introduces two heuristics and develops two local search algorithms for MWCP. Firstly, we propose a heuristic called strong configuration checking (SCC), which is a new variant of a recent powerful strategy called configuration checking (CC) for reducing cycling in local search. Based on the SCC strategy, we develop a local search algorithm named LSCC. Moreover, to improve the performance on massive graphs, we apply a low-complexity heuristic called Best from Multiple Selection (BMS) to select the swapping vertex pair quickly and effectively. The BMS heuristic is used to improve LSCC, resulting in the LSCC+BMS algorithm. Experiments show that the proposed algorithms outperform the state-of-the-art local search algorithm MN/TS and its improved version MN/TS+BMS on the standard benchmarks namely DIMACS and BHOSLIB, as well as a wide range of real world massive graphs.

Parameterized verification of parameterized protocols like cache coherence protocols is an important but hard problem. Our tool paraVerifier handles this hard problem in a unified framework: (1) it automatically discovers auxiliary invariants and the corresponding causal relations from a small reference instance of the verified protocol; (2) the above invariants and causal relation information are automatically generalized into a parameterized form to construct a parameterized formal proof in a theorem prover (e.g., Isabelle). Our method is successfully applied to typical benchmarks including snooping and directory cache coherence protocol benchmarks. The correctness of these protocols is guaranteed by a formal and readable proof which is automatically generated. The notoriously hard FLASH protocol, which is at an industrial scale, is also verified.

Minimum Vertex Cover (MinVC) is a well known NP-hard combinatorial optimization problem, and local search has been shown to be one of the most effective approaches to this problem. State-of-the-art MinVC local search algorithms employ edge weighting techniques and prefer to select vertices with higher weighted score. These algorithms are not robust and especially have poor performance on instances with structures which defeat greedy heuristics. In this paper, we propose a vertex weighting scheme to address this shortcoming, and combine it within the current best MinVC local search algorithm NuMVC, leading to a new algorithm called TwMVC. Our experiments show that TwMVC outperforms NuMVC on the standard benchmarks namely DIMACS and BHOSLIB. To the best of our knowledge, TwMVC is the first MinVC algorithm that attains the best known solution for all instances in both benchmarks. Further, TwMVC shows superiority on a benchmark of real-world networks.

Covering arrays (CAs) are often used as test suites for combinatorial interaction testing to discover interaction faults of real-world systems. Most real-world systems involve constraints, so improving algorithms for covering array generation (CAG) with constraints is beneficial. Two popular methods for constrained CAG are greedy construction and meta-heuristic search. Recently, a meta-heuristic framework called two-mode local search has shown great success in solving classic NPhard problems. We are interested whether this method is also powerful in solving the constrained CAG problem. This work proposes a two-mode meta-heuristic framework for constrained CAG efficiently and presents a new meta-heuristic algorithm called TCA. Experiments show that TCA significantly outperforms state-of-the-art solvers on 3-way constrained CAG. Further experiments demonstrate that TCA also performs much better than its competitors on 2-way constrained CAG.

Stochastic local search (SLS) algorithms are well known for their ability to efficiently find models of random instances of the Boolean satisfiability (SAT) problem. One of the most famous SLS algorithms for SAT is WalkSAT, which is an initial algorithm that has wide influence and performs very well on random 3-SAT instances. However, the performance of WalkSAT on random k-SAT instances with k > 3 lags far behind. Indeed, there are limited works on improving SLS algorithms for such instances. This work takes a good step toward 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 show that WalkSATlm improves WalkSAT by orders of magnitude on random k-SAT instances with k > 3 near the phase transition. Additionally, we propose an efficient implementation for WalkSATlm, which leads to a speedup of 100%. We also give some insights on different forms of linear make functions, and show the limitation of the linear make function on random 3-SAT through theoretical analysis.

The maximum satisfiability (MAX-SAT) problem, especially the weighted version, has extensive applications. Weighted MAX-SAT instances encoded from real-world applications may be very large, which calls for efficient approximate methods, mainly stochastic local search (SLS) ones. However, few works exist on SLS algorithms for weighted MAX-SAT. In this paper, we propose a new heuristic called CCM for weighted MAX-SAT. The CCM heuristic prefers to select a CCMP variable. By combining CCM with random walk, we design a simple SLS algorithm dubbed CCLS for weighted MAX-SAT. The CCLS algorithm is evaluated against a state-of-the-art SLS solver IRoTS and two state-of-the-art complete solvers namely akmaxsat_ls and New WPM2, on a broad range of weighted MAX-SAT instances. Experimental results illustrate that the quality of solution found by CCLS is much better than that found by IRoTS, akmaxsat_ls and New WPM2 on most industrial, crafted and random instances, indicating the efficiency and the robustness of the CCLS algorithm. Furthermore, CCLS is evaluated in the weighted and unweighted MAX-SAT tracks of incomplete solvers in the Eighth Max-SAT Evaluation (Max-SAT 2013), and wins four tracks in this evaluation, illustrating that the performance of CCLS exceeds the current state-of-the-art performance of SLS algorithms on solving MAX-SAT instances.

Two-mode stochastic local search (SLS) and focused random walk (FRW) are the two most influential paradigms of SLS algorithms for the propositional satisfiability (SAT) problem. Recently, an interesting idea called configuration checking (CC) was proposed to handle the cycling problem in SLS. The CC idea has been successfully used to improve SLS algorithms for SAT, resulting in state-of-the-art solvers. Previous CC strategies for SAT are based on neighboring variables, and prove successful in two-mode SLS algorithms. However, this kind of neighboring variables based CC strategy is not suitable for improving FRW algorithms. In this paper, we propose a new CC strategy which is based on clause states. We apply this clause states based CC (CSCC) strategy to both two-mode SLS and FRW paradigms. Our experiments show that the CSCC strategy is effective on both paradigms. Furthermore, our developed FRW algorithms based on CSCC achieve state-of-the-art performance on a broad range of random SAT benchmarks.

Existing algorithms for I/O Linear Temporal Logic (LTL) model checking usually output a single counterexample for a system which violates the property. However, in real-world applications, such as diagnosis and debugging in software and hardware system designs, people often need to have a set of counterexamples or even all counterexamples. For this purpose, we propose an I/O efficient approach for detecting all accepting cycles, called Detecting All Accepting Cycles (DAAC), where the properties to be verified are in LTL. Different from other algorithms for finding all cycles, DAAC first searches for the accepting strongly connected components (ASCCs), and then finds all accepting cycles of every ASCC, which can avoid searching for a great many paths that are impossible to be extended to accepting cycles. In order to further lower DAAC's I/O complexity and improve its performance, we propose an intersection computation technique and a dynamic path management technique, and exploit a minimal perfect hash function (MPHF). We carry out both complexity and experimental comparisons with the state-of-the-art algorithms including Detect Accepting Cycle (DAC), Maximal Accepting Predecessors (MAP) and Iterative-Deepening Depth-First Search (IDDFS). The comparative results show that our approach is better on the whole in terms of I/O complexity and practical performance, despite the fact that it finds all counterexamples.

Model checking is a powerful approach for the formal verification of hardware and software systems. However, this approach suffers from the state space explosion problem, which limits its application to large-scale systems due to space shortage. To overcome this drawback, one of the most effective solutions is to use external memory algorithms. In this paper, we propose an I/O efficient model checking algorithm for large-scale systems. To lower I/O complexity and improve time efficiency, we combine three new techniques: 1) a linear hash-sorting technique; 2) a cached duplicate detection technique; and 3) a dynamic path management technique. We show that the new algorithm has a lower I/O complexity than state-of-the-art I/O efficient model checking algorithms, including detect accepting cycle, maximal accepting predecessors, and iterative-deepening depth-first search. In addition, the experiments show that our algorithm obviously outperforms these three algorithms on the selected representative benchmarks in terms of performance.

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 {\it Dist}. Experimental results on PMS benchmarks from MaxSAT Evaluation 2013 show that {\it 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, {\it Dist} dramatically outperforms previous local search algorithms and is comparable with complete algorithms.

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.

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models for satisfiable instances of the satisfiability (SAT) problem, especially for random k-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random k-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as "score_2", was proposed for improving SLS algorithms on long-clause SAT instances, and was first used in the powerful CCASat solver as a tie breaker. In this paper, we propose three new scoring functions based on score_2. Despite their simplicity, these functions are very effective for solving random k-SAT with long clauses. The first function combines score and score_2, and the second one additionally integrates the diversification property "age". These two functions are used in developing a new SLS algorithm called CScoreSAT. Experimental results on large random 5-SAT and 7-SAT instances near phase transition show that CScoreSAT significantly outperforms previous SLS solvers. However, CScoreSAT cannot rival its competitors on random k-SAT instances at phase transition. We improve CScoreSAT for such instances by another scoring function which combines score_2 with age. The resulting algorithm HScoreSAT exhibits state-of-the-art performance on random k-SAT (k>3) instances at phase transition. We also study the computation of score_2, including its implementation and computational complexity.

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 WalkSAT$lm$. Our experimental results on random 5-SAT and 7-SAT instances show that WalkSAT$lm$ improves WalkSAT by orders of magnitudes. Moreover, WalkSAT$lm$ significantly outperforms state-of-the-art SLS solvers on random 5-SAT instances, while competes well on random 7-SAT ones. Additionally, WalkSAT$lm$ performs very well on random instances from SAT Challenge 2012, indicating its robustness.

This paper presents and analyzes two new efficient local search strategies for the Boolean Satisfiability (SAT) problem. We start by proposing a local search strategy called configuration checking (CC) for SAT. The CC strategy results in a simple local search algorithm for SAT called Swcc, which shows promising experimental results on random 3-SAT instances, and outperforms TNM, the winner of SAT Competition 2009. However, the CC strategy for SAT is still in a nascent stage, and Swcc cannot yet compete with Sparrow2011, which won SAT Competition 2011 just after Swcc had been designed. The CC strategy seems too strict in that it forbids flipping those variables even with great scores, if they do not satisfy the CC criterion. We improve the CC strategy by adopting an aspiration mechanism, and get a new variable selection heuristic called configuration checking with aspiration (CCA). The CCA heuristic leads to an improved algorithm called Swcca, which exhibits state-of-the-art performance on random 3-SAT instances and crafted ones. The third contribution concerns improving local search algorithms for random k-SAT instances with k>3. Although the SAT community has made great achievements in solving random 3-SAT instances, the progress lags far behind on random k-SAT instances with k>3. This work proposes a new variable property called subscore, which is utilized to break ties in the CCA heuristic when candidate variables for flipping have the same score. The resulting algorithm CCAsubscore is very efficient for solving random k-SAT instances with k>3, and significantly outperforms other state-of-the-art ones. Combining Swcca and CCAsubscore, we obtain a local search SAT solver called CCASat, which was ranked first in the random track of SAT Challenge 2012. Additionally, we perform theoretical analyses on the CC strategy and the subscore property, and show interesting results on these two heuristics. Particularly, our analysis indicates that the CC strategy is more effective for k-SAT with smaller k, while the subscore notion is not suitable for solving random 3-SAT.

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.

An interesting strategy called configuration checking (CC) was recently proposed to handle the cycling problem in local search for Minimum Vertex Cover. A natural question is whether this CC strategy also works for SAT. The direct application of CC did not result in stochastic local search (SLS) algorithms that can compete with the current best SLS algorithms for SAT. In this paper, we propose a new heuristic based on CC for SLS algorithms for SAT, which is called configuration checking with aspiration (CCA). It is used to develop a new SLS algorithm called Swcca. The experiments on random 3-SAT instances show that Swcca significantly outperforms Sparrow2011, the winner of the random satisfiable category of the SAT Competition 2011, which is considered to be the best local search solver for random 3-SAT instances. Moreover, the experiments on structured instances show that Swcca is competitive with Sattime, the best local search solver for the crafted benchmark in the SAT Competition 2011.

In this paper, we propose two new strategies to design efficient local search algorithms for the minimum vertex cover (MVC) problem. There are two main drawbacks in state-of-the-art MVC local search algorithms: First, they select a pair of vertices to be exchanged simultaneously, which is time consuming; Second, although they use edge weighting techniques, they do not have a strategy to decrease the weights. To address these drawbacks, we propose two new strategies: two stage exchange and edge weighting with forgetting. The two stage exchange strategy selects two vertices to be exchanged 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. We utilize these two strategies to design a new algorithm dubbed NuMVC. The experimental results show that NuMVC significantly outperforms existing state-of-the-art heuristic algorithms on most of the hard DIMACS instances and all instances in the hard random BHOSLIB benchmark.

Local Search is an appealing method for solving the Boolean Satisfiability problem (SAT). However, this method suffers from the cycling problem which severely limits its power. Recently, a new strategy called configuration checking (CC) was proposed, for handling the cycling problem in local search. The CC strategy was used to improve a state-of the-art local search algorithm for Minimum Vertex Cover. In this paper, we propose a novel local search strategy for the satisfiability problem, i.e., the CC strategy for SAT. The CC strategy for SAT takes into account the circumstances of the variables when selecting a variable to flip, where the circumstance of a variable refers to truth values of all its neighboring variables. We then apply it to design a local search algorithm for SAT called SWcc (Smoothed Weighting with Configuration Checking). Experimental results show that the CC strategy for SAT is more efficient than the previous strategy for handling the cycling problem called tabu. Moreover, SWcc significantly outperforms the best local search SAT solver in SAT Competition 2009 called TNM on large random 3-SAT instances.

The Minimum Vertex Cover (MVC) problem is a well-known combinatorial optimization problem of great importance in theory and applications. In recent years, local search has been shown to be an effective and promising approach to solve hard problems, such as MVC. In this paper, we introduce two new local search algorithms for MVC, called EWLS (Edge Weighting Local Search) and EWCC (Edge Weighting Configuration Checking). The first algorithm EWLS is an iterated local search algorithm that works with a partial vertex cover, and utilizes an edge weighting scheme which updates edge weights when getting stuck in local optima. Nevertheless, EWLS has an instance-dependent parameter. Further, we propose a strategy called Configuration Checking for handling the cycling problem in local search. This is used in designing a more efficient algorithm that has no instance-dependent parameters, which is referred to as EWCC. Unlike previous vertex-based heuristics, the configuration checking strategy considers the induced subgraph configurations when selecting a vertex to add into the current candidate solution. A detailed experimental study is carried out using the well-known DIMACS and BHOSLIB benchmarks. The experimental results conclude that EWLS and EWCC are largely competitive on DIMACS benchmarks, where they outperform other current best heuristic algorithms on most hard instances, and dominate on the hard random BHOSLIB benchmarks. Moreover, EWCC makes a significant improvement over EWLS, while both EWLS and EWCC set a new record on a twenty-year challenge instance. Further, EWCC performs quite well even on structured instances in comparison to the best exact algorithm we know. We also study the run-time behavior of EWLS and EWCC which shows interesting properties of both algorithms.

A number of algorithms have been proposed for the Minimum Vertex Cover problem. However, they are far from satisfactory, especially on hard instances. In this paper, we introduce Edge Weighting Local Search (EWLS), a new local search algorithm for the Minimum Vertex Cover problem. EWLS is based on the idea of extending a partial vertex cover into a vertex cover. A key point of EWLS is to find a vertex set that provides a tight upper bound on the size of the minimum vertex cover. To this purpose, EWLS employs an iterated local search procedure, using an edge weighting scheme which updates edge weights when stuck in local optima. Moreover, some sophisticated search strategies have been taken to improve the quality of local optima. Experimental results on the broadly used DIMACS benchmark show that EWLS is competitive with the current best heuristic algorithms, and outperforms them on hard instances. Furthermore, on a suite of difficult benchmarks, EWLS delivers the best results and sets a new record on the largest instance.