z3 - Z3: 開始値の設定

Question

制約を満たすために特定の開始値から検索するように Z3 に依頼できますか?

たとえば、 と が 2 つRealExprs xありy、x==y制約として があるとします。Z3 から検索して、Z3 が「SAT」と言うx=-9999, y=-9997モデルを返すように依頼できますか?x=-9998 and y=-9998

Answer 1

私があなたの質問を理解している限り、あなたは最大化/最小化の問題、つまり次の関数の解決策を探しています

f(x, y) = |x + 9999| + |y + 9997|

制約とともにx = y。この質問への回答で述べたように、Z3 は現在これを直接サポートしていません。ただし、前述のように、以前に見つかったソリューションを次のクエリの新しい制約として追加する Python ループ内で Z3 をクエリすることにより、このような問題の解決を試みることができます。