Towards Parallel Boolean Functional Synthesis

Given a relational specification \(\varphi (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.

• Publication year

  2017

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  2017-03-04

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-662-54577-5_19arXiv 1703.01440
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Mathematical Analysis Of Logic

  2016cited by this paper
• BDD-Based Boolean Functional Synthesis

  2016influential reference
• Skolem functions for factored formulas

  2015influential reference
• Efficient extraction of Skolem functions from QRAT proofs

  2014cited by this paper
• Boolector 2.0

  2014cited by this paper
• Template-based program verification and program synthesis

  2013cited by this paper
• Resolution Proofs and Skolem Functions in QBF Evaluation and Applications

  2011cited by this paper
• Complete functional synthesis

  2010cited by this paper
• A Recursive Paradigm to Solve Boolean Relations

  2009cited by this paper
• Quantifier Elimination via Functional Composition

  2009influential reference
• Programming by sketching for bit-streaming programs

  2005cited by this paper
• sKizzo: A Suite to Evaluate and Certify QBFs

  2005cited by this paper
• Program Repair as a Game

  2005cited by this paper
• A recursive paradigm to solve boolean relations

  2004cited by this paper
• Counterexample-guided abstraction refinement for symbolic model checking

  2003cited by this paper
• Robust Boolean reasoning for equivalence checking and functional property verification

  2002cited by this paper
• Building Circuits from Relations

  2000cited by this paper
• Binary Decision Diagrams

  1999influential reference
• Comparing different Boolean unification algorithms

  1998cited by this paper
• On the Complexity of Boolean Unification

  1998cited by this paper
• Unification in Boolean Rings and Abelian Groups

  1989cited by this paper
• Boolean Unification - The Story So Far

  1989cited by this paper
• Supervisory control of a class of discrete event processes

  1987cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• On the Complexity of Derivation in Propositional Calculus

  1983cited by this paper
• Parametric solutions of Boolean equations

  1972cited by this paper
• The mathematical analysis of logic

  1948cited by this paper
• Über die Auflösung von Gleichungen im logischen Gebietekalkul

  1910influential reference

• The Limitations and Power of NP-Oracle-Based Functional Synthesis Techniques

  2025cites this paper
• Synthesis with Explicit Dependencies

  2023cites this paper
• An Approximate Skolem Function Counter

  2023cites this paper
• Tractable representations for Boolean functional synthesis

  2023cites this paper
• Synthesizing Skolem functions: A view from theory and 1 practice 2

  2022influential citation
• On synthesizing Skolem functions for first order logic formulae

  2021cites this paper
• On Synthesizing Computable Skolem Functions for First Order Logic

  2021cites this paper
• Projected Model Counting: Beyond Independent Support

  2021cites this paper
• Engineering an Efficient Boolean Functional Synthesis Engine

  2021cites this paper
• A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis

  2021cites this paper
• Boolean functional synthesis: hardness and practical algorithms

  2020cites this paper
• Manthan: A Data-Driven Approach for Boolean Function Synthesis

  2020cites this paper
• Knowledge Compilation for Boolean Functional Synthesis

  2019influential citation
• Incremental Determinization for Quantifier Elimination and Functional Synthesis

  2019cites this paper
• Chasing Minimal Inductive Validity Cores in Hardware Model Checking

  2019cites this paper
• Functional Synthesis via Input-Output Separation

  2018influential citation
• Computer Aided Verification

  2018influential citation
• What's hard about Boolean Functional Synthesis

  2018influential citation
• Derivation of a Scalable Solution for the Problem of Factoring an n-bit Integer

  2018cites this paper
• Derivation of All Particular Solutions of a ‘Big’ Boolean Equation with Applications in Digital Design

  2018cites this paper
• Factored boolean functional synthesis

  2017cites this paper
• Pushing The Envelope for Boolean Functional Synthesis

  2017influential citation