- Here are a (somewhat elaborate) set of slides describing the SAT problem: The SAT problem and SAT solvers. The slides describe resolution, chronological and non-chronological backtrack based search.
- 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.

- 02/03: Preliminary concepts of primality, minimality, irredundancy and minimum cardinality of two level covers: Here are the slides. slides updated 2/18.
- And here are some scanned notes on primality and irredundancy and circuit testability.
- 02/05: CUDD + SAT Demo by Xiaojun
- 02/08: The recursive approach to prime implicant generation. Slides slides updated 2/18.
- 02/10: 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.
- 2/12, 2/17: Finished Chapter 4 in the textbook.

- Here are the slides that we covered in class.

- 2/26: Algebraic expression, factored forms and Weak Division. Here are the slides on the algebraic model and the factored form representations.
- 2/29: 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.

- 3/7: Simple disjunctive decomposition, to Ashenhurst/Curtis, to Bi-decomposition. Here are the slides on Ashenhurst/Curtis type decomp.
- 3/9: 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 .
- 3/21: The theories of Boolean function decomposition, AND decomp on K-maps, and how to solve it on BDDs.
- 3/23: Studied AND and OR bi- decompositions on BDDs.
- 3/25: Finished the BDS paper, studied MUX and XNOR decomp.

- Here is a set of powerpoint slides from a former UMass student that describes contruction and functional reduction of AIGs (called FRAIGing).
- 3/30: Will study Mishchenko and Steinbach's model of bi-decomposition, and then study how to model it using a SAT problem.
- 4/1: Here are some slides, borrowed from Prof. Roland Jiang, on Bi-decomposition using AIGs and SAT solvers.

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

- Here is the HW 5 assignment, due next Monday, April 11.
- In Q5, you will need to experiment with this file: hw5.eqn.
- These are some larger designs: C7552.blif and the optimized netlist C7552_fixed_opt.blif. The HW question asks you to experiment with these files.
- HW 5 solutions for the first 3 problems 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.