SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION

As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.

A Parallel Quantum Algorithm for the Satisfiability Problem

In this paper we present a classical parallel quantum algorithm for the satisfiability problem. We have exploited the classical parallelism of quantum algorithms developed in [G.L. Long and L. Xiao, Phys. Rev. A 69 （2004） 052303], so that additional acceleration can be gained by using classical parallelism. The quantum algorithm first estimates the number of solutions using the quantum counting algorithm, and then by using the quantum searching algorithm, the explicit solutions are found.

A Multilevel Tabu Search for the Maximum Satisfiability Problem

The maximum satisfiability problem (MAX-SAT) refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weight of satisfied clauses) in a Boolean Formula. Most local search algorithms including tabu search rely on the 1-flip neighbourhood structure. In this work, we introduce a tabu search algorithm that makes use of the multilevel paradigm for solving MAX-SAT problems. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. This process aims at looking at the search as a multilevel process operating in a coarse-to-fine strategy evolving from k-flip neighbourhood to 1-flip neighbourhood-based structure. Experimental results comparing the multilevel tabu search against its single level variant are presented.

A Semi-Tensor Product Based All Solutions Boolean Satisfiability Solver

Boolean satisfiability (SAT) is widely used as a solver engine in electronic design automation (EDA). Typically, SAT is used to determine whether one or more groups of variables can be combined to form a true formula. All solutions SAT (AllSAT) is a variant of the SAT problem. In the fields of formal verification and pattern generation, AllSAT is particularly useful because it efficiently enumerates all possible solutions. In this paper, a semi-tensor product (STP) based AllSAT solver is proposed. The solver can solve instances described in both the conjunctive normal form (CNF) and circuit form. The implementation of our method differs from incremental enumeration because we do not add blocking conditions for existing solutions, but rather compute the matrices to obtain all the solutions in one pass. Additionally, the logical matrices support a variety of logic operations. Results from experiments with MCNC benchmarks using CNF-based and circuit-based forms show that our method can accelerate CPU time by 8.1x (238x maximum) and 19.9x (72x maximum), respectively.

Empirical investigation of stochastic local search for maximum satisfiability

The maximum satisfiability (MAX-SAT)problem is an important NP-hard problem in theory,and has a broad range of applications in practice.Stochastic local search (SLS)is becoming an increasingly popular method for solving MAX-SAT.Recently,a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances.However,the performance of CCLS on solving industrial MAX-SAT instances lags far behind.In this paper,we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances.First,we conduct experiments to analyze why CCLS performs poor on industrial instances.Then we propose a new strategy called additive BMS (Best from Multiple Selections)to ease the serious issue.By integrating CCLS and additive BMS,we develop a new SLS algorithm for MAXSAT called CCABMS,and related experiments indicate the efficiency of CCABMS.Also,we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT,and combine an effective initialization method with CCABMS,resulting in an enhanced algorithm.Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.

Modified extremal optimization for the hard maximum satisfiability problem

Based on our recent study on probability distributions for evolution in extremal optimization (EO),we propose a modified framework called EOSAT to approximate ground states of the hard maximum satisfiability (MAXSAT) problem,a generalized version of the satisfiability (SAT) problem.The basic idea behind EOSAT is to generalize the evolutionary probability distribution in the Bose-Einstein-EO (BE-EO) algorithm,competing with other popular algorithms such as simulated annealing and WALKSAT.Experimental results on the hard MAXSAT instances from SATLIB show that the modified algorithms are superior to the original BE-EO algorithm.

Machine Learning Methods in Solving the Boolean Satisfiability Problem

This paper reviews the recent literature on solving the Boolean satisfiability problem(SAT),an archetypal N P-complete problem,with the aid of machine learning(ML)techniques.Over the last decade,the machine learning society advances rapidly and surpasses human performance on several tasks.This trend also inspires a number of works that apply machine learning methods for SAT solving.In this survey,we examine the evolving ML SAT solvers from naive classifiers with handcrafted features to emerging end-to-end SAT solvers,as well as recent progress on combinations of existing conflict-driven clause learning(CDCL)and local search solvers with machine learning methods.Overall,solving SAT with machine learning is a promising yet challenging research topic.We conclude the limitations of current works and suggest possible future directions.The collected paper list is available at https://github.com/ThinklabSJTU/awesome-ml4co.Keywords:Machine learning(ML),Boolean satisfiability(SAT),deep learning,graph neural networks(GNNs),combinatorial optimization.

Properties of the satisfiability threshold of the strictly d-regular random(3,2s)-SAT problem

