Project: Optimal Circuit Synthesis with SAT · A Synthesis Program

Lesson 1

Nikolai Chukhin · Alexander S. Kulikov

We now combine the encoding with a SAT solver. The solver interface is deliberately not prescribed: one may emit DIMACS CNF and run an external solver, use a library, or implement a small solver. What matters is the decoded circuit.

The output format below uses the same consecutive source numbering as the evaluator. Since a checker evaluates the submitted circuit on every input, different satisfying assignments and different optimal circuits are equally valid.

Programming problem. Construct a circuit of at most the given size for a target Boolean function.

Input format. The first line contains \(n\) and \(k\) (\(2\le n\le5\), \(0\le k\le12\)). The second line contains a bit string of length \(2^{n}\), the target truth table.

Output format. First print the number of gates \(m\le k\). Then print \(m\) gate lines, each containing predecessor indices \(a_{i},b_{i}\) and a four-bit operation string. Gate \(i\) has source index \(n+i\), so both predecessors must be smaller than \(n+i\). Finally, print one source index: the circuit output.

Public samples

Public sample 1

Input

2 1
0110

Expected output

1
0 1 0110
2

Public sample 2

Input

3 2
01101001

Expected output