Sciweavers

SAT
2004
Springer

Encoding Global Unobservability for Efficient Translation to SAT

13 years 9 months ago
Encoding Global Unobservability for Efficient Translation to SAT
The paper studies the use of global unobservability constraints in a CNF translation of Boolean formulas, where the unobservability of logic blocks is encoded with CNF unobservability variables and the logic output values of the blocks with CNF logic variables. Each block’s unobservability variable is restricted by local unobservability constraints, expressing conditions that the output value of the block will not propagate to the primary output, given values of inputs to nearby gates on the path to the primary output. Global unobservability constraints add conditions that a block is unobservable if all paths to the primary output pass through logic blocks that are unobservable. By introducing a cut of unobservability check-points at the inputs of the top gate in a Boolean formula, we can impose global unobservability constraints for every logic block. The results show that global unobservability constraints lead to small additional speedup if local unobservability is exploited, but ...
Miroslav N. Velev
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAT
Authors Miroslav N. Velev
Comments (0)