gophersat下載 - gophersat原始碼下載

gophersat

Ai源碼

1.0.0

下載

Gophersat，用 Go 寫的 SAT 和偽布林解算器

這是 Gophersat，一個純粹用 Go 寫的 SAT 和偽布爾求解器。 Gophersat 由阿圖瓦大學 CRIL（Centre de Recherche en Informatique de Lens）和 CNRS 開發。它是在 MIT 許可下發布的。 Gophersat 相當高效，即在典型的 SAT 基準測試中，它的運行速度比它受到強烈啟發的頂級求解器（即葡萄糖或 minisat）慢約 2 到 5 倍。它還可以解決 MAXSAT 問題以及偽布林決策和最佳化問題。

版本 1.4：切割平面

Gophersat 的最後一個穩定版本是 1.4 版。它包括可選的切割平面求解策略。

有些問題，例如著名的鴿巢問題，需要很長時間才能使用純邏輯推理來解決。

鴿籠問題可以這樣表達：是否可以將n只鴿子放入m個鴿子中，其中m = n-1，而不將幾隻鴿子放入同一個洞中並將所有鴿子放入一個洞中？答案很明顯：如果你有 4 隻鴿子在 3 個洞裡，你不能把它們全部放在不同的洞裡。但你要如何證明這一點呢？ SAT 或 PB 求解器將透過嘗試所有可能的組合來證明這一點，並且可能的組合的數量呈指數級增長。因此，嘗試解決 n=20 的問題在實踐中是不可行的，儘管該問題有明顯的答案。

一些 PB 求解器實作另一種策略：割平面策略。本文不會詳細描述，但這種策略在某些問題上可以非常有效，例如無法透過純邏輯推理有效解決的鴿巢問題，但在大多數問題上會比較慢。

現在可以將切割平面與 Gophersat 一起使用。只需使用-cp命令列選項即可。因此，不要調用：

 gophersat problem.opb

只需致電：

 gophersat -cp problem.opb

1.3版

Gophersat 的最後一個穩定版本是 1.3 版。這是一個小更新，增加了在處理 MAXSAT 問題時存取底層求解器的能力。

版本 1.2：可解釋的 AI：UNSAT 認證、MUS 提取

Gophersat 1.2 版包含一種理解 UNSAT 實例的方法，既可以在問題為 UNSAT 時提供 RUP 證書，也可以提供提取公式中不可滿足的子集的能力。也修正了一些錯誤，並改進了對增量 SAT 求解的支援。

要了解有關這些功能的更多信息，您可以查看有關 UNSAT 證書和 MUS 的教程。

要使用 gophersat 可執行檔產生證書，只需呼叫：

 gophersat -certified problem.cnf

然後，憑證將使用 RUP 符號列印在標準輸出上。憑證是動態產生的，因此請注意，即使問題實際上可以解決，也會產生部分無用的憑證。這是社群中的常見做法，雖然產生的子句是無用的噪音，但實際上這不是問題。

要從 UNSAT 實例中提取 MUS，只需呼叫：

 gophersat -mus problem.cnf

MUS 將列印在標準輸出上。如果問題不是 UNSAT，則會顯示錯誤訊息。

目前，這些工具僅適用於純 SAT 問題（即不是偽布爾問題）。

1.1版

自 1.1 版本以來，Gophersat 包含一個新的、更有效率的純 SAT 問題核心求解器和一個處理 MAXSAT 問題的套件。它還包括一個用於最佳化和模型計數的新 API，一旦發現新模型，就會將其寫入通道。

關於 Gophersat 中的版本號

自 1.0 版本以來，Gophersat 的 API 被認為是穩定的，這意味著該 API 保證保持向後相容，直到發生主要版本轉換。換句話說，如果您的程式適用於 1.0 版本的 gophersat，它仍然適用於 1.1 或更高版本，但不一定適用於 2.0 以上版本。

請注意，“仍然工作”只是指“將編譯並產生相同的輸出”，而不是“在記憶體或時間方面具有相同的性能”。這是一個重要的區別：在次要版本升級期間，可以引入新的啟發式方法或資料類型，這意味著某些給定的問題可以比以前更快或更慢地解決。

我該如何安裝它？

go get github.com/crillab/gophersat && go install github.com/crillab/gophersat

解決 SAT 問題

Gophersat 可以用作獨立求解器（讀取 DIMACS CNF 檔案）或用作任何 go 程式中的函式庫。

要解析 DIMACS 文件，您可以使用以下語法呼叫 gophersat：

 gophersat --verbose file.cnf

其中--verbose是可選參數，使求解器在求解過程中顯示資訊。

Gophersat 還能夠讀取和解決更通用的布林公式，而不僅僅是以用戶不友善的 DIMACS 格式表示的問題。它也本身處理基數約束，即必須至少有 n 個文字為 true 的子句，其中 n > 1。

解決偽布爾問題

Gophersat 可以用作獨立求解器（讀取 OPB 檔案）或用作任何 go 程式中的函式庫。

要解決偽布林問題（無論是決策問題還是最佳化問題），您可以使用以下語法呼叫 gophersat：

 gophersat --verbose file.opb

其中--verbose是可選參數，使求解器在求解過程中顯示資訊。

目前，它只能解決所謂的 DEC-SMALLINT-LIN 問題和 OPT-SMALLINT-LIN，即決策問題（是否有解），用於小整數的線性約束（加權文字的總和） (n < 2^30) ，或最佳化問題（最佳解決方案是什麼，最小化給定的成本函數），用於小整數的線性限制。

解決 MAXSAT 問題

由於maxsat軟體包，Gophersat 現在可以解決 MAXSAT 問題。

要解決加權 MAXSAT 問題，您可以使用以下語法呼叫 gophersat：

 gophersat --verbose file.wcnf

其中--verbose是可選參數，使求解器在求解過程中顯示資訊。該文件應以（WCNF 格式）[http://www.maxsat.udl.cat/08/index.php?disp=requirements] 表示。

什麼是 SAT 求解器？ SAT考試的問題是什麼？

SAT 代表布林可滿足性問題 (Boolean Satisfiability Problem) ，是典型的 NP 完全問題，即在最壞情況下不存在不花費指數時間的已知解決方案的問題。簡而言之，SAT 解算器嘗試為給定的命題公式找到使其所有變數都成立的賦值（如果存在這樣的賦值）。

雖然使用樸素演算法實作 SAT 求解器很簡單，但這種實作在實務上效率非常低。 Gophersat 實現了最先進的功能，因此非常高效，使其可在需要高效推理引擎的 Go 程式中實際使用。

儘管出於實際原因這並不總是最佳決定，但任何 NP 完全問題都可以轉化為 SAT 問題並由 Gophersat 解決。此類問題包括旅行商問題、限制規劃、背包問題、規劃、模型檢查、軟體正確性檢查等。

有關 SAT 問題的更多信息，請參閱維基百科有關 SAT 的文章。

您還可以在教程“SAT for noobs”中找到有關如何表示您自己的布林公式的信息，以便 gophersat 可以使用它們。

什麼是 MAXSAT？

MAXSAT 是 SAT 決策問題的最佳化等價物。純 SAT 求解器將傳回滿足所有子句的模型，如果不存在此類模型，則傳回 UNSAT，而 MAXSAT 求解器將傳回滿足盡可能多的子句的模型。

部分和加權 MAXSAT

MAXSAT 有擴充。

部分MAXSAT意味著，雖然我們希望滿足盡可能多的子句，但無論如何，有些子句（稱為硬子句）必須滿足。因此，部分 MAXSAT 問題可以被認為是不可滿足的。

例如，為學校產生時間表是一個部分MAXSAT 問題：既有軟性問題（例如，我們希望下午4 點之後開始的課程盡可能少），也有硬性問題（兩名教師不能同時在兩個不同的地方）同時）的限制。

加權 MAXSAT意味著條款與成本相關：儘管是可選的，但某些條款被認為比其他條款更重要。例如，如果子句C1 的成本為3，而子句C2 和C3 的成本均為1，則滿足C1 但既不滿足C2 也不滿足C3 的解決方案將被認為比滿足C2 和C3 但不滿足C1的解決方案更好，所有其他解決方案事物是平等的。

部分加權MAXSAT是指問題中同時存在軟子句和硬子句，並對軟子句進行加權。在這方面，「純」MAXSAT 是更通用的部分加權 MAXSAT 的特殊情況：「純」MAXSAT 問題是部分加權 MAXSAT 問題，其中所有子句都是與權重 1 關聯的軟子句。

那麼偽布爾問題呢？

在某種程度上，偽布林問題是 SAT 問題的概括：任何命題子句都可以寫成單一偽布林約束，但表示偽布林約束可能需要指數數量的命題子句。

（線性）偽布林表達式是這樣的表達式：

 w1 l1 + w2 x2 + ... + wn xn ≥ y

其中y和所有wi都是整數常數，所有li都是布林文字。

例如，如果下列表達式為真

 2 ¬x1 + x2 + x3 ≥ 3

布林變數x1必須為 false，且x2和x3至少其中之一必須為 true。這相當於命題公式

 ¬x1 ∧ (x2 ∨ x3)

偽布林表達式是命題子句的概括：任何子句

 x1 ∨ x2 ∨ ... ∨ xn

可以重寫為

 x1 + x2 + ... + xn ≥ 1

偽布爾問題的描述可能比其對應的命題問題小得多，但解決偽布爾問題仍然是 NP 完全的。

Gophersat 解決了決策問題（該問題是否有解決方案）和最佳化問題。最佳化問題是與成本函數相關的偽布爾問題，即必須最小化的項總和。 gophersat 不只是嘗試找到滿足給定限制的模型，而是嘗試找到保證既滿足限制又最小化成本函數的模型。

在搜尋最優解的過程中，gophersat 一旦找到就會提供次優解（即解決所有約束但尚不能保證最優的解），因此用戶可以在給定時間內得到次優解限制，或者等待更長時間以獲得保證的最佳解決方案。

Gophersat 快嗎？為什麼要使用它？

是和不是。它比簡單的實現要快得多，足以用於解決現實世界的問題，但比頂級、高度優化、最先進的求解器慢。

Gophersat 的目標並不是成為最快的 SAT/PB 求解器。目標是讓地鼠能夠存取 SAT 和 PB 技術，而無需借助用其他語言（通常是 C/C++）編寫的求解器的介面。

然而，在某些情況下，與用另一種語言編寫的求解器連接是您的應用程式的最佳選擇。如果您有很多小問題需要解決，Gophersat 將是最快的選擇。對於更大的問題，如果您想以解決問題時間為代價，盡可能減少依賴性，Gophersat 也不錯。如果您需要解決難題並且不介意使用 cgo 或使用外部程序，那麼 Gophersat 可能不是最佳選擇。

Go 中還有其他一些 SAT 解算器，主要是 go-sat 和 gini。根據我們運行的測試，Gini 的性能與 Gophersat 相當，儘管平均速度稍慢一些。

Gophersat 還提供了其他解算器所不具備的酷炫功能（例如，使用者友善的輸入格式），因此它可以用作描述和解決 NP 難題的工具，這些問題可以輕鬆簡化為 SAT/PB問題。