SMTLIB2 構文を使用して、満足のいくすべての割り当てを取得する方法はありますか?
私が使用しているソルバーは Z3 と CVC4 です。
質問する
103 次
1 に答える
0
これを「純粋な」SMTLIB2 で行う方法はありません。つまり、1 つのファイルだけで外部入力を使用しない場合、ソルバーとやり取りできるアプリケーションがある場合は、標準的な方法でこれを行うことができます。ソルバーをインタラクティブ モードで実行すると、一度に 1 つずつ SMTLIB2 コマンドを送信し、次の方法で対話できます (疑似コード)。
def get_all_assignments(instance):
create solver in interactive mode
for each declaration, assertion, etc. in instance:
send assertion to solver
let response := None
while response is not UNSAT:
send command '(check-sat)' to solver and get response
if response is SAT:
send command '(get-model)' to solver and get model
print model
send the solver a new assertion which is the negation of the model
事実上、満足のいく割り当てを見つけるたびに、モデルに新しい制約を追加して、ソルバーがその割り当てを再び見つけられないようにし、再解決するように依頼します。ソルバーが UNSAT を返すと、満足のいく割り当てがすべて見つかったことがわかります。
このトピックの詳細と Z3 の実装については、Z3: 条件を満たすすべてのモデルの検索とZ3py: 方程式のすべての解の確認を参照してください。
于 2015-11-18T22:36:27.947 に答える