查缺補(bǔ)漏:集和與非平凡屬性

前面的習(xí)題和知識點(diǎn)補(bǔ)充
Conjunctive normal form（CNF）是布爾邏輯的一種方法，它將公式表示為帶有AND或or的子句的連詞。由連詞or AND連接的每個(gè)子句必須是文字或包含析取or運(yùn)算符

子集和求和。
給定自然數(shù)s1，sn和一個(gè)整數(shù)W、 有一個(gè)子集加起來正好是W嗎？
例如{1,4,16,64,256,1040,1041,1093,1284,1344}，W=3754。
答案:對1 + 16 + 64 + 256 + 1040 + 1093 + 1284 = 3754.
評論對于算術(shù)問題，輸入整數(shù)被編碼為二進(jìn)制的多項(xiàng)式歸約必須是二進(jìn)制多項(xiàng)式編碼。

證明思路:給出3-SAT的一個(gè)實(shí)例Φ，我們構(gòu)造了有解 iff Φ的子集和是可滿足的。

建設(shè)給定3-SAT實(shí)例Φ，包含n個(gè)變量和m子句，形式為2n+2m十進(jìn)制整數(shù)，每n+m位，如下所示：
用一個(gè)表格1,0表示T/F, X,Y,Z,以及C1,C2,C3(C1,C2,C3 都是用XYZ組成的)
宣稱Φ是可滿足的，當(dāng)存在一個(gè)子集和W之和時(shí)。

Sat4j是一個(gè)功能齊全的布爾推理庫，旨在將最先進(jìn)的SAT技術(shù)引入Java虛擬機(jī)。
Sat4j是一個(gè)用于解決布爾滿足和優(yōu)化問題的java庫。它可以解決SAT、MAXSAT、偽布爾、最小不可滿足子集（MUS）問題。在Java中，我們的承諾不是以最快的速度解決這些問題（Java中的SAT解算器比C++中的SAT解算器慢約3.25倍），而是功能齊全、健壯、用戶友好，并遵循Java設(shè)計(jì)準(zhǔn)則和代碼約定（使用源代碼的靜態(tài)分析進(jìn)行檢查）。通過大量使用decorator和strategy設(shè)計(jì)模式，該庫的設(shè)計(jì)具有靈活性。此外，Sat4j是開源的，擁有雙業(yè)務(wù)友好的Eclipse公共許可證和學(xué)術(shù)友好的GNU LGPL許可證。
為了了解使用Sat4j可以做些什么，您可能想看看Sat4j案例研究（草稿）。
多年來，Sat4j已被許多研究小組使用，尤其是在軟件工程領(lǐng)域，并已被納入許多約束編程、人工智能或軟件驗(yàn)證課程。

支配集
支配集≈ 一組頂點(diǎn)，使得圖要么在支配集中，要么是圖中某個(gè)頂點(diǎn)的鄰域
占主導(dǎo)地位的場景。
證明：“測試S是否為支配集”
boolean C(G, S)
foreach v ∈ (V (G) \ S)
dom ← false
foreach s ∈ S
if v and s are adjacent
dom← true
if dom is false
return NO
return YES

非平凡屬性
非平凡屬性意味著某些語言滿足它，而另一些語言滿足它不與給定語言相等就是這樣一種屬性或者成為一種常規(guī)語言。
賴斯定理說，判斷一個(gè)特定TM識別的語言滿足一個(gè)非平凡的條件通過在字符串w上運(yùn)行TM M，然后為這些性質(zhì)運(yùn)行TM

問題:“M正好有5個(gè)狀態(tài)”是可識別的非平凡性質(zhì)語言嗎？
解決方案：“M正好有5個(gè)狀態(tài)”是一個(gè)語法屬性，而引號里面內(nèi)容是語義。因此，這個(gè)問題毫無意義。
問題: 如果“被一臺只有5個(gè)字符的機(jī)器識別”呢?
解決方案：非平凡(non-trivial)，因?yàn)?#xff1a;有一些語言可以被TMs識別，精確到5
狀態(tài)，例如空語言;此外，還必須有無法識別的語言由一個(gè)只有5個(gè)狀態(tài)的TM生成，因?yàn)?#xff1a;對于任何固定的字母表（例如，∑={a，b}），有無限多個(gè)字母
語言超過∑，但是5個(gè)狀態(tài)且使用∑的TMs的數(shù)量是有限的（因此，這些TMs只能接受有限的多種語言）

總結(jié)

以上是生活随笔為你收集整理的查缺补漏:集和与非平凡属性的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。