Issue No. 04 - July/August (2003 vol. 20)
Jo? Marques-Silva , Technical University of Lisbon
Lu? Guerra e Silva , Technical University of Lisbon
<p><div><em>Editor's note: </em></div>As EDA evolves, researchers continue to find modeling tools to solve problems of test generation, design verification, logic, and physical synthesis, among others. One such modeling tool is Boolean satisfiability (SAT), which has very broad applicability in EDA. The authors review modern SAT algorithms, show how these algorithms can account for structural information in combinational circuits, and explain what recursive learning can add to SAT.<div><em>—Marcelo Lubaszewski, Federal University of Rio Grande do Sul</em></div></p>
J. Marques-Silva and L. Guerra e Silva, "Solving Satisfiability in Combinational Circuits," in IEEE Design & Test of Computers, vol. 20, no. , pp. 16-21, 2003.