完全测试集及其近似

我们使用测试来检查组合电路$N$是否恒等于0（写作$N \equiv 0$）。我们将证明$N \equiv 0$的一组测试称为完全测试集（CTS）。传统观点是，要证明$N \equiv 0$必须生成平凡的CTS。它由全部$2^{|X|}$个输入赋值组成，其中$X$是$N$的输入变量集合。我们利用稳定赋值集（SSA）的概念表明，可以构建由少于$2^{|X|}$个测试组成的非平凡CTS。给定一个不可满足的CNF公式$H(W)$，$H$的SSA是证明$H$不可满足的$W$的赋值集。平凡SSA是$W$的全部$2^{|W|}$个赋值。重要的是，现实生活中的公式可以具有远小于$2^{|W|}$的非平凡SSA。一般而言，即使构建非平凡CTS也是低效的。我们描述了一种更高效的方法，其中测试是从为$N$在$N$的变量子集上的“投影”构建的SSA中提取的。这些测试可视为$N$的CTS的近似。我们给出了实验结果并描述了该方法的潜在应用。