合金の中で実行中に「インスタンスが見つかりません」という原因を発見する方法はありますか？

Question

私は合金を使用してモデルで書いています。しかし、ある条件では、述部を実行してインスタンスを見つけることができず、インスタンスが見つからないと言います。私は約16インスタンスにバインドを増加しようとしましたが、インスタンスが見つかりません。

これをデバッグする方法はありますか？どのような事実が原因で合金がインスタンスを見つけることができないのか分かりますか？

ありがとうございます！

Answer 1

デフォルトのsatソルバをunsat coreでminisatに変更すると、同じインスタンスでは満たされない制約を強調表示することができます。

解決策のもう1つは、分析がインスタンスを生成して問題を引き起こす可能性のある制約を突き止めるまで、制約を1つずつコメントすることです。

より具体的な回答は、モデルを共有してください。