1

smtlib2.0 インスタンスを使用して c++ API で maxsat を実行する方法はありますか。つまり、関数 get_soft_constraints を smtlib2.0 インスタンスで動作させる方法は?

4

1 に答える 1

1

いいえ、maxsat例は SMT 2.0 が導入される前に実装されました。この例を変更して、SMT 2.0 ファイルを読み取ることができます。基本的な考え方は、SMT 1.0 の代わりに SMT 2.0 パーサーを使用し、ソフトな制約を特定するメカニズムを考案することです。

于 2012-10-31T16:42:51.470 に答える