SAT见证生成器中可扩展性与均匀性的平衡
计算机科学中的逻辑
2014-03-26 v1
摘要
约束随机仿真是工业界用于复杂数字设计功能验证的主要方法。该方法的有效性取决于两个关键因素：用于生成测试向量的约束质量，以及从给定约束集生成的解的随机性。本文聚焦于第二个问题，提出了一种显著改进大规模布尔约束解（几乎）均匀生成现有技术的算法。该算法在生成解的均匀性方面提供了强理论保证，并能扩展到涉及数十万变量的问题。
引用
@article{arxiv.1403.6246,
title = {Balancing Scalability and Uniformity in SAT Witness Generator},
author = {Supratik Chakraborty and Kuldeep S. Meel and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1403.6246},
year = {2014}
}
备注
This is a full version of DAC 2014 paper