1.Pure logical reasoning

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)題的求解炒俱,

  1. Truth table assisgnment grows exponentially。
  2. 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}
 
最后編輯于
?著作權(quán)歸作者所有,轉(zhuǎn)載或內(nèi)容合作請(qǐng)聯(lián)系作者
  • 序言:七十年代末怔檩,一起剝皮案震驚了整個(gè)濱河市,隨后出現(xiàn)的幾起案子蓄诽,更是在濱河造成了極大的恐慌薛训,老刑警劉巖,帶你破解...
    沈念sama閱讀 222,729評(píng)論 6 517
  • 序言:濱河連續(xù)發(fā)生了三起死亡事件仑氛,死亡現(xiàn)場(chǎng)離奇詭異许蓖,居然都是意外死亡,警方通過(guò)查閱死者的電腦和手機(jī)调衰,發(fā)現(xiàn)死者居然都...
    沈念sama閱讀 95,226評(píng)論 3 399
  • 文/潘曉璐 我一進(jìn)店門,熙熙樓的掌柜王于貴愁眉苦臉地迎上來(lái)自阱,“玉大人嚎莉,你說(shuō)我怎么就攤上這事∨嫱悖” “怎么了趋箩?”我有些...
    開(kāi)封第一講書人閱讀 169,461評(píng)論 0 362
  • 文/不壞的土叔 我叫張陵赃额,是天一觀的道長(zhǎng)。 經(jīng)常有香客問(wèn)我叫确,道長(zhǎng)跳芳,這世上最難降的妖魔是什么? 我笑而不...
    開(kāi)封第一講書人閱讀 60,135評(píng)論 1 300
  • 正文 為了忘掉前任竹勉,我火速辦了婚禮飞盆,結(jié)果婚禮上,老公的妹妹穿的比我還像新娘次乓。我一直安慰自己吓歇,他們只是感情好,可當(dāng)我...
    茶點(diǎn)故事閱讀 69,130評(píng)論 6 398
  • 文/花漫 我一把揭開(kāi)白布票腰。 她就那樣靜靜地躺著城看,像睡著了一般。 火紅的嫁衣襯著肌膚如雪杏慰。 梳的紋絲不亂的頭發(fā)上测柠,一...
    開(kāi)封第一講書人閱讀 52,736評(píng)論 1 312
  • 那天,我揣著相機(jī)與錄音缘滥,去河邊找鬼轰胁。 笑死,一個(gè)胖子當(dāng)著我的面吹牛完域,可吹牛的內(nèi)容都是我干的软吐。 我是一名探鬼主播,決...
    沈念sama閱讀 41,179評(píng)論 3 422
  • 文/蒼蘭香墨 我猛地睜開(kāi)眼吟税,長(zhǎng)吁一口氣:“原來(lái)是場(chǎng)噩夢(mèng)啊……” “哼凹耙!你這毒婦竟也來(lái)了?” 一聲冷哼從身側(cè)響起肠仪,我...
    開(kāi)封第一講書人閱讀 40,124評(píng)論 0 277
  • 序言:老撾萬(wàn)榮一對(duì)情侶失蹤肖抱,失蹤者是張志新(化名)和其女友劉穎,沒(méi)想到半個(gè)月后异旧,有當(dāng)?shù)厝嗽跇?shù)林里發(fā)現(xiàn)了一具尸體意述,經(jīng)...
    沈念sama閱讀 46,657評(píng)論 1 320
  • 正文 獨(dú)居荒郊野嶺守林人離奇死亡,尸身上長(zhǎng)有42處帶血的膿包…… 初始之章·張勛 以下內(nèi)容為張勛視角 年9月15日...
    茶點(diǎn)故事閱讀 38,723評(píng)論 3 342
  • 正文 我和宋清朗相戀三年吮蛹,在試婚紗的時(shí)候發(fā)現(xiàn)自己被綠了荤崇。 大學(xué)時(shí)的朋友給我發(fā)了我未婚夫和他白月光在一起吃飯的照片。...
    茶點(diǎn)故事閱讀 40,872評(píng)論 1 353
  • 序言:一個(gè)原本活蹦亂跳的男人離奇死亡潮针,死狀恐怖术荤,靈堂內(nèi)的尸體忽然破棺而出,到底是詐尸還是另有隱情每篷,我是刑警寧澤瓣戚,帶...
    沈念sama閱讀 36,533評(píng)論 5 351
  • 正文 年R本政府宣布端圈,位于F島的核電站,受9級(jí)特大地震影響子库,放射性物質(zhì)發(fā)生泄漏舱权。R本人自食惡果不足惜,卻給世界環(huán)境...
    茶點(diǎn)故事閱讀 42,213評(píng)論 3 336
  • 文/蒙蒙 一仑嗅、第九天 我趴在偏房一處隱蔽的房頂上張望宴倍。 院中可真熱鬧,春花似錦无畔、人聲如沸啊楚。這莊子的主人今日做“春日...
    開(kāi)封第一講書人閱讀 32,700評(píng)論 0 25
  • 文/蒼蘭香墨 我抬頭看了看天上的太陽(yáng)恭理。三九已至,卻和暖如春郭变,著一層夾襖步出監(jiān)牢的瞬間颜价,已是汗流浹背。 一陣腳步聲響...
    開(kāi)封第一講書人閱讀 33,819評(píng)論 1 274
  • 我被黑心中介騙來(lái)泰國(guó)打工诉濒, 沒(méi)想到剛下飛機(jī)就差點(diǎn)兒被人妖公主榨干…… 1. 我叫王不留周伦,地道東北人。 一個(gè)月前我還...
    沈念sama閱讀 49,304評(píng)論 3 379
  • 正文 我出身青樓未荒,卻偏偏與公主長(zhǎng)得像专挪,于是被迫代替她去往敵國(guó)和親。 傳聞我的和親對(duì)象是個(gè)殘疾皇子片排,可洞房花燭夜當(dāng)晚...
    茶點(diǎn)故事閱讀 45,876評(píng)論 2 361

推薦閱讀更多精彩內(nèi)容