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 number of gates \(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 kinds of information:

  1. the two predecessors of every gate;
  2. the four-bit operation of every gate;
  3. the value of every gate on every global 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.