作为本系列的最后一篇文章,我们来看被广为研究的SAT问题。
SAT问题是第一个被证明为NP问题的判定问题。更多信息可以去百度或者维基一下。
前面我们看到了Horn公式可满足性的判定算法,现在把它推广到任意公式Φ。首先将公式变换成具有下面语法的等值公式:φ ::= p | (¬φ) | (φ ∧ φ)。变换方法如下(已被证明变换后是等价的):
在结果T(φ)的语法树中要公共子公式共享,这样将语法树变成一个有向无回路(环)图(DAG)。
例如,φ = p∧ ¬(q ∨¬p),变换后T(φ)=p ∧¬¬(¬q ∧¬¬p)。它们语法树分别是:
看明白怎么就是“分享子公式”了吧。
对于变换后的语法树进行从上到下的标记,根部标记T,如果没有冲突标记的结果就是一次合格的赋值。标记中需要用到的逼迫规则有下:
那么这个算法能判断所有的公式吗?答案是否定的!对于形如¬(φ1 ∧ φ2)这样的公式无法判断(自己试一下)。
上述算法是一个线性时间算法。我们还有一个三次多项式时间算法。算法的主要思想:
1.任选一个未标记结点试探标记T,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告失败或报告不可满足(矛盾),而不再有待试探的结点,算法报告”标记失败”并停机;否则转2.
2.对该结点标记F,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告不可满足且在前面标记该结点时也报告不可满足,则报告不可满足并停机;否则将两次试探标记都相同的结点标记作为永久标记.转1.
这个算法也不是万能的,比如它对于下图语法树对应的CNF不能判定:
SAT问题目前依然是逻辑界和计算理论界的研究热点。有兴趣的可以关注一下。
命题逻辑公式是否定理最起码可以通过真值表查看是否可满足,那么对于谓词逻辑公式呢?我们是不是有其他什么方法可以判断谓词逻辑公司是否有效呢?
答案是否定的:给定一个谓词逻辑公式φ,|=φ是否有效是不可判定的。这有点震惊了,到底是啥意思呢?
我们采用问题归约技术:将一个已知不可判定问题归约到所考虑的判定问题,使得要考虑的判定问题可判定必导致已知的不可判定问题成为可判定问题,这就导致了矛盾。这证明我们要考虑的判定问题是不可判定的。(如果没有学过算法的,可以先花点时间了解下什么是规约)
那么哪个判定问题是不可判定问题呢?我们选择著名的波斯特对应问题(Post Correspondence Problem, PCP,你可以先百度一下):PCP的一个问题实例由某个字母表Σ上串的两个表组成,这两个表的长度相等,一般称为A表和B表。对于某个正整数k,A=(s1,s2,...,sk),B=(t1,t2,...,tk)。(si, ti)表示一个对应对。如果存在整数序列i1,i2,...,in,当把这个序列解释成A表和B表中串的下标时,能够产生相同的串,则说这个PCP问题实例有解。i1,i2,...,in称为这个问题的一个解。PCP问题就是对于一个PCP实例,它是否有解。
波斯特对应问题是不可判定的。可以参考《自动机理论、语言和计算导论》John E. Hopcroft Rejeev Motwani Jeffrey D.Ullman著, 刘田、姜晖、王捍贫译,机械工业出版社,2004年6月第1版。
看一个波斯特对应问题实例:字母表Σ={0,1}。
例1. A={1,10,011}, B={101,00,11},其解为:(1,3,2,3),串是1011 10 011。
例2. A={1,10111,10},B={111,10,0},其解为(2,1,1,3)或(2,1,1,3,2,1,1,3)
例3. A={10,011,101},B={101,11,011} 这个PCP问题实例无解。
(你说什么?你感觉这个问题很简单,能够设计出算法?那你可以试试。)
定理 谓词逻辑公式的有效性判定问题是不可判定的:不存在判定算法,使得对于任给谓词逻辑公式Ф,判定是否|=Ф是有效的。
证明: 采用归约技术。对于给定的波斯特对应问题实例C,构造一个谓词逻辑公式Ф,且构造在有限的空间和时间内完成,使得|=Ф有效当且仅当波斯特对应问题实例C有解。
设波斯特对应问题实例C:
构造公式Ф:函数符号F={e,f0 ,f1},e是常量,e,f0 ,f1是一元函数。谓词符号P。
相关推荐
对命题逻辑和谓词逻辑的核心归纳可以做到一目了然
加深对归结原理进行定理证明过程的理解,掌握基于谓词逻辑的归结过程中子句变换过程、替换与合一算法即归结策略等重要环节,进一步了解实 现机器自动定理证明的步骤。 采用C++
人工智能课件,关于谓词逻辑与归结原理,在学习了离散数学的基础上,进一步深入的学习谓词逻辑,掌握人工智能的初步知识
人工智能谓词逻辑归结问题的推理系统是很好的学习资料 ,可以帮助广大学子进一步学习人工智能的相关知识。
谓词逻辑离散数学
命题逻辑与谓词逻辑PPT课件.pptx
为消除不透明谓词对程序恶意性判定的影响,以广义不透明谓词后趋依赖的属性为依据,结合逻辑恒定判定,提出了基于逻辑一致性的广义不透明谓词检测方法。通过静态分析提取谓词前置条件约束、后趋逻辑约束和谓词判定...
谓词逻辑推理,人工智能的基本理论,为人工智能系统的开发奠定了一定的理论基础
用于人工智能的学习,内容全面,人工智能 谓词逻辑
假设:所有不贫穷且聪明的人都快乐。那些看书的人都是聪明的。李明能看书且不贫穷。快乐的人过着激动人心的生活。 ;求证:李明过着激动人心的生活。 (\x)(~Poor(x)∧Smart(x)→happy(x)) (\x)(Read(x)→Smart(x)) ...
离散数学 谓词逻辑 PPT 基础 有用 好好学习
东北大学 离散数学课件 谓词逻辑 保证很详细哦
第2章(知识表示方法3-谓词逻辑)
第 2 章谓词逻辑命题逻辑对于反映在自然语言中的逻辑思维进行了精确的形式化描述,能够对一些比较复杂的逻辑推理,用形式化方法进行分析。在命题逻辑中,把命题分解到原
离散数学 谓词逻辑 习题课PPT课件.pptx
课件主要简介离散数学的谓词逻辑,帮助我们更好理解这章内容,除此之外,也使学生从逻辑的角度了解数学
一阶谓词逻辑下的Horn 逻辑是人工智能程序语言Prolog 的理论基础,利用Prolog 在计算机 上可实现机械化,从而使自动化求解问题和定理证明具备可行性。
人工智能课件:第三章 谓词逻辑与搜索原理.pdf
人工智能导论课件:第四章 谓词逻辑与归结原理.ppt
这是我的文章的第三章的第二节,因为有公式没法发,直接放这里了。