Combining finite learning automata with GSAT for the satisfiability problem

A large number of problems that occur in knowledge-representation, learning, very large scale integration technology (VLSI-design), and other areas of artificial intelligence, are essentially satisfiability problems. The satisfiability problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. The growing need for more efficient and scalable algorithms has led to the development of a large number of SAT solvers. This paper reports the first approach that combines finite learning automata with the greedy satisfiability algorithm (GSAT). In brief, we introduce a new algorithm that integrates finite learning automata and traditional GSAT used with random walk. Furthermore, we present a detailed comparative analysis of the new algorithm's performance, using a benchmark set containing randomized and structured problems from various domains.     

A Taxonomy of Exact Methods for Partial Max-SAT

Partial Maximum Boolean Satisfiability (Partial Max-SAT or PMSAT) is an optimization variant of Boolean satisfiability (SAT) problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many real-life problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis-Putnam-Logemann-Loveland (DPLL) procedure and Branch and Bound (B&B) algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007～2011 Max-SAT evaluations, emphasizing on the most promising research directions.     

Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

Much excitement has been generated by the success of stochastic local search procedures at finding solutions to large, very hard satisfiability problems. Many of the problems on which these procedures have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Approaches to solving non-Boolean satisfiability problems fall into two categories. In the direct approach, the problem is tackled by an algorithm for non-Boolean problems. In the transformation approach, the non-Boolean problem is reformulated as an equivalent Boolean problem and then a Boolean solver is used. This paper compares four methods for solving non-Boolean problems: one direct and three transformational. The comparison first examines the search spaces confronted by the four methods, and then tests their ability to solve random formulas, the round-robin sports scheduling problem, and the quasigroup completion problem. The experiments show that the relative performance of the methods depends on the domain size of the problem and that the direct method scales better as domain size increases. Along the route to performing these comparisons we make three other contributions. First, we generalize Walksat, a highly successful stochastic local search procedure for Boolean satisfiability problems, to work on problems with domains of any finite size. Second, we introduce a new method for transforming non-Boolean problems to Boolean problems and improve on an existing transformation. Third, we identify sufficient conditions for omitting at-least-one and at-most-one clauses from a transformed formula. Fourth, for use in our experiments we propose a model for generating random formulas that vary in domain size but are similar in other respects.     

基于布尔可满足性的组合电路ATPG算法

布尔可满足性被深入研究并广泛应用于电子设计自动化等领域。该文提出了一种基于布尔可满足性的组合电路ATPG改进算法。在采用当前最新布尔可满足性求解程序加速策略的基础上,比如冲突驱动训练、冲突导向回跳和重启动技术等,引入电路结构信息来实现基于结构的分支决策。通过新增的电路结构信息层,布尔可满足性求解程序只需稍加修改,就能利用和及时更新此信息。最后给出的实验结果表明了算法的可行性和有效性。     

Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas

We solve the problem of constructing extended finite state machines with execution scenarios and temporal formulas. We propose a new algorithm pstMuACO that combines a scenario filtering procedure, an exact algorithm efsmSAT for constructing finite state machines from execution scenarios based on a reduction to the Boolean satisfiability problem, and a parallel ant colony algorithm pMuACO. Experiments show that constructing several initial solutions for the ant colony algorithm with reduced sets of scenarios significantly reduces the total time needed to find optimal solutions. The proposed algorithm can be used for automated construction of reliable control systems.     

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).     

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).     

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 the Expression Complexity of Equivalence and?Isomorphism of?Primitive Positive Formulas

We study the complexity of equivalence and isomorphism on primitive positive formulas with respect to a given structure. We study these problems for various fixed structures; we present generic hardness and complexity class containment results, and give classification theorems for the case of two-element (boolean) structures.     

Logical and schematic characterization of complexity classes

