Functional Synthesis via Input-Output Separation

Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

תקציר

Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite significant recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem even when state-of-the-art methods are used for decomposing the specification. In this work we bring a fresh decomposition approach, orthogonal to existing methods, that explores the decomposition of the specification into separate input and output components. We make use of an input-output decomposition of a given specification described as a CNF formula, by alternatingly analyzing the separate input and output components. We exploit well-defined properties of these components to ultimately synthesize a solution for the entire specification. We first provide a theoretical result that, for input components with specific structures, synthesis for CNF formulas via this framework can be performed more efficiently than in the general case. We then show by experimental evaluations that our algorithm performs well also in practice on instances which are challenging for existing state-of-the-art tools, serving as a good complement to modern synthesis techniques.

שפה מקוריתאנגלית
כותר פרסום המארחProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
עורכיםNikolaj Bjorner, Arie Gurfinkel
מוציא לאורInstitute of Electrical and Electronics Engineers Inc.
עמודים139-147
מספר עמודים9
מסת"ב (אלקטרוני)9780983567882
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - 2 יולי 2018
פורסם באופן חיצוניכן
אירוע18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 - Austin, ארצות הברית
משך הזמן: 30 אוק׳ 20182 נוב׳ 2018

סדרות פרסומים

שםProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

כנס

כנס18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
מדינה/אזורארצות הברית
עירAustin
תקופה30/10/182/11/18

הערה ביבליוגרפית

Publisher Copyright:
© 2018 FMCAD Inc.

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'Functional Synthesis via Input-Output Separation'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי