z3 - z3 のメモリ使用量

Question

線形ハイブリッド オートマトンの到達可能性の問題を解決するために z3 を使用しています。限られたメモリの下で実験を実行します。メモリ使用量について混乱しています。z3 が 2500 という限られたメモリ内で解決できる場合があります。ただし、2000 に設定すると、z3 のメモリ使用量が最大許容量を超えます。これはなぜですか?

Answer 1

SMT2 ファイル内の制約の数が少ないからといって、Z3 が問題を解決するために使用するメモリが少なくなるとは限りません。たとえば、小さくても満足できない問題は、満足できる大きな問題よりも多くのメモリを必要とする場合があります。

オートマトンの巻き戻しに下限を設定すると、(境界 2500 での) 充足可能な問題が (境界 2000 での) 充足不可能な問題に変わり、Z3 の問題がより困難になります。制約。その結果、Z3 はより多くの時間やメモリを使用します。

これを回避するには、問題を別の方法でエンコードするか、ソルバーで別のオプションを使用する必要があります。たとえば、ヒューリスティックを調整して、より頻繁に「幸運」になり、解決策をより早く見つけるようにします。