可满足性

摘要： 随着计算机求解问题越加复杂,问题在转化为命题逻辑子句集包含的冗余信息也越来越多,浪费计算机大量的储存空间和搜索解的时间,因此,对于冗余信息的删减有助于提高计算机求解问题的效率.针对命题逻辑子句集化简问题,在原有冗余性质P、RP基础上,提出多种扩展的、具有性质HRP、ARP的子句消去方法,并通过将不对称文字添加前置方法与命题逻辑集合封锁(SET BC )、蕴涵模归结原则(IMR)结合,分别提出不对称集合封锁( ASET BC )消去方法和不对称蕴涵模归结(AIMR)原则.最后,提出 L -集合蕴涵模归结( L -SET IMR )原则和 L -不对称集合蕴涵模( L -ASET IMR )原则.所提出的方法丰富了命题逻辑中冗余性子句消去理论和方法.

摘要： 一阶逻辑是公理系统的标准形式逻辑之一,其中包含的程度化推理等研究内容,是一个研究热点也是难点.文中从一阶逻辑演算的语义理论出发,利用可满足性及完备性定理研究了一阶逻辑中公理化真度.首先给出并、交运算可满足性的定义,其次说明了两个特殊公式与逻辑有效公式以及定理的关系,最后得出与公式等价的前束范式.上述结果将为谓词逻辑程度化研究做准备.

摘要： 提出了一种云环境下网络感知的虚拟机分配问题的求解方法,该方法能求解带有任务优先级和强制任务的最大虚拟机分配问题等5类问题.该方法通过将虚拟机分配问题编码成对应的SAT类问题,并调用现有的SAT类求解器进行求解,可以更有效地解决较大规模的虚拟机分配问题.最后,通过实验验证了本文算法的合理性和有效性.通过与现有算法在以上5类问题中进行对比,表明了本文算法具有更高的求解效率和更大的求解规模.

摘要： #WS(≠)是互斥约束工作流可满足性的量化问题,与第三方环境中有重要意义的资源弹性密切相关.为克服其求解性能瓶颈,本文利用模式回溯法的解空间压缩特性和两层求解机制,提出了一种真实可行解的数量定界方法.它对模式回溯法的结构进行扩展,实现完全可行模式的遍历和统计.对其中每个模式,计算其资源指派二分图上匹配数量的界.再汇总二者,给出#WS(≠)的上、下界.随机生成数据集上的实验表明,在高资源配比和低约束密度条件下,本文算法相对现有算法有比较突出的时间和空间性能,且其给出的上界相当接近于准确值.

摘要： 德国著名管理理论学家马克斯·韦伯指出,在所有社会中,包括中国、印度和伊斯兰国家,获利的贪婪都普遍存在,但是以获利为至善却未曾出现过。“人心不足,蛇吞象”,人性欲望具有不可满足性,给予国企高管再多的物质奖励,都难以满足贪欲太重的人。通过分析腐败案发现,从贪污几百万元到几千万元,从几亿元到几十亿元,几辈子都花不完的钱,还是收不住手。贪欲太重,人的价值观出了问题,什么激励方式都是无效的。

摘要： 针对命题逻辑中逻辑公式的某个单元子句及其负文字和冗余子句,给出了含单元子句的子句集的等价条件,同时刻画了子句集中文字和子句的冗余性,得到了一些冗余文字和冗余子句的判定方法,还提出了与子句集可满足性的等价条件.所提方法可以使命题逻辑的逻辑公式更简单,为命题逻辑中逻辑公式的简化提供一定的理论支撑.

摘要： 基于模型诊断作为克服第1代诊断系统的缺陷而出现的智能诊断推理技术,现已成为十分活跃的人工智能研究分支,随着相关技术的不断发展,应用愈加广泛.其中,大多数研究集中于诊断求解过程,而诊断解的极小性检测方法保证了最终求得诊断解的极小性,也是问题求解过程中至关重要的一步.传统诊断解的极小性判定过程是将新求得的诊断解与已有诊断集合中的诊断解依次比较,检查是否有新得诊断解的超集或子集来判定极小性,这种方法随着求解过程中得到的诊断解数量增多,检测难度逐渐提高,耗时也随之增大.为解决此问题,提出了一种基于子集一致性检测的诊断解极小性判定的新方法:子集一致性(subset consistency detection,SCD)方法.通过对诊断解少数几个子集的一致性检测来给出该诊断解的极小性判定,避免了求解过程中诊断解集合增大对效率的影响.SCD方法可应用于许多高效的诊断方法,如GD(grouped diagnosis)和ACDIAG (abstract circuit diagnosis)方法,算法效率均有所提高.

