非線形の実数演算に z3 を使用すると、タイムアウトの問題が発生します。次のコードは、4 次元超長方形の体積が 50000 を超えており、いくつかの制約も満たしているかどうかを確認するものです。しかし、z3 は 1 分以内に応答できません。速くする方法は？
a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')
s = Tactic('qfnra-nlsat').solver()
s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min > 0.0,
a0min < a0max,
a0max < 1000000.0,
a1min > 0.0,
a1min < a1max,
a1max < 1.0,
a2min > 1.0,
a2min < a2max,
a2max < 1000.0,
a3min > 1.0,
a3min < a3max,
a3max < 50.0,
(a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min))
print s.check()
興味深いことに、">" と "<" の一部を "<=" と ">=" に置き換えると、z3 ソルバーは 2 秒で答えを返すことができます。対応するコードは次のとおりです。なぜこれが起こるのか誰にも分かりますか？
a0min = Real('a0min')
a0max = Real('a0max')
a1min = Real('a1min')
a1max = Real('a1max')
a2min = Real('a2min')
a2max = Real('a2max')
a3min = Real('a3min')
a3max = Real('a3max')
volume = Real('volume')
s = Tactic('qfnra-nlsat').solver()
s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0,
a0min >= 0.0,
a0min <= a0max,
a0max <= 1000000.0,
a1min >= 0.0,
a1min <= a1max,
a1max <= 1.0,
a2min >= 1.0,
a2min <= a2max,
a2max <= 1000.0,
a3min >= 1.0,
a3min <= a3max,
a3max <= 50.0,
(a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min) > 50000.0,
volume == (a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min))
print s.check()