Alloy Analyzerが考慮するケースの数を見つける方法はありますか？

Question

付録E ソフトウェアアブストラクションには、Hotel Operationsのモデルがあります。モデルはアサートNoIntruderと命名されています。

check NoIntruder for 6 but 12 Time, 3 Room, 3 Guest 

は合金アナライザはチェックコマンドのその評価に考えていることを例数を確認する方法はあります：アサートが、このコマンドを使用して評価されますか？アナライザーからのこのメッセージは、ケースの数を示していますか？

Executing "Check NoIntruder for 6 but 12 Time, 3 Room, 3 Guest" 
    Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 
    38549 vars. 921 primary vars. 76238 clauses. 90ms. 
    No counterexample found. Assertion may be valid. 2914ms. 

Answer 1

「考慮する」とは何かを意味します。最も広い意味では、探索の状態空間は2^vであり、ここで、vはブール変数の数であり、この場合は38,459である。もちろん、SATアナライザは、プルーニングのためにインスタンスが見つからなくても、そのスペース全体を検索する必要はありません。