專用集成電路與系統國家重點實驗室
講座信息

題 目👩🏿‍🍳：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.

聯系人：王伶俐