查缺補漏:集和與非平凡屬性

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

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

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

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

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

支配集
支配集≈ 一組頂點，使得圖要么在支配集中，要么是圖中某個頂點的鄰域
占主導(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ī)語言。
賴斯定理說，判斷一個特定TM識別的語言滿足一個非平凡的條件通過在字符串w上運行TM M，然后為這些性質(zhì)運行TM

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

總結(jié)

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

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