A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so carry-ing out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysisfor random 3-CNF formulas.Some subclasses of the regular(3,s)-CNF formula have also characteristics of intractabilitythat differ from random 3-CNF formulas.For this purpose,we propose strictly d-regular(k,2s)-CNF formula,which is aregular(k,2s)-CNF formula for which d≥0 is an even num-ber and each literal occurs s-d/2 or s+d/2 times(the literals from a variable x are x and-x,where x is positive and-x isnegative).In this paper,we present a new model to generatestrictly d-regular random(k,2s)-CNF formulas,and focuson the strictly d-regular random(3,2s)-CNF formulas.Let F be a strictly d-regular random(3,2s)-CNF formula suchthat 2s>d.We show that there exists a real number so suchthat the formula F is unsatisfiable with high probability whens>so,and present a numerical solution for the real numberso.The result is supported by simulated experiments,and isconsistent with the existing conclusion for the case of d=0.Furthermore,we have a conjecture:for a given d,the strictlyd-regular random(3,2s)-SAT problem has an SAT-UNSAT(satisfiable-unsatisfiable)phase transition.Our experimentssupport this conjecture.Finally,our experiments also showthat the parameter d is correlated with the intractability of the 3-SAT problem.Therefore,our research maybe helpful for generating random hard instances of the 3-CNF formula.

On the satisfiability of authorization requirements in business process

Satisfiability problem of authorization require- ments in business process asks whether there exists an as- signment of users to tasks that satisfies all the requirements, and methods were proposed to solve this problem. However, the proposed methods are inefficient in the sense that a step of the methods is searching all the possible assignments, which is time-consuming. This work proposes a method to solve the satisfiability problem of authorization requirements with- out browsing the assignments space. Our method uses im- proved separation of duty algebra （ISoDA） to describe a sat- isfiability problem of qualification requirements and quan- tification requirements （Separation of Duty and Binding of Duty requirements）. Thereafter, ISoDA expressions are re- duced into multi-mutual-exclusive expressions. The satisfia- bilities of multi-mutual-exclusive expressions are determined by an efficient algorithm proposed in this study. The experiment shows that our method is faster than the state-of-the-art methods.

A mathematic-physical approach to the satisfiability problem

A one-to-one and onto mapping between the set of conjunctive normal forms and a subset of the potential functions of static electric fields is given; it has been further proved that a conjunctive normal form is satisfiable if and only if there exists a zero point for its corresponding potential function. A particle is always moving in the direction of gradient descent in the field which is the fastest decreasing direction of potential of the particle. Thus, if a conjunctive normal form is satisfiable, the gradient method for its corresponding potential function becomes a fast algorithm to solve its satisfiability problem.

Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems

In this paper we study the solution of SAT problems formulated as discretedecision and discrete constrained optimization problems. Constrained formulations are better thantraditional unconstrained formulations because violated constraints may provide additional forces tolead a search towards a satisfiable assignment. We summarize the theory of extended saddle pointsin penalty formulations for solving discrete constrained optimization problems and the associateddiscrete penalty method (DPM). We then examine various formulations of the objective function,choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoidingtraps. Experimental evaluations on hard benchmark instances pinpoint that traps contributesignificantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set ofor nearby points in the original variable space. To address this issue, we propose and study twotrap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside atrap, leading to very large penalties for unsatisfied clauses that are trapped more often and makingthese clauses more likely to be satisfied in the future. The second strategy stores information onpoints visited before, whether inside traps or not, and avoids visiting points that are close topoints visited before. It can be implemented by modifying the penalty function in such a way that,if a trajectory gets close to points visited before, an extra penalty will take effect and force thetrajectory to a new region. It specializes to the first strategy because traps are special cases ofpoints visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACSand SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, andGrasp. The results demonstrate that DPM with trap avoidance is robust as well as effective forsolving hard SAT problems.

Complete Boolean Satisfiability Solving Algorithms Based on Local Search

Boolean satisfiability （SAT） is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem of Model RB structure that is similar to graph coloring problems and others. We propose a translation method and three effective complete SAT solving algorithms based on the characterization of Model RB structure. We translate clauses into a graph with exclusive sets and relative sets. In order to reduce search depth, we determine search order using vertex weights and clique in the graph. The results show that our algorithms are much more effective than the best SAT solvers in numerous Model RB benchmarks, especially in those large benchmark instances.

On Optimizing the Satisfiability (SAT) Problem

