MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g., model-checking, circuit testing, propositional planning) by encoding into SAT. However, a purely Boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in linear arithmetic logic (LAL), that is, the Boolean combination of propositional variables and linear constraints over numerical variables. In this paper we present MathSAT, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve MathSAT in two different directions. First, the top‐level line procedure is enhanced and now features a tighter integration between the Boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of Boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way. Second, the mathematical solver is based on layering; that is, the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes call of the subsequent solvers superfluous. We provide a through experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of MathSAT is often superior to its competitors, both on LAL and in the subclass of difference logic. This work has been partly supported by ISAAC, a European-sponsored project, contract no. AST3-CT-2003-501848; by ORCHID, a project sponsored by Provincia Autonoma di Trento; and by a grant from Intel Corporation. The work of T. Junttila has also been supported by the Academy of Finland, project 53695. S. Schulz has also been supported by a grant of the Italian Ministero dell'Istruzione, dell'Università e della Ricerca and the University of Verona.     

An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems

This paper presents a bounded model checking tool called Hydlogic{\texttt{Hydlogic}} for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our Hydlogic{\texttt{Hydlogic}} implementation successfully handled several examples including those with nonlinear constraints.     

基于分组的启发式SAT新算法——DC&DS算法

目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。     

一个适于形式验证的ATPG引擎

自动测试产生(ATPG)不仅应用于芯片测试向量生成，也是芯片设计验证的重要引擎之一．提出了一种组合电路测试产生的代数方法，既可作为组合验证的ATPG引擎，又可用于通常的测试产生．该算法充分发挥了二叉判决图(BDD)及布尔可满足性(SAT)的优势，通过启发式策略实现SAT算法与BDD算法的交替，防止因构造BDD可能导致的内存爆炸，而且使用增量的可满足性算法，进一步提高了算法的效率．实验结果表明了该算法的可行性和有效性．     

Efficient software product-line model checking using induction and a SAT solver

Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques.     

GridSAT: Design and Implementation of a Computational Grid Application

We present the latest instantiation of GridSAT [1], a distributed and complete satisfiability solver that is explicitly designed to aggregate Grid resources for application performance. GridSAT was previously shown to outperform the state-of-the-art sequential solvers. In this work, we explore the unprecedented solving power GridSAT enables through algorithmic and implementation innovations. We describe the implementation techniques that allow GridSAT to leverage a variety of high-end batch-scheduled resources, clusters, interactive workstations, and personal computing resources through autonomous scheduling, checkpoint scheduling, and work migration. These innovations have allowed GridSAT to solve a set of ‘hard’ and previously unsolved industrial and community satisfiability problems. In addition to this new solution power, GridSAT also outperforms the otherwise highest performance general solvers on the annual SAT competition [21] performance benchmarks.This work was supported by grants from the National Science Foundation, numbered CAREER-0093166, EIA-9975020, ACI-0103759, and CCR-0331654 and by the San Diego Supercomputer Center and the TeraGrid project.     

Simulating Circuit-Level Simplifications on CNF

Boolean satisfiability (SAT) and its extensions have become a core technology in many application domains, such as planning and formal verification, and continue finding various new application domains today. The SAT-based approach divides into three steps: encoding, preprocessing, and search. It is often argued that by encoding arbitrary Boolean formulas in conjunctive normal form (CNF), structural properties of the original problem are not reflected in the CNF. This should result in the fact that CNF-level preprocessing and SAT solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural SAT instance representations such as Boolean circuits. Motivated by this, various simplification techniques and intricate CNF encodings for circuit-level SAT instance representations have been proposed. On the other hand, based on the highly efficient CNF-level clause learning SAT solvers, there is also strong support for the claim that CNF is sufficient as an input format for SAT solvers. In this work we study the effect of CNF-level simplification techniques, focusing on SatElite-style variable elimination (VE) and what we call blocked clause elimination (BCE). We show that BCE is surprisingly effective both in theory and in practice on CNF formulas resulting from a standard CNF encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circuit-level simplifications and previously suggested polarity-based CNF encodings. We also show that VE can achieve many of the same effects as BCE, but not all. On the other hand, it turns out that VE and BCE are indeed partially orthogonal techniques. We also study the practical effects of combining BCE and VE for reducing the size of formulas and on the running times of state-of-the-art SAT solvers. Furthermore, we address the problem of how to construct original witnesses to satisfiable CNF formulas when applying a combination of BCE and VE.     

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

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