摘要： 布尔公式的最小纠正集MCS是子句的集合.对于一个不可满足公式,移除MCS后,所得到的新公式可满足.任一MCS中的子句保留在公式中,所得到的新公式不可满足.通过求解MCS并调整约束集合,能够求解最小不可满足核心、MaxSAT问题和最大(小)可满足解问题;还能够应用于故障定位、模型检查配置优化等实际问题中.提出了一种基于不可满足原因的MCS求解算法,实现了相应的CUC工具.通过与目前最好的MCS求解工具LBX进行比较,得到了CUC性能优于LBX的结论.CUC比LBX平均多解出5％(65个)的公式.对于CUC和LBX均可解出的公式,CUC的平均求解时间比LBX快2.5倍.

摘要： 交替投影时序逻辑(alternating projection temporal logic,简称APTL)公式简单易懂,表达能力强;不仅可以描述经典时序逻辑LTL可以描述的性质,而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.根据检查APTL公式的可满足性的方法,开发实现了工具APTL2BCG.具体细节如下:首先,利用公式P的范式构造P的标记范式图(labeled normal form graph,简称LNFG);然后,将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机(generalized alternating Büchi automaton over concurrent game structure,简称GBCG);最后,将GBCG转化为基于并发博弈结构的交替Büchi自动机(alternating Büchi automaton over concurrent game structure,简称BCG)并且化为最简形式并检查公式P的可满足性.%Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power.It is able to express not only properties specified in classical temporal logic LTL,but also interval related sequential and periodical properties,as well as game related properties of open systems and multi-agent systems.To verify whether a system satisfies an APTL formula,the satisfiability of the APTL formula should be checked.In this paper,based on the method for checking satisfiability of an arbitrary APTL formula provided,a supporting tool APTL2BCG has been developed.The details of implementation are given as follows.Firstly,LNFG of P is constructed according to the normal form of the formula P.Then,the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG).Finally,the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG,and the BCG is simplified for checking the satisfiability of the formula P.

摘要： 检验查询可满足性是XML文档查询的一个重要问题。Active XML(AXML)文档在XML文档中引入嵌入式Web服务,增强了文档的动态性和灵活性,同时也为现有文档查询可满足性问题的解决方法提出了新的要求和挑战。研究了模式约束下的AXML文档查询可满足性问题,给出了AXML查询可满足性问题的形式化定义,基于树自动机理论,针对XPath树模式查询片段{"/,//,[]"},提出了一种多项式时间的AXML文档查询可满足性检验算法。实验数据表明,提出的算法在查询过程中以较小的代价显著地节省查询处理时间.

摘要： 基于可满足性(SAT)的模型检验技术已逐渐成为主流的形式验证技术.在RTL,SAT问题的复杂性表现在位(bit)和字(word)数据类型并存和多样化的约束关系。其中,对数据通路的约束求解尤为关键.本文提出采用二元CSP来求解RTL数据通路的可满足性问题,并给出了算法的流程以及流程中每个步骤的实现方法。我们初步实现了算法,并对实验进行了设计.实验结果表明,即使是在没有采取很多优化策略的条件下,基于CSP的方法仍有较好的性能.这说明了本文方法的可行性和进一步研究的价值.

摘要： 本文考虑十八元非链的格值命题逻辑系统L18P(X)下的归结方法.首先提出了基于超滤的归结原理,得到归结删除原理,讨论了格值逻辑公式的可满足性;其次研究了它的可靠性.

