既存のSMTソルバを使用して、QF_UF公式の等価ブール式を得ることは可能ですか？

熱心なSMTソルバでは、SMT式は、同等のブール式としてエンコードされ、SATソルバに供給されます。通常、QF_UFの式では、未知の関数はAckermannの減少またはブライアントの減少によって減少し、等値グラフの手法によって等価ブール式が構築されます。既存のSMTソルバを使用して、QF_UF公式の等価ブール式を得ることは可能ですか？

ソルバの低レベルの実装をハックすることなく、QF_UFの公式で同等のブール式を得るために既存のSMTソルバを呼び出すことが可能かどうかを知りたいと思います。たとえば、Z3には入力問題（たとえばtseitin-cnfとelim-term-iteなど）を変換するためのいくつかの戦術があり、そのような変換のための戦術はありますか？

出典

2017-07-13 cxcfan

Z3では、ブールZ3変数の上になりますhttps://gist.github.com/nunoplopes/8cd9fb433b2663c99cb34c8a95ae812f

ます。また、SAT式を取得するには、ビットブラスト戦術を使用することができるようなパッチ、とDIMACSをダンプすることができます。私はそれがCNFかNNFかどんな形式であることが保証されているとは思わない。

出典

2017-07-13 12:33:12

私は後で最初の解決策を試みます。 QF_UF問題（[リンク]（http://rise4fun.com/Z3/hWVI））に 'ビットブラスト '戦術を適用しようとすると、出力はまだQF_UFの問題です。私は何か間違ったことをしたのですか、「ビットブラスト」戦術はBVの問題のみをサポートしていますか？ – cxcfan

ああ、そうです。最初にUFシンボルを取り除く必要があります。 Ackermannizationの戦術があります。名前はackermannize_bv IIRCです。 –

ありがとうございました。 UFのシンボルが減少しました。しかし、QF_UFの問題をSATの式に変換するのに、ビットブラストはまだ機能していないことがわかりました（[example]（http://rise4fun.com/Z3/MSfEo））。 QF_UF式を非ゼロアリティの未解釈関数なしでSAT式に変換するための作業方法はありますか？ありがとうございました！ – cxcfan

既存のSMTソルバを使用して、QF_UF公式の等価ブール式を得ることは可能ですか？

答えて

関連する問題