Lesson 3

Let \(O_{i,u,v}\) denote the operation bit of gate \(i\) on local inputs \((u,v)\), and let \(V_{i,x}\) denote the value of gate \(i\) on global input assignment \(x\). Once \(S_{i,a,b}\) is true, the implication \[V_{i,x}=O_{i,V_{a,x},V_{b,x}}\] must hold for every \(x\). Each possible triple of local values yields a small collection of clauses. Values of input sources are constants, and the value of the last gate is fixed to \(f(x)\).

This separation is central to many SAT encodings: selector variables describe a combinatorial object, while auxiliary variables certify that the selected object behaves correctly.