The satisfiability(SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient optimization algorithms for finding a solution for a satisfiable CNF formula. A new formulation, the Universal SAT problem model, which transforms the SAT problem on Boofean space into an optimization problem on real space has been developed. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the Universal SAT problem. In this paper, we prove that, when the initial solution is sufficiently close to the optimal solution, the steepest descent method has a linear convergence ratio β<1, Newton's method has a convergence ratio of order two, and the convergence ratio of the coordinate descent method is approximately (1-β/m) for the Universal SAT problem with m variables. An algorithm based on the coordinate descent method for the Universal SAT problem is also presented in this paper.

Satisfiability with Index Dependency

We study the Boolean satisfiability problem （SAT） restricted on input formulas for which there are linear arithmetic constraints imposed on the indices of variables occurring in the same clause. This can be seen as a structural counterpart of Schaefer＇s dichotomy theorem which studies the SAT problem with additional constraints on the assigned values of variables in the same clause. More precisely, let k-SAT（m, A） denote the SAT problem restricted on instances of k-CNF formulas, in every clause of which the indices of the last k - m variables are totally decided by the first m ones through some linear equations chosen from A. For example, if A contains i3 = il ＋ 2i2 and i4 = i2 - i1 ＋ 1, then a clause of the input to 4-SAT（2, A） has the form Yi1 V Yi2 V Yi1＋2i2 V yi2-i1＋1, with yi being xi or xi^-. We obtain the following results： 1） If m ≥ 2, then for any set .4 of linear constraints, the restricted problem k-SAT（m, A） is either in P or NP-complete assuming P ≠ NP. Moreover, the corresponding #SAT problem is always #P-complete, and the MAx-SAT problem does not allow a polynomial time approximation scheme assuming P ≠ NP. 2） m = 1, that is, in every clause only one index can be chosen freely. In this case, we develop a general framework together with some techniques for designing polynomial-time algorithms for the restricted SAT problems. Using these, we prove that for any .A, #2-SAT（1, .A） and MAX-2-SAT（1, A） are both polynomial-time solvable, which is in sharp contrast with the hardness results of general #2-SAT and MAX-2-SAT. For fixed k ≥ 3, we obtain a large class of non-trivial constraints .4, under which the problems k-SAT（1, A）, #k-SAT（1, .A） and MAx-k-SAT（1, A） can all be solved in polynomial time or quasi-polynomial time.

An algorithm for solving satisfiability problem based on the structural information of formulas

1 Introduction The propositional satisfiability(SAT)problem is an important and prototypical NP-hard problem in theoretical computer science[1].Many efforts have been made for designing high-performance SAT solvers.The existing practical techniques for solving SAT problems are mainly divided into two categories:complete search technique and stochastic local search technique.

Efficient Static Compaction of Test Patterns Using Partial Maximum Satisfiability

Static compaction methods aim at finding unnecessary test patterns to reduce the size of the test set as a post-process of test generation.Techniques based on partial maximum satisfiability are often used to track many hard problems in various domains,including artificial intelligence,computational biology,data mining,and machine learning.We observe that part of the test patterns generated by the commercial Automatic Test Pattern Generation(ATPG)tool is redundant,and the relationship between test patterns and faults,as a significant information,can effectively induce the test patterns reduction process.Considering a test pattern can detect one or more faults,we map the problem of static test compaction to a partial maximum satisfiability problem.Experiments on ISCAS89,ISCAS85,and ITC99 benchmarks show that this approach can reduce the initial test set size generated by TetraMAX18 while maintaining fault coverage.

Event-Triggered Bipartite Consensus Tracking and Vibration Control of Flexible Timoshenko Manipulators Under Time-Varying Actuator Faults

For bipartite angle consensus tracking and vibration suppression of multiple Timoshenko manipulator systems with time-varying actuator faults,parameter and modeling uncertainties,and unknown disturbances,a novel distributed boundary event-triggered control strategy is proposed in this work.In contrast to the earlier findings,time-varying consensus tracking and actuator defects are taken into account simultaneously.In addition,the constructed event-triggered control mechanism can achieve a more flexible design because it is not required to satisfy the input-to-state condition.To achieve the control objectives,some new integral control variables are given by using back-stepping technique and boundary control.Moreover,adaptive neural networks are applied to estimate system uncertainties.With the proposed event-triggered scheme,control inputs can reduce unnecessary updates.Besides,tracking errors and vibration states of the closed-looped network can be exponentially convergent into some small fields,and Zeno behaviors can be excluded.At last,some simulation examples are given to state the effectiveness of the control algorithms.

Lyapunov Conditions for Finite-Time Input-to-State Stability of Impulsive Switched Systems

Dear Editor,This letter studies finite-time input-to-state stability(FTISS)for impulsive switched systems.A set of Lyapunov-based conditions are established for guaranteeing FTISS property.When constituent modes governing continuous dynamics are FTISS and discrete dynamics involving impulses are destabilizing,the FTISS can be retained if impulsive-switching signals satisfy an average dwell-time(ADT)condition.

PSL的有界模型检验

基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.

Clause-based enhancing mode for tableau algorithm for ALCN

As the tableau algorithm would produce a lot of description overlaps when judging the satisfiabilities of concepts（thus wasting much space）,a clause-based enhancing mode designed for the language ALCN is proposed.This enhancing mode constructs a disjunctive normal form on concept expressions and keeps only one conjunctive clause,and then substitutes the obtained succinctest conjunctive clause for sub-concepts set in the labeling of nodes of a completion tree constructed by the tableau algorithm （such a process may be repeated as many times as needed）.Due to the avoidance of tremendous descriptions redundancies caused by applying ∩- and ∪-rules of the ordinary tableau algorithm,this mode greatly improves the spatial performance as a result.An example is given to demonstrate the application of this enhancing mode and its reduction in the cost of space. Results show that the improvement is very outstanding.