基于改进连续时间动态系统的模拟SAT求解器

针对布尔可满足性问题的高效求解进行了研究。首先,通过对k-SAT问题和基于耦合常微分方程形式的确定性连续时间动态系统的分析,提出了一种基于时延信息形式的改进连续时间动态系统方程,以保持集中搜索特性;然后,提出了实现该系统方程的三个主要组件即信号动态电路、辅助变量电路和数字验证电路的模拟设计。在信号动态电路的设计中,设计了一种获得更高性能、更小面积和更低功耗的模拟硬件形式;在提出的辅助变量电路和数字验证电路的模拟硬件设计中,实现了避免梯度下降搜索陷入无解和确定给定问题的解是否已经找到的目标;同时提出了降低面积和功耗的可替代辅助变量电路的两种设计方案。仿真实验结果表明,提出的新的模拟SAT求解器不仅是有效的,而且相比于单一软件算法实现的SAT求解器和其他硬件类SAT求解器具有更高的加速性能和更低的功耗。     

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

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

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

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

一种基于SAT的运算电路查错方法

基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句技术的E-SAT求解器进行求解.实验表明该方法自动化程度高,能处理大规模的运算电路,有较强的查找错误能力.     

电路宽度制导的布尔推理

在基于逻辑电路的布尔推理过程中，经常用到二又判决图(BDD)与布尔可满足性(SAT)相结合的算法．由于电路宽度能很好地反映电路的复杂性，提出了一种基于电路宽度的启发式策略，根据电路宽度来实现SAT算法与BDD算法的交替．充分发挥两者的优势，不仅可以防止因构造BDD可能导致的内存爆炸，而且还能避免SAT算法可能遇到的超时现象．与以往同类策略相比，该启发式策略更节省计算资源，提高算法性能．针对组合电路的测试产生实验，证实了其在布尔推理中的效率．     

Parallel SAT Solving on Peer-to-Peer Desktop Grids

Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to one of the most challenging environments for parallel computing—Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as non-uniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers.     

基于不完全算法的并行FPGA SAT求解器

可满足性问题是计算机理论与应用的核心问题。在FPGA上提出了一个基于不完全算法的并行求解器pprobSAT+。使用多线程的策略来减少相关组件的等待时间,提高了求解器效率。此外,不同线程采用共用地址和子句信息的数据存储结构,以减少片上存储器的资源开销。当所有数据均存储在FPGA的片上存储器时,pprobSAT+求解器可以达到最佳性能。实验结果表明,相比于单线程的求解器,所提出的pprobSAT+求解器可获得超过2倍的加速比。     

Accelerating Bounded Model Checking of Safety Properties

Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search for a counterexample in executions whose length is bounded by some integer k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures are based on general-purpose heuristics that are designed for any propositional formula. We show how the unique characteristics of BMC invariant formulas (G p) can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs prove their efficiency in many of the hard test cases, in comparison to both the standard SAT procedure and a BDD-based model checker.     

最坏情况下Min-2SAT问题的上界

最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题,在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此对MinSAT问题进行研究.针对Min-2SAT问题提出算法MinSATAlg,该算法首先利用化简算法Simplify对公式进行化简,然后通过分支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Min-2SAT问题可在O(1.134 3m)时间内求解,对于每个变量至多出现在3个2-子句中的情况,得到最坏情况下的上界为O(1.122 5n),其中n为变量的数目.     

SMELS: Satisfiability Modulo Equality with Lazy Superposition

We consider the problem of checking satisfiability of quantified formulae in First Order Logic with Equality. We propose a new procedure for combining SAT solvers with Superposition Theorem Provers to handle quantified formulae in an efficient and complete way. In our procedure, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SAT solver, which runs a DPLL method to build partial models. The partial model is reduced, and then passed to a Superposition procedure, along with justifications of literals. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the ground literals and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of our procedure, using a nontrivial modification of the Bachmair and Ganzinger’s model generation technique. We have implemented a theorem prover based on this idea by reusing state-of-the-art SAT solver and Superposition Theorem Prover. Our theorem prover inherits the best of both worlds: a SAT solver to handle ground clauses efficiently, and a Superposition theorem prover which uses powerful orderings to handle the nonground clauses. Experimental results are promising, and hereby confirm the viability of our method.