专用集成电路与系统国家重点实验室
讲座信息

题 目：Canonical Computation without Canonical Data Structure （to appear in DAC’2018）
报告人：Dr. Alan Mishchenko （UC Berkeley）
时 间：2018年3月16日上午9:30-11:30
地 点：张江校区微电子楼369室

Abstract
A computation is canonical if the result depends only on the Boolean function and a selected variable order, and does not depend on how the function is represented and how the computation is implemented. In the context of Boolean satisfiability (SAT), canonicity implies that the result (a satisfying assignment for satisfiable instances and a UNSAT core for unsatisfiable ones) does not depend on the circuit structure, CNF generation algorithm, and the SAT solver used. The main highlight of this presentation is that SAT-based computations can be made canonical without building a canonical data-structure. The runtime overhead for inducing canonicity is relatively small and is often justifies by the uniqueness of solution and the improved quality of results.

Biography
Alan Mishchenko graduated from Moscow Institute of Physics and Technology (Moscow, Russia) in 1993 with M.S.and received his Ph.D. from the Glushkov Institute of Cybernetics (Kiev, Ukraine) in 1997. In 2002, he joined the EECS Department at UC Berkeley, where he is currently a full researcher. Alan’s research interests are in developing computationally efficient methods for synthesis and verification.

联系人：王伶俐