This session addresses new techniques for SAT and extensions thereof.  The first paper proposes a linear time algorithm for generation of compact CNF from circuits.  The second paper proposes techniques for exploiting structure in QBF solvers, including functional definition of variables and non-linear quantifier structures.  The third paper proposes a path-oriented approach for width manipulation in bit-vector verification for accelerated satisfiability checking.