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

合取范式(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更为有效.     

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

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

The complexity of homomorphisms and renamings for minimal unsatisfiable formulas

We investigate the complexity of deciding whether for minimal unsatisfiable formulas F and H there exists a variable renaming, a literal renaming or a homomorphism such that (F) = H. A variable renaming is a permutation of variables. A literal renaming is a permutation of variables which additionally replaces some of the variables by its complements. A homomorphism can be considered as a literal renaming which can map different literals to one literal.     

The complexity of homomorphisms and renamings for minimal unsatisfiable formulas

We investigate the complexity of deciding whether for minimal unsatisfiable formulas F and H there exists a variable renaming, a literal renaming or a homomorphism such that (F)=H. A variable renaming is a permutation of variables. A literal renaming is a permutation of variables which additionally replaces some of the variables by its complements. A homomorphism can be considered as a literal renaming which can map different literals to one literal.     

随机自归约的一个四步零知识证明协议

文中用位提交（ｂｉｔ－ｃｏｍｍｉｔ）等方法，构造了随机归约的一个四步零知识主证明协议，该协议没有附加任何复杂性假设和证明者的计算能力假设，且交互次数量优，适应面最广（二次剩余，离散对数，图同构等问题都在其中）该协议符合知识和语言的证明系统的完备性，完美零知识性等条件，但它不符合知识和语言的证明系统的可靠性定义，文中给出了新的可靠性定义，在实际应用中，该定义是合理的，该协议是可靠的，可用在安全保密，     

A proof procedure for the logic of hereditary Harrop formulas

A proof procedure is presented for a class of formulas in intuitionistic logic. These formulas are the so-calledgoal formulas in the theory of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem for this logic: formulas cannot in general be preprocessed into a form such as the clausal form, and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. An interesting aspect of the formulas we consider here is that this analysis can be carried out in a relatively controlled manner in their context. In particular, the task of finding a proof can be reduced to one of demonstrating that a formula follows from a set of assumptions, with the next step in this process being determined by the structure of the conclusion formula. An acceptable implementation of this observation must utilize unification. However, since our formulas may contain universal and existential quantifiers in mixed order, care must be exercised to ensure the correctness of unification. One way of realizing this requirement involves labelling constants and variables and then using these labels to constrain unification. This form of unification is presented and used in a proof procedure for goal formulas in a first-order version of hereditary Harrop formulas. Modifications to this procedure for the relevant formulas in a higher-order logic are also described. The proof procedure that we present has a practical value in that it provides the basis for an implementation of the logic programming language Prolog.     

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.     

Elementary Definability and Completeness in General and Positive Modal Logic

The paper generalises Goldblatt's completeness proof for Lemmon–Scott formulas to various modal propositional logics without classical negation and without ex falso, up to positive modal logic, where conjunction and disjunction, andwhere necessity and possibility are respectively independent.Further the paper proves definability theorems for Lemmon–Scottformulas, which hold even in modal propositional languages without negation and without falsum. Both, the completeness theorem and the definability theoremmake use only of special constructions of relations,like relation products. No second order logic, no general frames are involved.     

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

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

可验证的基于词典的可搜索加密方案

针对云存储中数据检索和安全问题,提出了一个可验证的基于词典的可搜索加密方案.该方案能够验证搜索结果的完备性.在适应性不可区分安全模型下证明了该方案的安全性.与现有方案相比,该方案具有陷门大小固定、适应性安全、更新无需重新计算、可验证等优势.