基于否证蕴含的极小一阶不可满足子式求解算法

解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.     

一种求解布尔不可满足子式的局部搜索算法

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。     

基于悖论证明与局部搜索的不可满足子式求解算法

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.     

布尔不可满足子式的求解方法研究进展

解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.     

一种基于消解的变量极小不可满足子公式的提取方法

变量极小不可满足(VMU)问题是极小不可满足(MU)问题的一个扩充和延伸.着重研究VMU子公式的提取算法.首先从理论上比较MU和VMU的基本性质,并分析了目前流行的MU子公式提取算法.研究Davis-Putman-消解的基本性质,给出一个判定变量极小不可满足公式的充分必要条件,进而提出一个基于消解的VMU子公式提取算法.此算法可以使用ZBDDs压缩存储消解式,并实现单步多重消解.     

基于SMT的不完全信息游戏求解

不完全信息博弈是人工智能领域的一个重要研究领域.本文提出了一种基于可满足性模理论(Satisfiability Modulo Theories, SMT)的不完全信息游戏求解方法,首先通过情景演算将游戏动态过程描述成对应的约束,并将约束编写成命题逻辑公式,然后将推理问题转化为逻辑公式可满足性问题,调用SMT求解器Z3进行求解.应用表明,本文的算法能有效地推理出游戏的正确结果.     

针对MUS求解问题的加强剪枝策略

极小不可满足子集(minimal unsatisfiable subsets, MUS)的求解是布尔可满足性问题中的一个重要子问题. 对于一个给定的不可满足问题, 其MUS的求解能够反映出问题中导致其不可满足的关键原因. 然而, MUS的求解是一项极其耗时的任务, 不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数, 从而影响算法的求解效率. 提出一种针对MUS求解的加强剪枝策略ABC (accelerating by critical MSS), 依据MSS、MCS、MUS这3者之间的对偶性和碰集关系特点, 提出cMSS和subMUS概念, 并总结出4条性质, 即每个MUS必是subMUS的超集, 进而在避免对MCS的碰集进行求解的情况下有效利用MUS和MCS互为碰集的特征, 有效避免求解碰集时的时间开销. 当subMUS不可满足时, 则subMUS是唯一的MUS, 算法将提前结束执行; 当subMUS可满足时, 则剪枝掉此节点, 进而有效避免对求解空间中的冗余空间进行搜索. 同时, 通过理论证明ABC策略的有效性, 并将其应用于目前最高效的单一化模型算法MARCO和双模型算法MARCO-MAM, 在标准测试用例下的实验结果表明, 该策略可以有效地对搜索空间进行进一步剪枝, 从而提高MUS的枚举效率.     

基于互补概念和搜索图的MUPS求解优化方法

本体调试是人工智能中非标准推理任务之一,对于本体工程具有很重要的意义.本文结合互补概念与基于术语集的搜索图提出极小不可满足子术语集求解的优化方法.首先,通过判断扩展的术语集是否包含互补概念,确定该子术语集是否需要进行概念可满足性检测,可以有效减少推理机的调用次数.接着,根据术语集扩展过程构造一个术语集搜索图,分别采用宽度优先搜索和深度优先搜索策略快速查找不可满足子术语集.该优化方法一方面减少了待测子术语集的规模,另一方面提高了查找不可满足子术语集对应的节点的查找效率.最后,实现了本文给出的各类优化算法并与现有的黑盒优化算法进行了比较.实验效果表明,本文方法从推理机调用次数和待测术语集规模方面均优于现有的MUPS求解方法,能够有效提高求解术语集MUPS的效率.     

基于可满足性模理论的虚拟网映射问题求解

针对物理网络不支持路径分割且物理节点不支持重复映射的虚拟网映射问题，建立以物理网络资源消耗量最小化为目标的整数线性规划模型；基于可满足性模理论，构建这类虚拟网映射问题的SMT公式，并采用SMT求解器求解最优解。实验表明，所提方法能有效提高虚拟网络构建请求的接受率和物理网络提供商的长期收益。     

On exact selection of minimally unsatisfiable subformulae

A minimally unsatisfiable subformula (MUS) is a subset of clauses of a given CNF formula which is unsatisfiable but becomes satisfiable as soon as any of its clauses is removed. The selection of a MUS is of great relevance in many practical applications. This expecially holds when the propositional formula encoding the application is required to have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). While selection of a MUS is a hard problem in general, we show classes of formulae where this problem can be solved efficiently. This is done by using a variant of Farkas' lemma and solving a linear programming problem. Successful results on real-world contradiction detection problems are presented.     

On exact selection of minimally unsatisfiable subformulae

A minimally unsatisfiable subformula (MUS) is a subset of clauses of a given CNF formula which is unsatisfiable but becomes satisfiable as soon as any of its clauses is removed. The selection of a MUS is of great relevance in many practical applications. This expecially holds when the propositional formula encoding the application is required to have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). While selection of a MUS is a hard problem in general, we show classes of formulae where this problem can be solved efficiently. This is done by using a variant of Farkas lemma and solving a linear programming problem. Successful results on real-world contradiction detection problems are presented.     

Extension and equivalence problems for clause minimal formulae

Inspired by the notion of minimal unsatisfiable formulae we first introduce and study the class of clause minimal formulae. A CNF formula F is said to be clause minimal if any proper subformula of F is not equivalent to F. We investigate the equivalence and extension problems for clause minimal formulae. The extension problem is the question whether for two formulae F and H there is some formula G such that F+G is equivalent to H. Generally, we show that these problems are intractable. Then we discuss the complexity of these problems restricted by various parameters and constraints. In the last section we ask several open questions in this area.     

Extension and equivalence problems for clause minimal formulae

Inspired by the notion of minimal unsatisfiable formulae we first introduce and study the class of clause minimal formulae. A CNF formula F is said to be clause minimal if any proper subformula of F is not equivalent to F. We investigate the equivalence and extension problems for clause minimal formulae. The extension problem is the question whether for two formulae F and H there is some formula G such that F + G is equivalent to H. Generally, we show that these problems are intractable. Then we discuss the complexity of these problems restricted by various parameters and constraints. In the last section we ask several open questions in this area.     

NP-completeness of small conflict set generation for congruence closure

The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.     

Improved usability and performance of SMT solvers for debugging specifications

It is now common to construct an extended static checker or software verification system using an SMT theorem prover as the underlying logical verifier. SMT provers have improved significantly in performance over the last several years. However, their usability as a component of software checking and verification systems still has gaps. This paper describes investigations in two areas: the reporting of counterexample information and the testing of vacuity, both of which are important to realistic use of such tools for typical software development. The use of solvers in verification is more effective if the solvers support minimal unsatisfiable cores and incremental construction, evolution and querying of satisfying assignments; current solvers only partially support these capabilities.