Mar, 2014

在 SAT 证据生成器中平衡可扩展性和一致性

TL;DR本文提出了一种基于算法的方法来解决 “几乎均匀地生成大型布尔约束条件的解” 的问题,该算法在解的均匀性方面提供了强大的理论保证,并可适用于涉及数十万个变量的问题。