- BDD basics ,
- BDD composition from circuits: ITE and the symbol table implementation ,
- Concluding BDDs .
- As an example application of how to synthesize circuits using BDDs, here is a paper on Synthesis with Pass Transistor Logic. To get a basic idea, just browse through Sections 1, 2 and 3.

- Here are a (somewhat elaborate) set of slides describing the SAT problem: The SAT problem and SAT solvers. slides updated Feb 1. The slides describe resolution, chronological and non-chronological backtrack based search, UNSAT cores, and Craig Interpolants.
- Solving The Boolean Satisfiability Problem. Here is the technical report on GRASP -- Generic Search for Satisfiability that describes SAT solvers, conflict-analysis and non-chronological backtracking.

- 01/30: Preliminary concepts of primality, minimality, irredundancy and minimum cardinality of two level covers: Here are the slides. slides updated Feb 1.
- 01/30: And here are some scanned notes on primality and irredundancy and circuit testability.
- 02/03: The recursive approach to prime implicant generation. Slides slides updated Feb 1.
- 02/05 - 02/13: Formulating the Table Covering Problem: First, let us review the theoretical concepts, then we will build the branch and bound algorithm. Here are the slides that we used to show examples of row and column covering: Row and Column covering examples.
- Also, here are the slides (courtesy Prof. Chris Myers) on the UCP and BCP formulations and solving the covering table using branch-and-bound.
- 02/13: Finished Chapter 4 in the textbook.
- 2/15, 2/18, 2/20: Heuristic minimization of two-level covers: Espresso
(Chapter 5)
- Here are the slides that we covered in class. The study of Espresso's approach.

- Simple disjunctive decomposition, to Ashenhurst/Curtis, to Bi-decomposition. Here are the slides on Ashenhurst/Curtis type decomp.
- We will finish Ashenhurst/Curtis type decomposition, and move on to Bi-decomposition. Here are some slides on Bi-decomposition and how to do it on BDDs .
- Also, attached is the paper that describes all these results: BDS: BDD-based Bi-decomp .
- The theories of Boolean function decomposition, AND decomp on K-maps, and how to solve it on BDDs.
- Studied AND and OR bi- decompositions on BDDs.
- 03/04: Finished the BDS paper, studied MUX and XNOR decomp.

- 03/04: Algebraic expression, factored forms and Weak Division. Here are the slides on the algebraic model and the factored form representations.
- 03/04: Kernels, co-Kernels and their computation. And here are the slides on algebraic division and kernel set theory.
- 3/2: Introduced the Rectangle Covering Problem
- 3/4: Complete the algebraic model: Common Subexpression Extraction, identifying common cubes from multiple expressions, and identifying common subkernels. Also covered resubstitution.

- Here is a set of powerpoint slides from a former UMass student that describes contruction and functional reduction of AIGs (called FRAIGing).

- Here are the slides: Partial Synthesis

- Here is the PDF file for the DIET paper, by Yang and Ciesielski.

- Timing analysis
- And here are some slides that consolidate these concept on PPT: timing.ppt.

- Download the BDD package from github: https://github.com/ivmai/cudd , or better yet, download the GZIPPED tarball from here.
- You will also need this main.c file.

- Question 1 solutions on prime computation.
- Question 2 solutions on on the UCP table covering.
- Question 3 solutions on Tautology Checking.
- Question 4 solutions on Two level heuristics (containment, expand, essential) .
- For questions 6 & 7: Solutions for Simple Disjunctive decomp and Ashenhurst-Curtis Decomp related questions are available from here.

- Here is the HW 5 assignment, due next Wednesday, April 24.
- These are some BLIF files designs: C7552.blif The HW question asks you to experiment with these files.
- HW 5 solutions are here.

- Here is the picoSAT website from where you can download and compile the source code. MAC OS users can find one through MacPorts.
- Here is the Lingeling website
- Here is the zchaff website from where you can download and compile the source code.
- Here is a linux binary that I use zchaff on the CADE machines.
- Here is a sample CNF file in the DIMACS CNF format that these SAT solvers can take as input.
- Here is a blif2cnf perl script. Feel free to use it.

- exam_table_cover.lp .
- Another lp example which is infeasible.