完全测试集的生成
计算机科学中的逻辑
2018-04-03 v1
摘要
我们使用测试来检查组合电路 N 是否总是求值为 0。通常的观点是，要证明 N 总是求值为 0，必须检查 N 在所有 2^|X| 个输入赋值下的值，其中 X 是 N 的输入变量集合。我们使用稳定赋值集（SSA）的概念来表明，可以构建一个完全测试集（即证明 N 总是求值为 0 的测试集），其包含的测试少于 2^|X| 个。给定一个不可满足的 CNF 公式 H(W)，H 的 SSA 是证明 H 不可满足的 W 的赋值集合。一个平凡的 SSA 是 W 的所有 2^|W| 个赋值的集合。重要的是，现实生活中的公式可以具有远小于 2^|W| 的 SSA。仅使用 SSA 的机制为 N 生成完全测试集是低效的。我们描述了一种快得多的算法，它将 SSA 的计算与归结推导相结合，并为 N 在 N 的变量子集上的“投影”生成完全测试集。我们给出了实验结果并描述了该算法的潜在应用。
引用
@article{arxiv.1804.00073,
title = {Generation of complete test sets},
author = {Eugene Goldberg},
journal= {arXiv preprint arXiv:1804.00073},
year = {2018}
}