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.

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.

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.

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.

Formal Verification under Unknown Constraints

We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) formulas.Furthermore,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.

Enhancing SAT-Based Test Pattern Generation

This paper presents modeling tools based on Boolean satisfiability (SAT) to solve problems of test generation for combinational circuits. It exploits an added layer to maintain circuit-related information and value justification relations to a generic SAT algorithm. It dovetails binary decision graphs (BDD) and SAT techniques to improve the efficiency of automatic test pattern generation (ATPG). More specifically, it first exploits inexpensive reconvergent fanout analysis of circuit to gather information on the local signal correlation by using BDD learning, then uses the above learned information to restrict and focus the overall search space of SAT-based ATPG. Its learning technique is effective and lightweight. The experimental results demonstrate the effectiveness of the approach.

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.

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.

Test Generation with Unspecified Variable Assignments

ATPG for very large scale integrated circuit designs is an important problem in industry. With the advent of SOC designs, testing and verification of the core-based designs become a challenging problem. This paper presents an algebraic test generation algorithm with unspecified variable assignments. Given a stuck at fault of the circuit with unspecified signals, the proposed algorithm uses a new encoding scheme for unspecified variable assignments, and solves the Boolean satisfiability formula representing the Boolean difference to obtain a test pattern. Experimental results demonstrate the efficiency and feasibility of the proposed algorithm.