問題タブ [satisfiability]

Subgraph Isomorphism (SI) 問題は、2 つのグラフ G と H が入力として与えられる計算タスクであり、G に H と同型のサブグラフが含まれているかどうかを判断する必要があります。

これはNP 完全問題です。

SAT問題との関係を知りたいです。特に、この問題のインスタンスを SAT ソルバー ( miniSAT
など) 全体で解決できるようにしたいと考えています。SI から SAT 問題へのマッピングを多項式時間で実行できるアルゴリズムが必要であり、SAT 割り当てを使用してノードからマッピングを見つけることができます。 G から H のノードへ。

何か案が ？？？

一連のブール方程式を解くために、次の入力を使用してConstraint-Programming Solver MiniZincを試しています。

MiniZincは小さなパラメータの解決策を見つけます(rows=cols=2, products=7)が、わずかに増加したパラメータでは解決しません。生成されたFlatZincモデルをCryptominisat、Lingeling 、またはClaspなどのSAT ソルバーにフィードしたいと考えています。これらのツールが既存の MiniZinc バックエンドよりも優れていることを願っています。

私の質問:純粋な Boolean FlatZincモデルをCNF (DIMACS)
に変換するツールはありますか? MiniZinc バックエンドの一部がサポートしていないように見える ため、述語を置き換えるにはどうすればよいですか?
xorall()

コードに対して間違った答えが返ってきました

n は変数の数で、formula は節を含むリストです

リスト 'formula' でエンコードされた 'n' 個の変数と節を持つ SAT インスタンスを指定すると、インスタンスが満足できる場合は 'satisfiable' を返し、それ以外の場合は 'unsatisfiable' を返します。'formula' の各要素は句を表し、整数のリストです。ここで、整数 i はリテラル Xi が句に存在することを示し、整数 -i はリテラル ~Xi が句に存在することを示します。たとえば、節「X1 v ~X11 v X7」はリスト [1, -11, 7] で表されます。

前回の質問で、SBV ライブラリを利用して命題式を解析し、式のすべてのモデルを見つける方法を尋ねました。ブール式の解析には hatt ライブラリを使用しました。

残念ながら、SBV はかなり高速な SAT 解決には適していないか、すべてのモデルを検索する「allSat」機能が高速化のために実装されていないようです。やはりSBVはSMT解決を目指しています。

picosat と比較して、プルーバー Z3 および CVC4 を使用して、haskell SBV パッケージのパフォーマンスをテストしました。36 個の変数と 840 個の有効なモデルを含む命題の公式を使用しました。picosat の結果は、0.5 秒かかったのに対し、Z3 は 3 分、CVC4 は 6 分かかりました。SBV と "allSat" 関数を使用して、命題の式のためにそれをトリミングするためのいくつかのパフォーマンスのトリックがあります。または、他の証明者が Z3 よりも高速である可能性があります。

しかし、SAT を解くにはより高速なオプションを使用する必要があると思います。過去に良い結果があり、SAT 競技の結果も良さそうなので、PicoSAT または MiniSAT を使用したいと考えています。

質問:

• 命題式のすべてのモデル (つまり、高速な結果を得るための C/C++ レベル)を見つけるのに適した、Picosat または MiniSAT へのバインディングはありますか? たとえば、picosat への python バインディングは、それを行う関数「itersolve」を備えています。しかし、haskell の picosat や miniSAT のバインディングについては、この関数を見つけることができませんでした (おそらく見落としていたのでしょう)。

• hatt パッケージで解析された文字列から、picosat/miniSat に適した「int リスト」に進むにはどうすればよいですか。したがってExpr、hatt ライブラリの型の式から、たとえば picosat に適したスタイルで CNF 式を表現することになります。Picosat は、int のリストの一般的な SAT 形式を使用します。文字列から解析された私の数式は、もともと既に CNF にあることに注意してください。または、hatt Expr から int リストに直接移動します。または、前回の質問のコードを SBVの機能に適した形式に使用し、SBVallSatの機能のバリアントを再実装して、allSATpicosat/miniSAT の hasekll バインディングを使用します。

リンク:

• 私の最後の質問
• SBV ライブラリ
• ハット図書館
• haskell picosat バインディング
• ミニットSAT

haskellでランダムな命題式を取得するにはどうすればよいですか? できればCNFの式が必要ですが、そうします

私は、SAT ソルバーも含むパフォーマンス テストの式を使用したいと考えています。私の目標は、SAT ソルバーのパフォーマンスをテストすることではないことに注意してください。私は非常に難しい数式にも興味がないので、難易度はランダムにするか、簡単な数式のみを含める必要があります。

私の現実世界のデータは、SAT ソルバーにとって難しくない命題の公式につながることを知っています。

現時点では、HattライブラリとSBVライブラリをデータ構造として使用して、命題式を操作しています。hGenライブラリも調べました。おそらく、ランダムな式を生成するために使用できます。ただし、ドキュメントはなく、hGenのソース コードを見てもうまくいきませんでした。

私の目標は、ブール変数nを含む数式を選択して取得することです。n

CNFの命題式を使用して文字列をDIMACSに解析したいので、haskellのネストされたintリストです。この形式は、SAT 解決の他のオプションよりもパフォーマンスが高いと思われる haskell picosat バインディングに適しています。

問題は、これを実装したコードが複雑すぎることです。現在、見つけにくいバグの可能性を探しています。

(私のアプローチは、haskell hatt パッケージを使用し、パッケージを変更して、変数名に単一文字の代わりに文字列を使用し、hatt で式を解析し、結果の式を DIMACS 形式に変換することでした。)

CNF 記法で命題式を表す文字列を解析したい (以下の例を参照)。結果は、ネストされた int のリストになります。したがって、結果はhaskell picosat bindingssolveAllの一部に適しているはずです。

入力：

結果：