Project: Optimal Circuit Synthesis with SAT · Circuits as Satisfying Assignments

Lesson 1

Nikolai Chukhin · Alexander S. Kulikov

Fix a target function \(f\) and a candidate size \(s\). We construct a CNF formula \(F_{f,s}\) that is satisfiable exactly when a circuit with \(s\) gates computes \(f\).

A satisfying assignment must describe three things:

  1. the two predecessors of every gate;
  2. the four-bit operation of every gate;
  3. the value of every gate on every input assignment.
The third family may look redundant, since values follow from structure and operations. Introducing it makes the local meaning of every gate easy to express in CNF.