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

Lesson 2

Nikolai Chukhin · Alexander S. Kulikov

Let \(S_{i,a,b}\) mean that gate \(i\) uses predecessors \(a\) and \(b\). For each gate, at least one legal pair must be selected: \[\bigvee_{0\le a,b<n+i}S_{i,a,b}.\] At most one pair is selected by adding \[\lnot S_{i,a,b}\lor\lnot S_{i,c,d}\] for every two distinct pairs. Together these clauses express “exactly one.”

Ordered predecessor pairs are convenient. If all operations are available, swapping the predecessors can be compensated by transposing the operation table, so one may later impose \(a\le b\) as a symmetry-breaking constraint.

Problem. Gate 2 in a two-input circuit may choose any ordered pair of earlier sources. Gate 3 may do the same. How many variables of the form \(S_{i,a,b}\) are needed for these two gates in total?

5 points