The automated synthesis of correct-by-construction Boolean functions from
logical specifications is known as the Boolean Functional Synthesis (BFS)
problem. BFS has many application areas that range from software engineering to
circuit design. In this paper, we introduce a tool BNSynth, that is the first
to solve the BFS problem under a given bound on the solution space. Bounding
the solution space induces the synthesis of smaller functions that benefit
resource constrained areas such as circuit design. BNSynth uses a
counter-example guided, neural approach to solve the bounded BFS problem.
Initial results show promise in synthesizing smaller solutions; we observe at
least \textbf{3.2X} (and up to \textbf{24X}) improvement in the reduction of
solution size on average, as compared to state of the art tools on our
benchmarks. BNSynth is available on GitHub under an open source license.

该论文介绍了一种名为 BNSynth 的工具，它是解决具有解决方案空间范围限制的 BFS 问题的第一个工具，该工具利用反例指导的神经方法去综合较小的函数，并且相比现有的工具，平均方案大小减少了至少 3.2 倍（最高可达 24 倍）。

BNSynth: 有界布尔函数综合

BNSynth: Bounded Boolean Functional Synthesis

Boolean functional synthesis is a fundamental problem in computer science
with wide-ranging applications and has witnessed a surge of interest resulting
in progressively improved techniques over the past decade. Despite intense
algorithmic development, a large number of problems remain beyond the reach of
the state of the art techniques. Motivated by the progress in machine learning,
we propose Manthan, a novel data-driven approach to Boolean functional
synthesis. Manthan views functional synthesis as a classification problem,
relying on advances in constrained sampling for data generation, and advances
in automated reasoning for a novel proof-guided refinement and provable
verification. On an extensive and rigorous evaluation over 609 benchmarks, we
demonstrate that Manthan significantly improves upon the current state of the
art, solving 356 benchmarks in comparison to 280, which is the most solved by a
state of the art technique; thereby, we demonstrate an increase of 76
benchmarks over the current state of the art. Furthermore, Manthan solves 60
benchmarks that none of the current state of the art techniques could solve.
The significant performance improvements, along with our detailed analysis,
highlights several interesting avenues of future work at the intersection of
machine learning, constrained sampling, and automated reasoning.

Manthan 是一种基于数据驱动的方法，将布尔函数综合视为分类问题，依赖于约束采样和自动推理等技术，通过对 609 个基准测试案例的评估，证明了其在现有技术上的显著改进，解决了当前技术不能解决的 60 个基准测试案例。

基于数据驱动的布尔函数合成方法 Manthan

Manthan: A Data Driven Approach for Boolean Function Synthesis

Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a
vector of inputs, the Boolean functional synthesis problem requires us to
compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever
\exists X F(X,Y) holds. In this paper, we investigate the relation between the
representation of the specification F(X,Y) and the complexity of synthesis. We
introduce a new normal form for Boolean formulas, called SynNNF, that
guarantees polynomial-time synthesis and also polynomial-time existential
quantification for some order of quantification of variables. We show that
several normal forms studied in the knowledge compilation literature are
subsumed by SynNNF, although SynNNFcan be super-polynomially more succinct than
them. Motivated by these results, we propose an algorithm to convert a
specification in CNF to SynNNF, with the intent of solving the Boolean
functional synthesis problem. Experiments with a prototype implementation show
that this approach solves several benchmarks beyond the reach of
state-of-the-art tools.

研究 Boolean functional synthesis 问题中 CNF 转化为 SynNNF 的算法，并证明 SynNNF 具有多项式时间综合的优势。

布尔函数综合的知识编译

Knowledge Compilation for Boolean Functional Synthesis

Given a relational specification between Boolean inputs and outputs, the goal
of Boolean functional synthesis is to synthesize each output as a function of
the inputs such that the specification is met. In this paper, we first show
that unless some hard conjectures in complexity theory are falsified, Boolean
functional synthesis must necessarily generate exponential-sized Skolem
functions, thereby requiring exponential time, in the worst-case. Given this
inherent hardness, what does one do to solve the problem? We present a
two-phase algorithm for Boolean functional synthesis, where the first phase is
efficient both in terms of time and sizes of synthesized functions, and solves
an overwhelming majority of benchmarks. To explain this surprisingly good
performance, we provide a sufficient condition under which the first phase must
produce exact correct answers. When this condition fails, the second phase
builds upon the result of the first phase, possibly requiring exponential time
and generating exponential-sized functions in the worst-case. Detailed
experimental evaluation shows our algorithm to perform better than
state-of-the-art techniques for a majority of benchmarks.

通过两阶段算法求解 Boolean functional synthesis，在满足一定条件下的第一阶段可提供正确答案，若不满足条件则第二阶段需通过指数级时间生成指数大小的函数，实验表明算法比现有技术更优秀。