We consider classes of well-known program schemes from a complexity theoretic viewpoint. We define logics which express all those problems solvable using our program schemes and show that the class of problems so solved or expressed coincides exactly with the complexity classPSPACE (our problems are viewed as sets of finite structures over some vocabulary). We derive normal form theorems for our logics and use these normal form theorems to show that certain problems concerning acceptance and termination of our program schemes and satisfiability of our logical formulae arePSPACE-complete. Moreover, we show that a game problem, seemingly disjoint from logic and program schemes, isPSPACE-complete using the results described above. We also highlight similarities between the results of this paper and the literature, so providing the reader with an introduction to this area of research.     

一类布尔方程组的可满足性阈值研究*

以一类布尔方程组形式的NP问题可满足性阈值估计为研究目的,通过将高斯消去算法与摘叶算法相结合的方法给出了一种求解该问题的完全算法,并通过不同参数条件下对大量随机实例进行数值实验得到了原问题可满足性阈值的算法估计值。所得研究结果不仅首次给出了该问题的可满足性阈值估计,而且可以作为相关启发式完全算法的设计依据。     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem — they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

Solving SAT problem by heuristic polarity decision-making algorithm

This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability (SAT). The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many "real-life" instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem – they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.     

Modular verification of software components in C

We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the counterexample guided abstraction refinement (CEGAR) paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, weak simulation is checked via a reduction to Boolean satisfiability. MAGIC has been interfaced with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel, the OpenSSL toolkit, and several industrial strength benchmarks.     

An overview of parallel SAT solving

Boolean satisfiability (SAT) solvers are currently very effective in practice. However, there are still many challenging problems for SAT solvers. Nowadays, extra computational power is no longer coming from higher processor frequencies. At the same time, multicore architectures are becoming predominant. Exploiting this new architecture is essential for the evolution of SAT solvers. Due to the increasing interest in parallel SAT solving, it is important to give an overview of what has been done so far. This paper presents an overview of parallel SAT solving and it is expected to be a valuable document for researchers in this field. This overview covers the main topics of parallel SAT solving, namely, different approaches and a variety of clause sharing strategies. Additionally, an evaluation of multicore SAT solvers is presented, showing the evolution of multicore SAT solvers over the last years.     

Automatic Construction and Verification of Isotopy Invariants

We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Isotopism is an important generalisation of isomorphism, and is studied by mathematicians in domains such as loop theory. This extension was not straightforward, and we had to solve two major technical problems, namely, generating and verifying isotopy invariants. Concentrating on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on subblocks. In addition, given the complexity of the theorems that verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an interplay of computer algebra, model generation, theorem proving, and satisfiability-solving methods. To demonstrate the power of the approach, we generate isotopic classification theorems for loops of size 6 and 7, which extend the previously known enumeration results. This work was previously beyond the capabilities of automated reasoning techniques. The author’s work was supported by EPSRC MathFIT grant GR/S31099.     

基于硬件可编程逻辑的SAT求解算法研究与进展

布尔可满足性SAT问题作为第一个被证明的NP完全问题,是计算机理论与应用的核心问题,有着重要的应用价值,因此近年来涌现了各种各样SAT求解器。但是,SAT求解器的运算效率始终是影响其应用的关键因素,所以利用硬件的高性能与并行性来加速SAT求解过程已成为验证领域的一个研究热点。归纳总结了在SAT求解过程中,利用硬件现场可编程门逻辑FPGA的并行性和灵活性加速求解过程的各种算法研究,着重总结分析了应用型SAT求解器的加速策略。通过对各种方法的深入分析,指出它们的优缺点,为未来的研究提供了思路。     

Satisfiability solving for software verification

Declarative techniques for software verification require the availability of scalable, predictable, and flexible satisfiability solvers. We describe our approach to build such solvers by combining equational theorem proving, Boolean solving, arithmetic reasoning, and some transformations of the proof obligations. The proposed techniques have been implemented in a system called haRVey and the viability of the approach is shown on proof obligations generated in the certification of aerospace code.