5

リンク:
Z3 定理証明者
picosat と pyhton バインディング

Z3 を SAT ソルバーとして使用しました。より大きな数式ではパフォーマンスの問題があるように思われるため、ピコサットをチェックして、それがより高速な代替手段であるかどうかを確認したかったのです. 私の既存の python コードは、z3 構文で命題式を生成します。

from z3 import *

import pycosat
from pycosat import solve, itersolve

#
#1 2  3  4  5  6  7   8  (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))

# formula in Z3:
f = simplify(C)

print f

出力/結果

And(S,
    Or(Not(S), P),
    Or(Not(P), S),
    Or(Not(P), B),

    Or(Not(C), P),
    Or(Not(G), P),
    Or(Not(M), P),
    Or(Not(R), P),
    Or(Not(SN), P),
    Or(Not(B), P))

ただし、Picosat は、次の例に示すように、数値のリスト/配列を使用します (「clauses1」: 6 は変数 P を参照し、-6 は「非 P」を意味するなど)。

import pycosat
from pycosat import solve, itersolve
#
# use pico sat
#
nvars = 8
clauses =[
    [6],
    [-6, 4],   ##  "Or(Not(S), P)" from OUPUT above
    [-4, 6],
    [-4, 8],
    [-1, 4],
    [-2, 4],
    [-3, 4],
    [-5, 4],
    [-7, 4],
    [-8, 4]]

#
# efficiently find all models of the formula
#
sols = list(itersolve(clauses, vars=nvars))
print "result:"
print sols
print "\n\n====\n"

CNF の式を表す Z3 変数 (コード例の変数 "f" など) を、picosat が CNF の式を表すために使用する前述の形式に変換するための簡単なソリューションとして何をお勧めしますか? Z3 の python API を実際に使用してみましたが、ドキュメントが不十分で、自分で問題を解決することはできませんでした。

(上記の例は単に概念を示しているだけであることに注意してください。変数 C で表される式は動的に生成され、z3 で直接効率的に処理するには複雑すぎます)

4

1 に答える 1

5

まず、Z3 式を CNF に変換する必要があります。次の投稿でこの問題に対処します

Z3 CNF 式を Dimacs に変換するには、それをトラバースして整数のリストのリストを生成する関数を書くだけです。次の 2 つの投稿では、Z3 式をトラバースする方法について説明します。

最後に、式から値へのマップが必要な場合は、次のアプローチを使用できます

于 2013-10-24T15:52:50.603 に答える