摘要： 时序描述逻辑能够通过概念(或个体)问的时序关系描述动态领域的时序行为。时序概念的表现形式具有多样性，而其推理算法却常常是不可判定的。本文提出时序描述逻辑TL-SI，将时序网络间的蕴含算法、时序概念间的蕴含算法以及非时序概念的Tableau算法有机结合起来，并证明了三种算法的可靠性和完备性。rn 该逻辑可以有效表示动作行为，实现了可判定的逻辑推理，为语义Web服务的行为描述提供了有力支持。

摘要： 时序描述逻辑能够通过概念(或个体)问的时序关系描述动态领域的时序行为。时序概念的表现形式具有多样性，而其推理算法却常常是不可判定的。本文提出时序描述逻辑TL-SI，将时序网络间的蕴含算法、时序概念间的蕴含算法以及非时序概念的Tableau算法有机结合起来，并证明了三种算法的可靠性和完备性。rn 该逻辑可以有效表示动作行为，实现了可判定的逻辑推理，为语义Web服务的行为描述提供了有力支持。

摘要： 时序描述逻辑能够通过概念(或个体)问的时序关系描述动态领域的时序行为。时序概念的表现形式具有多样性，而其推理算法却常常是不可判定的。本文提出时序描述逻辑TL-SI，将时序网络间的蕴含算法、时序概念间的蕴含算法以及非时序概念的Tableau算法有机结合起来，并证明了三种算法的可靠性和完备性。rn 该逻辑可以有效表示动作行为，实现了可判定的逻辑推理，为语义Web服务的行为描述提供了有力支持。

摘要： 时序描述逻辑能够通过概念(或个体)问的时序关系描述动态领域的时序行为。时序概念的表现形式具有多样性，而其推理算法却常常是不可判定的。本文提出时序描述逻辑TL-SI，将时序网络间的蕴含算法、时序概念间的蕴含算法以及非时序概念的Tableau算法有机结合起来，并证明了三种算法的可靠性和完备性。rn 该逻辑可以有效表示动作行为，实现了可判定的逻辑推理，为语义Web服务的行为描述提供了有力支持。

摘要： 时序描述逻辑能够通过概念(或个体)问的时序关系描述动态领域的时序行为。时序概念的表现形式具有多样性，而其推理算法却常常是不可判定的。本文提出时序描述逻辑TL-SI，将时序网络间的蕴含算法、时序概念间的蕴含算法以及非时序概念的Tableau算法有机结合起来，并证明了三种算法的可靠性和完备性。rn 该逻辑可以有效表示动作行为，实现了可判定的逻辑推理，为语义Web服务的行为描述提供了有力支持。

摘要： 本发明涉及一种十分安全，同时非常容易使用的认证密码的生成方法。在一个基于本发明的技术方案而开发的密码管理软件中，设置一些被称为代换字符串的中间变量，把通过键盘输入的被称作表观密码的一串字符，转换成输出到外部实施身份认证的真实密码。由于表观密码并不参与实际的身份认证，因此可以从简设置。而存储在本软件中的代换字符串并无任何实际意义，只有当输出认证密码时，才将它们按照预设的混插方式立刻组合起来、生成真实密码、再一键输出到外部的密码认证表单中，执行实际的身份认证。

摘要： 同时满足跟踪性和鲁棒性的燃气锅炉最优分数阶PID控制方法，利用PSO算法能通过迭代寻找最优解以及PSO算法收敛速度快的特性。对H∞稳定域范围内的分数阶PID控制器参数进行迭代寻优。首先初始化PSO算法中的粒子，其位置坐标随机分布在稳定域内。然后对粒子进行适应度计算，并设置其初始速度，使得粒子能够朝适应度更好的方向移动。最后不断进行迭代，直至两次迭代差值小于设定误差，得出最优解，即在稳定域范围内的分数阶PID控制器参数最优解。本发明采用的PSO算法，能够更快更精确的同时整定多个分数阶PID控制器参数。

摘要： 可以利用安全策略来同意或拒绝与计算资源的访问相关的许可。可以对两个或更多个安全策略进行比较，以确定所述策略是否为等效的，一个安全是否比另一个更宽松，等等。在一些情况下，可能可以识别是否存在足以确定两个安全策略缺乏等效性的安全许可。命题逻辑可以用于评估安全策略。

