## cnfgen-nand-opt

This program can generate CNF (Conjunctive Normal Form) to check possibility to build
circuit built on NAND or NOR gates that returns given values from table.

WARNING: For some greater examples this program can generates CNF that can excess
1 gigabyte.

This program can read problem from file. If no given file then program read problem
from standard input. The format of input is in TOML format:

```
gate = "Nand"
layers = 5
max_gates = 18
table = [ 6, 62, 11, 17, 26, 47, 53, 35 ]
```

The `gate` field is gate type - it can be `Nand` or `Nor`. The `layers` defines number
of layers (steps) of calcuation in circuit. The `max_gates` defines maximal number of
gates. The `table` is table of values that should be returned by circuit.

List of commands:

* generate - Generate CNF file and print it to standard output.
* execute - Generate CNF file and pass it to SAT solver, check and print results. The `SAT_SOLVER` environment variable must be set to path to SAT solver executable.
* check - Check and print results from SAT output. The SAT output file given as the second argument after command or the first FILE is not given.
* help - Print help.

Sample output:

```
Number of gates for layers: [8, 11, 12, 6, 12, 6]
Layer 1:
  (0, 0) 0
  (0, 0) 0
  (0, 2) 2
  (0, 2) 2
....
Output:
  (6, 1) 167
  (6, 2) 168
  (6, 0) 166
  (5, 7) 159
```

It returns structure of circuit. In the layer listing are gate inputs where the first number
in parentheses is number of layer (0 - index input) and number of output.