Symbolic Approaches for Boolean Synthesis

Boolean synthesis is the problem defined as the procedure to construct solutions for unknown variables in a given specification in Boolean formula as a conjunction of constraints describing the relationship over known and unknown variables. Formally, the problem consists of two parts, the identification of full, partial, and nullary realizability for the input domain, and the construction of the functions for the unknown variables. As a fundamental problem with applications in circuit design, formal verification, and temporal logic synthesis, in the last few decades there have been algorithmic solutions in relevant works using mainly search-based and also symbolic approaches, especially those using Binary Decision Diagrams (BDDs), an acyclic directed graph that maps the solutions for a boolean formula to its paths. Scalability challenges also rose as exponential memory blowups occurred in handling large-scale problems using BDDs, but it also becomes one of the most interested measurement that values the potential to solve larger problems for industrial purposes. Zero-suppressed Decision Diagrams (ZDDs) offer more compact representations for sparse and large-size conjunctive normal form (CNF) formulas, which decomposes input formulas into factored components that are represented by tree decompositions, with improved performance in realizability checking and witness function synthesis construction. Dynamic programming(DP) framework, which also shows capability and potential in model counting works, improves the operations such as existential quantifications and conjunctions by utilizing graded project-join trees. This dissertation introduces approaches that take ZDDs and dynamic programming to address these limitations and add solvers to the portfolio of promising industrial synthesis tools. Three algorithms are proposed as symbolic approaches for boolean synthesis, with their corresponding tools ZSynth, DPSynth, and DPZynth. The first approach is monolithic ZDD-based, shows better performance in compilation and realizability checking, but has a tie dependent on benchmark families with BDD-based tool. The second approach taking BDDs and DP shows a general better performance over non-DP tool and machine learning-based tool even if taking DP overhead into consideration. The third approach has better general picture in time performance, overcomes the planning overhead, and has a scalability potential on some benchmarks. By empirical evaluations, we show the existence of unique features for the proposed approaches, and evaluate their strengths as necessary additions to the portfolio of industrial solvers. The crux of the portfolio does not rely on a particular always best solver, but is proved to be in need of future works that adjusts the selection based on characteristics of a problem.

Name thesis:degree_name

Doctor of Philosophy

Level thesis:degree_level

Doctoral

Discipline thesis:degree_discipline

Engineering

Grantor

Rice University

Year dc:date.issued

2025

Author dc:creator

• Lin, Yi

Advisor dc:contributor.advisor

• Vardi, Moshe

• Boolean synthesis
• Binary decision diagram
• Zero-suppressed binary decision diagram
• Quantifier elimination
• Resolution
• Dynamic programming
• Bucket elimination
• Exploration-exploitation

Statement dc:rights

• Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder.

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1911/118622

OAI identifier oai:identifier

oai:repository.rice.edu:1911/118622