共查询到19条相似文献,搜索用时 171 毫秒
1.
命题逻辑可满足性问题的算法分析 总被引:7,自引:0,他引:7
1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。 相似文献
2.
求解难可满足性问题的混合算法 总被引:1,自引:0,他引:1
张德富 《小型微型计算机系统》2003,24(8):1528-1531
提出了一个求解难可满足性问题的简单混合算法.拟人和禁忌表两个策略被给出.数值实验表明,对于一类公认比较难的可满足性问题,该算法胜过目前据认为是最好方法之一的NOVELTY算法. 相似文献
3.
对SAT问题及其各种约束子问题进行分类并给出具体定义,着重介绍常规SAT问题、最大可满足性问题(MAX—SAT)和参数化SAT问题的相关算法,并对参数算法中运用的技术进行分析和比较,提出一些SAT问题研究中值得关注的几个方面。 相似文献
4.
该文为可满足性问题的高效近似求解提出了改进的模拟退火算法。数值实验表明,对于该文随机产生的测试问题例,改进的模拟退火算法完全胜过局部搜索算法、模拟退火算法以及目前国际上流行的WSAT算法。 相似文献
5.
本文对布尔表达式的可满足性问题作了进一步的研究,证明了该问题的充要条件,本文把布尔表达式可满足性的“判定的问题”与它的“求解问题”区别开来。 相似文献
6.
CP-nets是一种简单而又直观的图形化偏好表示工具,成为近几年人工智能的一个研究热点,然而对于CP-nets的可满足性和一致性等相关性质的研究还很欠缺.既没有给出严格的定义,也没有探讨不同性质之间的联系,没有一个求可满足性序列的通用算法.从研究CP-nets的可满足性和一致性的关系着手,得出了任意结构二值CP-nets的可满足性判定算法及可满足性序列生成算法.首先通过构造CP-nets导出图及其性质的研究,得出CP-nets的可满足性及一致性的相关定理.再把不同性质结合起来分析,给出CP-nets可满足性等价于一致性的结论,从而利用拓扑排序的思想实现了任意结构二值CP-nets的可满足性序列的生成.强化和扩充了Boutilier所提出的一些概念,深化了CP-nets的基础理论研究. 相似文献
7.
RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展. 相似文献
8.
9.
10.
可满足性问题的一种DNA表面计算模型是一种特殊的DNA计算方法,该模型是采用荧光标记的策略和荧光猝灭技术,通过观察荧光灭光情况排除非解,从而有效的解决可满足性问题(SAT).该模型方法具有错误率低、编码简单、读取方便等很好的性能,能够大大减少实验过程中的错差. 相似文献
11.
12.
Artifact行为的一致性检测,是在流程建模、运行之后亟待解决的关键问题之一.针对现有一致性检测技术忽略数据操作方面检测的问题,提出了一种基于Artifact快照序列的行为一致性检测方法.首先,利用全序Artifact快照序列定义了Artifact的行为模式,该行为模式不仅体现了服务的运行轨迹,也描述出了Artifact数据属性赋值的状态变化;然后,将Artifact行为一致性检测问题转换为语言可判定问题,证明了该问题是一个可判定问题,该过程中,设计一台判定该语言的图灵机作为一致性验证模型,该模型不仅检测了Artifact生命周期中服务路径的一致性,同时也检测了生命周期中Artifact属性赋值的正确性;进一步地,利用服务-快照关联矩阵的等价转换,给出了行为一致性量化指标中确切度的精确计算方法;最后,通过实例分析及实验对所提出的方法进行了验证. 相似文献
13.
求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。 相似文献
14.
15.
Symbolic Techniques in Satisfiability Solving 总被引:1,自引:0,他引:1
Recent work has shown how to use binary decision diagrams for satisfiability solving. The idea of this approach, which we
call symbolic quantifier elimination, is to view an instance of propositional satisfiability as an existentially quantified proposition formula. Satisfiability
solving then amounts to quantifier elimination; once all quantifiers have been eliminated, we are left with either 1 or 0. Our goal in this work is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability
solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization
techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety
of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of
formulas, the symbolic approach is superior for other classes of formulas. Once we have demonstrated the viability of the
symbolic approach, we focus on optimization techniques for this approach. We study techniques from constraint satisfaction
for finding a good plan for performing the symbolic operations of conjunction and of existential quantification. We also study
various variable-ordering heuristics, finding that while no heuristic seems to dominate across all classes of formulas, the
maximum-cardinality search heuristic seems to offer the best overall performance.
★A preliminary version of the paper was presented in SAT'04. Supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326,
IIS-9908435, IIS-9978135, EIA-0086264, ANI-0216467, and by BSF grant 9800096. 相似文献
16.
服务组合一般是根据用户需求来查找匹配的服务并对其进行组合,但用户需求往往是基于自然语.言的,很难用于服务的自动组合.提出了一种基于环境本体的组合服务需求模型,该模型以环境实体上的意图为基础,将关联意图集定义为任务.引入Petri网作为任务间的控制逻辑关系,并给出了一种判定需求可满足性的方法.最后选择旅行安排作为具体案例... 相似文献
17.
Inês Lynce João P. Marques-Silva 《Annals of Mathematics and Artificial Intelligence》2003,37(3):307-326
Propositional Satisfiability (SAT) is often used as the underlying model for a significant number of applications in Artificial Intelligence as well as in other fields of Computer Science and Engineering. Algorithmic solutions for SAT include, among others, local search, backtrack search and algebraic manipulation. In recent years, several different organizations of local search and backtrack search algorithms for SAT have been proposed, in many cases allowing larger problem instances to be solved in different application domains. While local search algorithms have been shown to be particularly useful for random instances of SAT, recent backtrack search algorithms have been used for solving large instances of SAT from real-world applications. In this paper we provide an overview of backtrack search SAT algorithms. We describe and illustrate a number of techniques that have been empirically shown to be highly effective in pruning the amount of search on significant and representative classes of problem instances. In particular, we review strategies for non-chronological backtracking, procedures for clause recording and for the identification of necessary variable assignments, and mechanisms for the structural simplification of instances of SAT. 相似文献
18.
L. Trevisan 《Algorithmica》2000,28(1):145-172
We study the approximability of the Maximum Satisfiability Problem (MAX SAT) and of the boolean k -ary Constraint Satisfaction Problem (MAX k CSP) restricted to satisfiable instances. For both problems we improve on the performance ratios of known algorithms for
the unrestricted case.
Our approximation for satisfiable MAX 3CSP instances is better than any possible approximation for the unrestricted version
of the problem (unless P=NP). This result implies that the requirement of perfect completeness weakens the acceptance power
of non-adaptive PCP verifiers that read 3 bits.
We also present the first non-trivial results about PCP classes defined in terms of free bits that collapse to P.
Received August 1997; revised February 1999. 相似文献
19.
Ştefan Andrei 《Artificial Intelligence Review》2004,22(4):339-366
We present a new algorithm for counting truth assignments of a clausal formula using inverse propositional resolution and its associated normalization rules. The idea is opposite of the classical resolution, and is achieved by constructing in a bottom-up manner a computation graph. This means that we successively add complementary literals to generate new bigger clauses instead of solving them. Next, we make a comparison between the classical and inverse resolution, followed by a new algorithm which combines these two techniques for solving the SAT problem. 相似文献