Task
Research ways to optimize encoding of circuit synthesis as SAT.
Current state
Current model is more or less described in "Finding Efficient Circuits Using SAT-Solvers" paper.
Problems
- Maybe it will be possible to reduce variables or constraints.