Automatic Decoder Synthesis: Advancements in Communication and Cryptography
Cutting-edge progress in automatic decoder synthesis for communication and cryptography systems, presented in a comprehensive study covering motivation, prior work, preliminary notations, SAT solver algorithms, and experimental findings.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Towards Completely Automatic Decoder Synthesis Presented by Dec. 3, 2010
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
Introduction Motivation Data processing Communication, cryptography Encode-decode system Prior work Craig interpolation
Outline Introduction Preliminary Notation SAT Solver Craig Interpolation State Transition System Problem Statement Main Algorithm Experimental Result Conclusion
Preliminary Notation Boolean vector Cardinality Set of truth valuation
Preliminary SAT Solver For a Boolean vector and a Boolean function , SAT Solver asks whether That is whether is unsatisfiable.
Preliminary Craig interpolation refers to the common variables of and such that unsatisfiable
Preliminary State Transition System Initial states Transition relation Input variables Current-/Next-state variables Output variables
Tn T 1 T0 T1 Tp Preliminary T* 1 T*0 T*1 T*p T* n State Transition System Furthermore ? ? At time t T Duplication ? ? Duplication at time t
Preliminary State Transition System Dangling, recurrent and transition states dangling transition recurrent recurrent
Preliminary Problem Statement Streaming decoder Time-frame expansion of an encoder Finite observing window Prefix and postfix issue Care-state
Outline Introduction Preliminary Main Algorithm Decoder Existence Decoder Synthesis Disjunction on CNF Incremental SAT Experimental Result Conclusion
Decoder Existence(II) the same state information, the same output equivalent constrain. ?? ???? ??? ?????? ???????? ?? ?????? ???????.
Decoder Existence(III) No more information obtain from adding new timeFrame ??????? ????? ? ?????.
Decoder Existence(IV) Decoder existence checking flow.
Decoder Synthesis T n T 1 T0 T1 Tp = = = = = T* n T* 1 T*0 T*1 T*p
Outline Introduction Preliminary Main Algorithm Experimental Result Existence Checking Decoder Synthesis Conclusion
Comparison on Decoder Generation time generate check aig size level
Compare: Decoder Existence Checking Time to check circuit without decoder
Comparison on Existence Checking and Decoder Generation
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
? ? T T ? ?
