命题逻辑可满足性问题的算法分析

1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。     

基于一阶逻辑的可满足求解方法研究进展

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。     

利用命题逻辑最大可满足性的冗余通孔最优插入方法

在纳米尺度的集成电路设计中,冗余通孔插入是减轻通孔失效造成良率降低问题的常用技术.文中将最优冗余通孔插入问题规约到命题逻辑最大逻辑可满足性(maximum satisfiability, Max SAT)问题,并利用完备求解器求取最优解.MaxSAT问题是一个NP困难问题,采用2种方法来降低求解难度;一是预选取方法,将提前确定的不与其他通孔产生冲突的冗余通孔作为部分解来降低问题的规模;二是分治法,根据连通分量将原问题划分成多个子问题分别求解,降低求解的复杂度.同时,从理论上证明这2种方法能够保证解的最优性.在2019年国际物理设计研讨会(ISPD)举办的详细布线比赛基准测试集上进行实验的结果表明,所提出的插入方法带来的时间开销不到详细布线时间的5%,算法的最优性保证了最大化解决插入冲突后的插入率,在所有可插入通孔中,冗余通孔的插入率为67%～87%.     

分支时态描述逻辑ALC-CTL及其可满足性判定

时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL。该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言。最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别。通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。     

命题逻辑提升到一阶逻辑上的子句消去方法

在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。     

可满足性模理论综述

可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。     

二维逻辑PPTLSL的可满足性检查

由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(Separation Logic)与命题投影时序逻辑PPTL(Propositional Projection Temporal Logic),能够描述和验证操作链表的指针程序的时序性质.本文简要回顾了PPTLSL的相关理论,并详细介绍工具SAT-PPTLSL的工作原理.该工具主要利用PPTLSL与PPTL之间构建起来的“同构”关系进行PPTLSL公式的可满足性检查.此外,本文结合一些实例展示了SAT-PPTLSL的执行过程,并通过实验分析了关键参数对SAT-PPTLSL执行效率的影响.     

可满足性问题的研究综述

对SAT问题及其各种约束子问题进行分类并给出具体定义,着重介绍常规SAT问题、最大可满足性问题（MAX—SAT）和参数化SAT问题的相关算法,并对参数算法中运用的技术进行分析和比较,提出一些SAT问题研究中值得关注的几个方面。     

求解难可满足性问题的混合算法

提出了一个求解难可满足性问题的简单混合算法．拟人和禁忌表两个策略被给出．数值实验表明，对于一类公认比较难的可满足性问题，该算法胜过目前据认为是最好方法之一的NOVELTY算法．     

可满足性问题的一种DNA表面计算模型

可满足性问题的一种DNA表面计算模型是一种特殊的DNA计算方法,该模型是采用荧光标记的策略和荧光猝灭技术,通过观察荧光灭光情况排除非解,从而有效的解决可满足性问题(SAT).该模型方法具有错误率低、编码简单、读取方便等很好的性能,能够大大减少实验过程中的错差.     

Algorithms for Testing Satisfiability Formulas

The present paper presents algorithms for testing satisfiabily of clausalformulas in the propositional logic and the firs-order logic. The algorithmbased on the enumeration of solutions for testing the satisfiability ofpropositional formula, has already been given by K. Iwama, O. Dubois. Theoriginality in this paper is to combine this algorithm to other procedures,especially with the pure-literal literal and the one-literal rule, and also theone which consists in changing any formulas in formulas bounded. Thealgorithm based on the enumeration of the solution combined to theseprocedures is more efficient. The algorithm based on the concept ofresolutive derivation from Skolem normal form of formula in first-order logic, has already been given. The idea in present's paper is tocombined to this algorithm to process of elimination of tautological clausesand process of elimination of subsumed clauses.     

语义网的一阶逻辑推理技术支持

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.     

Efficient data structures for backtrack search SAT solvers

The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing data structures, since different solvers are often characterized by fairly different algorithmic organizations and techniques, and by different search strategies and heuristics. This paper aims the evaluation of data structures for backtrack search SAT solvers, under a common unbiased SAT framework. In addition, advantages and drawbacks of each existing data structure are identified. Finally, new data structures are proposed, that are competitive with the most efficient data structures currently available, and that may be preferable for the next generation SAT solvers.     

Efficient data structures for backtrack search SAT solvers

The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing data structures, since different solvers are often characterized by fairly different algorithmic organizations and techniques, and by different search strategies and heuristics. This paper aims the evaluation of data structures for backtrack search SAT solvers, under a common unbiased SAT framework. In addition, advantages and drawbacks of each existing data structure are identified. Finally, new data structures are proposed, that are competitive with the most efficient data structures currently available, and that may be preferable for the next generation SAT solvers.     

Probability logic and optimization SAT: The PSAT and CPA models

Both probabilistic satisfiability (PSAT) and the check of coherence of probability assessment (CPA) can be considered as probabilistic counterparts of the classical propositional satisfiability problem (SAT). Actually, CPA turns out to be a particular case of PSAT; in this paper, we compare the computational complexity of these two problems for some classes of instances. First, we point out the relations between these probabilistic problems and two well known optimization counterparts of SAT, namely Max SAT and Min SAT. We then prove that Max SAT with unrestricted weights is NP-hard for the class of graph formulas, where Min SAT can be solved in polynomial time. In light of the aforementioned relations, we conclude that PSAT is NP-complete for ideal formulas, where CPA can be solved in linear time.     

Probability logic and optimization SAT: The PSAT and CPA models

Both probabilistic satisfiability (PSAT) and the check of coherence of probability assessment (CPA) can be considered as probabilistic counterparts of the classical propositional satisfiability problem (SAT). Actually, CPA turns out to be a particular case of PSAT; in this paper, we compare the computational complexity of these two problems for some classes of instances. First, we point out the relations between these probabilistic problems and two well known optimization counterparts of SAT, namely Max SAT and Min SAT. We then prove that Max SAT with unrestricted weights is NP-hard for the class of graph formulas, where Min SAT can be solved in polynomial time. In light of the aforementioned relations, we conclude that PSAT is NP-complete for ideal formulas, where CPA can be solved in linear time.     

半扩展规则下分解的定理证明方法

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.     

Generating Instances for MAX2SAT with Optimal Solutions

A test instance generator (an instance generator for short) for MAX2SAT is a procedure that produces, given a number n of variables, a 2-CNF formula F of n variables (randomly chosen from some reasonably large domain), and simultaneously provides one of the optimal solutions for F. We propose an outline to design an instance generator using an expanding graph of a certain type, called here an "exact 1/2-enlarger". We first show a simple algorithm for constructing an exact 1/2-enlarger, thereby deriving one concrete polynomial-time instance generator GEN. We also show that an exact 1/2-enlarger can be obtained with high probability from graphs randomly constructed. From this fact, we propose another type of instance generator RGEN; it produces a 2-CNF formula with a solution which is optimal for the formula with high probability. However, RGEN produces less structured formulas and a much larger class of formulas than GEN. In fact, we prove the NP-hardness of MAX2SAT over the set of 2-CNF formulas produced by RGEN.     

The Propositional Formula Checker HeerHugo

HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. The underlying algorithm is based on a specific breadth-first search procedure, with several enhancements including unit resolution and 2-satisfiability tests. Its main ingredient is the branch/merge rule inspired by an algorithm proposed by Stållmarck, which is protected by a software patent. In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results.