תקציר
Boolean functional synthesis is the process of automatically obtaining a constructive formalization from a declarative relation that is given as a Boolean formula. Recently, a framework was proposed for Boolean functional synthesis that is based on Craig Interpolation and in which Boolean functions are represented as And-Inverter Graphs (AIGs). In this work we adapt this framework to the setting of Binary Decision Diagrams (BDDs), a standard data structure for representation of Boolean functions. Our motivation in studying BDDs is their common usage in temporal synthesis, a fundamental technique for constructing control software/hardware from temporal specifications, in which Boolean synthesis is a basic step. Rather than using Craig Interpolation, our method relies on a technique called Self-Substitution, which can be easily implemented by using existing BDD operations. We also show that this yields a novel way to perform quantifier elimination for BDDs. In addition, we look at certain BDD structures called input-first, and propose a technique called TrimSubstitute, tailored specifically for such structures. Experiments on scalable benchmarks show that both Self- Substitution and TrimSubstitute scale well for benchmarks with good variable orders and significantly outperform current Boolean-synthesis techniques.
שפה מקורית | אנגלית |
---|---|
כותר פרסום המארח | Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings |
עורכים | Swarat Chaudhuri, Azadeh Farzan |
מוציא לאור | Springer Verlag |
עמודים | 402-421 |
מספר עמודים | 20 |
מסת"ב (מודפס) | 9783319415390 |
מזהי עצם דיגיטלי (DOIs) | |
סטטוס פרסום | פורסם - 2016 |
פורסם באופן חיצוני | כן |
אירוע | 28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, קנדה משך הזמן: 17 יולי 2016 → 23 יולי 2016 |
סדרות פרסומים
שם | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
כרך | 9780 |
ISSN (מודפס) | 0302-9743 |
ISSN (אלקטרוני) | 1611-3349 |
כנס
כנס | 28th International Conference on Computer Aided Verification, CAV 2016 |
---|---|
מדינה/אזור | קנדה |
עיר | Toronto |
תקופה | 17/07/16 → 23/07/16 |
הערה ביבליוגרפית
Publisher Copyright:© Springer International Publishing Switzerland 2016.