無需阻塞子句的 SAT 和 SMT 不相交投影枚舉算法

本文提出了一種名為 TabularAllSAT 和 TabularAllSMT 的新型 AllSAT 和 AllSMT 求解器，它們結合了衝突驅動子句學習 (CDCL) 和時間回溯，在不使用阻塞子句的情況下實現了高效的不相交枚舉，並通過積極的蘊含項簡化算法來減少搜索空間。