Towards Parallel Boolean Functional Synthesis
From MaRDI portal
Abstract: Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.
Recommendations
- Boolean circuit programming: A new paradigm to design parallel algorithms
- Boolean functional synthesis: hardness and practical algorithms
- Parallel algorithms for evaluation of directional Boolean derivatives of multivalued logic functions
- Parallel and sequential computation on Boolean networks
- Boolean functional synthesis: from under the hood of solvers
- Generation of universal series-parallel Boolean functions
- BDD-based Boolean functional synthesis
- Exploiting regularities for Boolean function synthesis
- scientific article; zbMATH DE number 2073566
- On the construction of parallel computers from various basis of Boolean functions
Cites work
- A Recursive Paradigm to Solve Boolean Relations
- Automated Deduction – CADE-20
- BDD-based Boolean functional synthesis
- Binary Decision Diagrams
- Boolean unification - the story so far
- Computer Aided Verification
- Counterexample-guided abstraction refinement for symbolic model checking
- Graph-Based Algorithms for Boolean Function Manipulation
- scientific article; zbMATH DE number 1670772 (Why is no real title available?)
- scientific article; zbMATH DE number 3062907 (Why is no real title available?)
- On the complexity of Boolean unification
- Parametric solutions of Boolean equations
- Quantifier Elimination via Functional Composition
- Supervisory Control of a Class of Discrete Event Processes
- Unification in Boolean rings and Abelian groups
Cited in
(15)- Boolean circuit programming: A new paradigm to design parallel algorithms
- Boolean functional synthesis: hardness and practical algorithms
- Lazy but effective functional synthesis
- Generation of universal series-parallel Boolean functions
- A dual rail circuits synthesis environment for the implementation of multiple output boolean functions
- scientific article; zbMATH DE number 589878 (Why is no real title available?)
- BDD-based Boolean functional synthesis
- What's hard about Boolean functional synthesis?
- Functional synthesis via input-output separation
- Boolean functional synthesis: from under the hood of solvers
- Projected model counting: beyond independent support
- Efficient synthesis of a class of Boolean programs from I-O data: application to genetic networks
- ZDD Boolean synthesis
- Counterexample guided knowledge compilation for Boolean functional synthesis
- Tractable representations for Boolean functional synthesis
This page was built for publication: Towards Parallel Boolean Functional Synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303903)