选一个公式，看它的真值表，系统自动判定它属于重言式、矛盾式还是可满足式。

判定标准：真值表全为 1 → 重言式（永真式）；全为 0 → 矛盾式（永假式）； 至少有一个 1 → 可满足式。所以「可满足式」包含重言式，而矛盾式一定不可满足。