Solving satisfiability in combinational circuits
João P. Marques-Silva, Luís Guerra e Silva · IEEE Design & Test of Computers · 2003
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.