Comparison of schemes for encoding unobservability in translation to SAT
Comparison of schemes for encoding unobservability in translation to SAT
复制标题
翻译成 SAT 时不可观察性编码方案的比较
DOI：
10.1145/1120725.1120823
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
M. Velev
中科院分区：
文献类型：
--
作者：
M. Velev
比较了布尔-CNF转换中逻辑块不可观测性的七种编码方案。四个方案是基于合并的逻辑块与相邻的门向主输出。两个是基于使用CNF不可观测变量编码的逻辑块的不可观测性。还探讨了一种混合方案。对逻辑块的不可观测性进行编码加速了复杂微处理器形式验证中布尔公式的SAT求解，同时允许我们使用传统的基于CNF的SAT求解器。在不可满足的CNF公式中，最好的策略是将逻辑块与从块输出到主输出的唯一路径上的相邻门合并，对于具有数十万个变量，数百万个子句和数千万个文字的CNF公式，加速高达16倍。此外，加速是相对于已经非常有效的布尔到CNF转换。在可满足的CNF公式中，最好的策略是将逻辑块与叶门合并，并与通向主输出的唯一路径上的相邻门合并，以及利用门和逻辑块的极性来减少子句的数量。所提出的优化方法是通用的，并适用于其他类型的布尔公式。
Compared are seven schemes for encoding unobservability of logic blocks in Boolean-to-CNF translation. Four of the schemes are based on merging of logic blocks with adjacent gates toward the primary output. Two are based on using CNF unobservability variables to encode the unobservability of logic blocks. Also explored is a hybrid scheme. Encoding the unobservability of logic blocks accelerated the SAT-solving of Boolean formulas from formal verification of complex microprocessors, while allowing us to use a conventional CNF-based SAT-solver. On unsatisfiable CNF formulas, best was the strategy of merging logic blocks with adjacent gates on the only path from the block output to the primary output, with a resulting speedup of up to 16x for CNF formulas with hundreds of thousands of variables, millions of clauses, and tens of millions of literals. Furthermore, the speedup is relative to an already very efficient Boolean-to-CNF translation. On satisfiable CNF formulas, best was the strategy of merging logic blocks with leaf gates and with adjacent gates on the only path to the primary output, as well as exploiting the polarity of gates and logic blocks to reduce the number of their clauses. The presented optimizations are general and applicable to other classes of Boolean formulas.