On August 20-22, 2012 CTIC organized and hosted a three-day workshop on Boolean Satisfiability.  When using the term "workshop" in academia, this usually refers to a small conference with lots of talks and lectures.

This workshop was however different, as it was a combination of lectures presented by the invited leading reaserchers, and group work where participants provided open problems to be discussed in small groups of 4, and presented in plenum.

With three invited speakers and 12 participants from several places, the workshop was comparably small in size, which created a stimulating atmosphere and was very well suited to doing research in groups.

The small scale of the workshop also provided participants an excellent opportunity to exchange ideas, and especially for PhD students it was a great opportunity to personally meet great scientists and see them at work.

Ramamohan Paturi talked about how certain combinatorial statements about CNF formulas, like Håstad's Switching Lemma or the Satisfiability Coding Lemma, were originally intended to prove circuit lower bounds, but also led to algorithms which for k-CNF formulas significantly improve over exhaustive search. Then he explored more systematic ways of obtaining lower bounds from certain algorithms and extracting algorithms from lower bound proofs.

Rahul Santhanam talked about formally provable connections between algorithms and lower bounds. (1) The classic result that if SAT is in P, then EXP does not have polynomial size circuits; (2) the recent result of Ryan Williams that solving CircuitSAT just a little bit faster than exhaustive search proves strong lower bounds, and how this result can be generalized to more restricted versions of CircuitSAT.

Russell Impagliazzo talked about unconditional lower bounds for resolution, and thus for branching-based SAT-algorithms. In particular about a recent result about tradeoffs between the size of a resolution proof and its space. This explains time/space tradeoffs observed in practice for SAT-solveres using clause learning.

The groups worked on several problems provided by the participants as well as by the speakers. They were related to important open problems in the field, i.e. obtaining explicit strongly exponential lower bounds for depth-3-circuits; derandomizing the PPSZ algorithm; improving over exhaustive search for more general circuit classes than ACC_0.