极小不可满足公式在多项式归约中的应用

合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式限制于(r,s)-CNF.对于正整数r≥3,有一个临界函数f(r),使得(r,f(r))-CNF中的公式都是可满足的,而(r,f(r)+1)-SAT却是NP-完全的.函数f是否可计算是一个开问题,除了知道f(3)=3,f(4)=4外,只能估计f(r)的界.描述了极小不可满足公式在CNF公式类之间转换中的作用.为使转换过程中引入较少的新变元,给出了CNF公式到3-CNF公式的一种新的转换方法,对于长度为l(＞3)的子句,仅需引入|l/2|个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.     

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

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

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

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

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

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

极小布尔不可满足子式的提取算法

研究了极小布尔不可满足子式的提取算法,它分为近似算法和精确算法两种．文中就精确算法提出了局部预先赋值的优化方案,并且在理论上证明了该算法的正确性;通过实验显示了此算法可以获得更高的效率．通过模拟实验观察到,利用完法计算法进行近似提取的一个有趣现象,即随着公式密度的增加,算法的提取误差会趋于下降．     

基于同态hash的数据多副本持有性证明方案

为检查云存储中服务提供商(CSP)是否按协议完整地存储了用户的所有数据副本,在分析并指出一个基于同态hash的数据持有性证明方案安全缺陷的基础上,对其进行了改进和扩展,提出了一个多副本持有性证明方案。为实现多副本检查,将各副本编号与文件连接后利用相同密钥加密以生成副本文件,既有效防止了CSP各服务器的合谋攻击,又简化了用户和文件的授权访问者的密钥管理;为提高检查效率,利用同态hash为数据块生成验证标签,实现了对所有副本的批量检查;为保证方案安全性,将文件标志和块位置信息添加到数据块标签中,有效防止了CSP进行替换和重放攻击。安全性证明和性能分析表明,该方案是正确和完备的,并具有计算、存储和通信负载低,以及支持公开验证等特点,从而为云存储中数据完整性检查提供了一种可行的方法。     

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

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

一个正则NP-完全问题及其不可近似性

通过一个适当的归约变换,可以将一个CNF (conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性.带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性.极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足.借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换.这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4.因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题.     

变量极小不可满足在模型检测中的应用

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.     

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

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

基于信息系统属性同态的数据压缩

数据压缩是数据处理的一个重要主题,同态是实现数据压缩的一种有效工具。根据信息系统属性集及其上的依赖关系,定义了信息系统属性同构和信息系统属性同态的概念。研究了信息系统属性同态的性质,利用属性等价关系诱导出了信息系统属性理想同态,应用信息系统属性理想同态实现了信息系统属性集的无损压缩。最后通过比较原信息系统与同态像信息系统的距离,给出了度量任意属性同态理想程度的方法。     

基于哈希证明系统的区块链两方椭圆曲线数字签名算法研究

椭圆曲线数字签名算法(ECDSA)是区块链密码学技术中常见的数字签名之一,其在加密货币、密钥身份认证等方面已被广泛应用.然而当前的区块链ECDSA算法灵活性较低、匿名性较弱且分散性不高,性能相对高效的应用实例也十分有限.基于哈希证明系统,文章提出一种适用于区块链的两方椭圆曲线数字签名算法.通过给定签名算法的数理逻辑及其...     

秘密同态技术研究及其算法实现

在数据库加密系统中,秘密同态技术(privacy honaonlorphisrn)能够对一些敏感的、重要的数据直接在密文的状况下进行操作,从而有效地保护这些数据。该文从实际工作出发,阐明了秘密同态技术的概念、算法、实现及其实现过程中的一些关键点。     

Dialogue Systems as Proof Editors

This paper shows how a dialogue system for information-seekingdialogues can be implemented in a type-theory-based syntax editor,originally developed for editing mathematical proofs.The implementation gives a simple logical metatheory tosuch dialogue systems and also suggests new functions forthem, e.g., a local undo operation. The method developed provides alogically based declarative way of implementing simple dialoguesystems that is easy to port to new domains.     

Complexities of Homomorphism and Isomorphism for Definite Logic Programs

A homomorphism (?) of logic programs from P to P' is a function mapping Atoms(P) to Atoms(P') and it preserves complements and program clauses. For each definite program clause a←a1,...,an∈P it implies that (?)(a)←(?)(a1),...,(?)(an) is a program clause of P'. A homomorphism (?) is an isomorphism if (?) is a bijection. In this paper, the complexity of the decision problems on homomorphism and isomorphism for definite logic programs is studied. It is shown that the homomorphism problem (HOM-LP) for definite logic programs is NP-complete, and the isomorphism problem (ISO-LP) is equivalent to the graph isomorphism problem (GI).     

ML Systems: A Proof Theory for Contexts

In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches.