3

私は MAX-SAT に興味があり、Z3 にこれが組み込まれていることを期待していました。近い将来、これを行う計画はありますか?

上記がない場合、コマンドラインから maxsat アプリケーションの例を使用してみました。残念ながら、exec.sh "filename.z3" を実行すると、常に次の応答が返されます。私は何を間違っていますか？この応答は、ファイルの実際の内容とはまったく無関係であるように思われます。

最後に、maxsat の例のコメントでは、制約をハードまたはソフトとしてマークする方法が明確に指定されていません。ハード制約は :formula が前に付いた式であり、ソフト制約は :assumption が前に付いた式です。では、"(assert (> x 0))" をソフトとしてマークするには、":assumption" を正確にどこに置くのでしょうか? (私はハード制約とソフト制約に関するクエリを読みましたが、満足できない式の「最大の満足できるコア」とは対照的に、満足できないコアを見つけるという文脈で質問/応答がより多くのように見えました。)

4

1 に答える 1

2

Z3 ディストリビューションの MaxSAT サンプルは、Z3 API を使用して 2 つの MaxSAT アルゴリズムを実装する方法を示しています。この例では、制約をアサートするために古い (非推奨の) API を引き続き使用していますが、新しいソルバー API を使用するように簡単に変更できます。サンプル アプリケーションは、SMT 1.0 ファイルを読み取ります。ただし、MaxSAT 関数は、C API を使用して作成された数式で使用できます。:assumptionスクリプトは、フィールドがソフトな制約で:formulaあり、ハードな制約であると想定しています。ここに小さな例があります。ここで(> x 0)、 、(> y 0)、(< x y)および(> x (- y 1))はソフト制約であり、(> (+ x y) 0)および(< (- x y) 100)はハード制約です。サンプル アプリケーションは を返します3。つまり、最大 3 つの柔軟な制約を満たすことができます。

(benchmark ex
  :extrafuns ((x Int))
  :extrafuns ((y Int))
  ;; Soft Constraints
  :assumption (> x 0)
  :assumption (> y 0)
  :assumption (< x y)
  :assumption (> x (- y 1))
  :formula 
  (and 
  ;; Hard Constraints
  (> (+ x y) 0)
  (< (- x y) 100)
))

そうは言っても、Z3 API で MaxSAT を直接サポートする予定はありません。将来のバージョンでは、MaxSAT の例を他の API (.NET、Python、および C++) に移植する可能性があります。

于 2012-05-22T01:07:09.163 に答える