SAT 問(wèn)題(布林可滿足性問(wèn)題)
定義:SAT問(wèn)題是判定一個(gè)命題公式是否可滿足的問(wèn)題档桃,通常這個(gè)命題公式是CNF公式夭禽。(the Boolean Satisfiability Problem)
CNF公式:C1 ∧… ∧ Cm為CNF公式珠移,其中∧是邏輯上的合取連接詞嗤锉,Ci是子句沐飘; CNF公式也常被表示為子句的集合匿乃。
子句:l1∨… ∨ lk形式的式子稱為子句,其中∨是邏輯上的析取連接詞初橘, li是文字验游;子句也常被表示為文字的集合充岛。
文字:布爾變量x和布爾變量的非﹁x稱為文字。
那么批狱,SAT問(wèn)題可以簡(jiǎn)化為:給定一個(gè)CNF公式F裸准,判定它是否存在一個(gè)賦值t,使得t(F)=1赔硫。
SAT 問(wèn)題通常被視為NPC問(wèn)題(NPC(Nondeterministic Polynomial Complete)問(wèn)題:只有把解域里面的所有可能都窮舉了之后才能得出答案)
缺點(diǎn):這類問(wèn)題的求解炒俱,
- Truth table assisgnment grows exponentially。
- Important SAT problems have thousands of variables
Solution:對(duì)于 (p→q)→(r ∧ ?(p ∨ ?s))爪膊,先轉(zhuǎn)化為Negation Normal Form权悟,得到
(p ∧ ?q) ∨ (r ∧ (?p ∨ s))。再轉(zhuǎn)化成Conjunctive Normal Form推盛,得到(p ∨ r) ∧ (p ∨ ?p ∨ s) ∧ (?q ∨ r) ∧ (?q ∨ ?p ∨ s)峦阁。
常用:A?B equivalent to (A∧B)∨(?A∧?B),A→B equivalent to ?A∨B
最后耘成,通過(guò)方法{(p1 ∨ ... ∨ pn ∨ q)∨(?q ∨ r1 ∨ ... ∨ rm) 等于 p1 ∨ ... ∨ pn ∨ r1 ∨ ... ∨ rm } deduce the unsatisfiable/satisfiable
Unit propagation
Definition: a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.
Iterating these inference moves is unit propagation
DPLL: a better way to solve the SAT Problem
它是一個(gè)回溯搜索算法
基本思想: 每次選中一個(gè)未被賦值的變量進(jìn)行賦值榔昔,然后判斷該賦值是否滿足整個(gè)公式:
滿足:結(jié)束搜索;
導(dǎo)致沖突(某個(gè)子句為0):回溯瘪菌;
否則:對(duì)下一個(gè)變量進(jìn)行賦值
improve the DPLL:
1.Clause learning
2.Choosing good atoms for branching
3.Intelligent backtracking
4.Restarts
存在quantifiers(existential撒会,universal)的logic formula
先將其化為 Prenex normal form(quantifiers are outside),再Removing the quantifiers(Variable replaced by a new name or function师妙,delete existential and universal)最后調(diào)整為clause form诵肛,通過(guò)substituting terms for variables in order to make literals match,就可以正常推理了默穴。
Example:
Γ = { ?x(?Q(x) → P(x)), ??y P (y), Q(a) → ?x(R(x) ∧ ?Q(x)) }
1.Use normal-forming moves to transform Γ into a set ? of first order clauses such that ? is satisfiable if and only if Γ is satisfiable.
First get the quantifiers to the front (prenex normal form):
?x(?Q(x) → P(x)),
?y ?P (y),
?x(Q(a) → (R(x) ∧ ?Q(x)))
Next remove the existential quantifier and use a name (skolem constant) instead:
?x(?Q(x) → P(x)),
?y ?P (y),
Q(a) → (R(b) ∧ ?Q(b))
Delete the universal quantifiers, and put the propositional parts into clause form:
? = { Q(x)∨P(x), ?P (y), ?Q(a) ∨ R(b), ?Q(a) ∨ ?Q(b) }
2.Write out a resolution proof by which the empty clause is derived from ?. For each resolution inference in the proof, make a note of any unifier that is involved.
1. Q(x) ∨ P (x) given
2. ?P(y) given
3. Q(x) from 1, 2 unifier {y ← x}
4. ?Q(a) ∨ ?Q(b) given
5. ?Q(b) from 3, 4 {x ← a}
6. ⊥ from 3, 5 {x ← b}