Solving Satisfiability in Combinational Circuits with Bactrack Search and Recursive Learning

João P. Marques-SilvaLuís Guerra e Silva

Boolean Satisfiability (SAT) is widely accepted as a ubiquitous modeling tool in Electronic Design Automation (EDA). It finds application in test pattern generation, delay-fault testing, equivalence checking and circuit delay computation, among many other problems. This paper starts by describing how Boolean Satisfiability algorithms can take circuit structure into account when solving instances derived from combinational circuits. Afterwards, it shows how recursive learning techniques can be incorporated into Boolean Satisfiability algorithms. The proposed algorithmic framework has several natural applications in EDA. Moreover, potential advantages include smaller run times, the utilization of circuit-specific search pruning techniques, avoiding the over-specification problem that characterizes Boolean Satisfiability testers, and reducing the time for iteratively generating instances of SAT from circuits. The experimental results obtained on a large number of benchmark examples in different problem domains illustrate the effectiveness of the proposed techniques.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: