Automated synthesis techniques generate systems—such as functions or circuits—that provably satisfy a formal specification. Traditional synthesis frameworks often adopt an all-or-nothing approach: either the system satisfies all constraints, or synthesis fails. However, in many practical settings, such strict completeness is either infeasible or too costly to achieve, especially in terms of resources like time, memory, or circuit area. This work addresses such scenarios by moving beyond the all-or-nothing paradigm. We propose a novel synthesis framework that distinguishes between hard constraints, which must be strictly satisfied, and soft constraints, which may be relaxed. The goal is to synthesize systems that provably satisfy all hard constraints while achieving a user-defined threshold of satisfiability on the soft constraints. We quantify this relaxation using a satisficing measure, such as accuracy—i.e., the proportion of inputs for which the system satisfies all constraints.Our approach integrates AI-based methods to generate candidate systems and automated reasoning techniques to ensure formal guarantees. Through extensive experiments, we show that our framework significantly reduces synthesis time compared to traditional approaches. Moreover, the synthesized systems (e.g., circuits) tend to be smaller, connecting our method naturally to the domain of approximate circuit synthesis. Unlike existing approximate synthesis techniques, our framework provides formal guarantees on both correctness (for hard constraints) and quality (for soft constraints).

Quantified Boolean Formulas (QBF) extend propositional logic with quantification$\forall,\exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope. Dependency Quantified Boolean Formulas (DQBF) restrict the dependencies of existentially quantified variables. In DQBF, existentially quantified variables have explicit dependencies on a subset of universally quantified variables, called Henkin dependencies. Given a Boolean specification between the set of inputs and outputs, the problem of Henkin synthesis is to synthesize each output variable as a function of its Henkin dependencies such that the specification is met. Henkin synthesis has wide-ranging applications, including verification of partial circuits, controller synthesis, and circuit realizability. This work proposes a data-driven approach for Henkin synthesis called Manthan3. On an extensive evaluation of over 563 instances arising from past DQBF solving competitions, we demonstrate that Manthan3 is competitive with state-of-the-art tools. Furthermore, Manthan3 solves 26 benchmarks that none of the current state-of-the-art techniques could solve.

Abstract Quantified information flow (QIF) has emerged as a rigorous approach to quantitatively measure confidentiality; the information-theoretic underpinning of QIF allows the end-users to link the computed quantities with the computational effort required on the part of the adversary to gain access to desired confidential information. In this work, we focus on the estimation of Shannon entropy for a given program $$\varPi $$ Π . As a first step, we focus on the case wherein a Boolean formula $$\varphi (X,Y)$$ φ ( X , Y ) captures the relationship between inputs X and output Y of $$\varPi $$ Π . Such formulas $$\varphi (X,Y)$$ φ ( X , Y ) have the property that for every valuation to X, there exists exactly one valuation to Y such that $$\varphi $$ φ is satisfied. The existing techniques require $$\mathcal {O}(2^m)$$ O ( 2 m ) model counting queries, where $$m = |Y|$$ m = | Y | . We propose the first efficient algorithmic technique, called $$\mathsf {EntropyEstimation}$$ EntropyEstimation to estimate the Shannon entropy of $$\varphi $$ φ with PAC-style guarantees, i.e., the computed estimate is guaranteed to lie within a $$(1\pm \varepsilon )$$ ( 1 ± ε ) -factor of the ground truth with confidence at least $$1-\delta $$ 1 - δ . Furthermore, $$\mathsf {EntropyEstimation}$$ EntropyEstimation makes only $$\mathcal {O}(\frac{min(m,n)}{\varepsilon ^2})$$ O ( m i n ( m , n ) ε 2 ) counting and sampling queries, where $$m = |Y|$$ m = | Y | , and $$n = |X|$$ n = | X | , thereby achieving a significant reduction in the number of model counting queries. We demonstrate the practical efficiency of our algorithmic framework via a detailed experimental evaluation. Our evaluation demonstrates that the proposed framework scales to the formulas beyond the reach of the previously known approaches.

The problem of uniform sampling is, given a formula F, sample solutions of F uniformly at random from the solution space of F. Uniform sampling is a fundamental problem with widespread applications, including configuration testing, bug synthesis, function synthesis, and many more. State-of-the-art approaches for uniform sampling have a trade-off between scalability and theoretical guarantees. Many state of the art uniform samplers do not provide any theoretical guarantees on the distribution of samples generated, however, empirically they have shown promising results. In such cases, the main challenge is to test whether the distribution according to which samples are generated is indeed uniform or not. Recently, Chakraborty and Meel (2019) designed the first scalable sampling tester, Barbarik, based on a grey-box sampling technique for testing if the distribution, according to which the given sampler is sampling, is close to the uniform or far from uniform. They were able to show that many off-the-self samplers are far from a uniform sampler. The availability of Barbarik increased the test-driven development of samplers. More recently, Golia, Soos, Chakraborty and Meel (2021), designed a uniform like sampler, CMSGen, which was shown to be accepted by Barbarik on all the instances. However, CMSGen does not provide any theoretical analysis of the sampling quality. CMSGen leads us to observe the need for a tester to provide a quantitative answer to determine the quality of underlying samplers instead of merely a qualitative answer of Accept or Reject. Towards this goal, we design a computational hardness-based tester ScalBarbarik that provides a more nuanced analysis of the quality of a sampler. ScalBarbarik allows more expressive measurement of the quality of the underlying samplers. We empirically show that the state-of-the-art sampler, CMSGen is not accepted as a uniform-like sampler by ScalBarbarik. Furthermore, we show that ScalBarbarik can be used to design a sampler that can achieve balance between scalability and uniformity.

Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reasoning to synthesise Boolean functions efficiently. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We implement these improvements in the state-of-the-art framework, called Manthan. The proposed framework is called Manthan2. Manthan2 shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan - an increment of 153 instances over the state-of-the-art. To put this into perspective, Manthan improved on the prior state-of-the-art by only 76 instances.

Given a specification φ(X, Y ) over inputs X and output Y and defined over a background theory T, the problem of program synthesis is to design a program f such that Y = f (X), satisfies the specification φ. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach to program synthesis where in addition to the specification φ, the end-user also specifies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T constrained synthesis. We show that T-constrained synthesis can be reduced to DQF(T),i.e., to the problem of finding a witness of a dependency quantified formula modulo theory. When the underlying theory is the theory of bitvectors, the corresponding DQF problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific program synthesis techniques; thereby positioning DQBF as a core representation language for program synthesis. Our empirical analysis shows that T-constrained synthesis can achieve significantly better performance than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers perform on par with domain-specific synthesis techniques.

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 $$\textsf {Manthan}$$ , a novel data-driven approach to Boolean functional synthesis. $$\textsf {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 $$\textsf {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, $$\textsf {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.