摘要： 公开了一种能够同时满足优异性能和高耐久性两个要求的膜电极组件以及包括该膜电极组件的燃料电池。本发明的膜电极组件包括：第一电极；第二电极；以及设置在第一电极和第二电极之间的电解质膜，其中第一电极包括具有第一耐久性的第一部分和具有与第一耐久性不同的第二耐久性的第二部分。

摘要： 本发明涉及超大规模集成电路设计验证技术领域，特别是组合电路的形式验证方法——等价性检验方法。该方法是以可满足性算法为引擎，增量地验证整个电路设计，所述方法具有两个阶段，第一阶段是确定两个电路内部的候选等价信号，并通过电路结构分析，对候选等价信号作静态筛选，第二阶段是通过子句分组实现增量可满足性方法，并验证每对候选信号的等价性。其主要特点在于：1)通过电路结构分析对电路内部的候选等价信号进行筛选，在验证过程中则动态地选择分割集中的等价信号，保证分割集中信号是相互独立的。2)通过对子句进行分组，来实现增量的可满足性算法，节省计算资源，提高算法性能和处理能力。

摘要： 本发明公开了一种布尔可满足性求解器中学习子句的删除方法及布尔可满足性求解器，所述方法包括：在求解的过程中生成多个学习子句，并对每个学习子句的使用次数及LBD值进行记录；当触发学习子句删除条件时，根据学习子句的使用次数和LBD值对学习子句进行删减。采用本发明的技术方案，可提高学习子句的质量，提升求解器的运行效率。

摘要： 本发明涉及超大规模集成电路设计验证技术领域，特别是组合电路的形式验证方法——等价性检验方法。该方法是以可满足性算法为引擎，增量地验证整个电路设计，所述方法具有两个阶段，第一阶段是确定两个电路内部的候选等价信号，并通过电路结构分析，对候选等价信号作静态筛选，第二阶段是通过子句分组实现增量可满足性方法，并验证每对候选信号的等价性。其主要特点在于：1)通过电路结构分析对电路内部的候选等价信号进行筛选，在验证过程中则动态地选择分割集中的等价信号，保证分割集中信号是相互独立的。2)通过对子句进行分组，来实现增量的可满足性算法，节省计算资源，提高算法性能和处理能力。

摘要： 本发明为基于线性规划的布尔可满足性判定方法，属于逻辑电路领域，包括如下步骤：S1提取布尔命题逻辑公式；S2：转换为等可满足的CNF布尔逻辑公式；S3：转化为CNF形式的3‑SAT问题；S4：转化为1‑in‑3‑SAT问题；S5：等效转化为一个线性规划的最优值大小问题；S6：对线性规划的最优值求解问题进行求解精度设定；S7：求解线性规划问题的最优值，并根据最优值大小来判定布尔命题逻辑公式的可满足性；S8：对于可满足的布尔命题逻辑公式，递归地对线性规划问题添加约束并进行求解，得到可满足问题的一个解答。本发明实现了在多项式时间复杂度下的快速判定，能够判定的提高效率，节约能源。

摘要： 本发明提供了一种布尔可满足性验证方法、系统、验证过程中的CNF生成方法及存储装置，所述布尔可满足性验证中的CNF生成方法包括：在将miter电路的每个节点转换为CNF的过程中，释放后续节点无需调用的CNF的占用内存。采用本发明的技术方案，可降低布尔可满足性验证中的内存占用。

摘要： 本发明涉及一种服装定制需求可满足性验证的建模方法，包括以下步骤；步骤一，将用户个性化需求进行形式化建模；对用户个性化定制服装的要求进行分类描述；根据服装加工制造流程的先后次序，将需求划分为若干个层次：步骤二，将生产制造能力进行形式化建模；生产制造能力包括生产产品所需的原料、人员和设备的一种或多种中的若干个生产要素；步骤三，将服装定制需求形式化为一阶逻辑公式，通过可满足性理论方法判断问题是否可解。本发明提供了一种服装定制需求可满足性验证的建模方法，能建立一个满足性验证模型，对服装定制需求进行满足性的验证。