Why does sat flag -dump_cnf report more variables than the original logic has?

[benjamin051000]

I'm learning about SAT checkers. Specifically, I am trying to reverse-engineer the original boolean logic formula of the RTL from the SAT checker.

I have a very simple SystemVerilog file:

// benchmarks/custom/simple.sv
module simple (
        input logic a,
        output logic b
);

assign b = ~a;

endmodule

Here's my Yosys script:

# Read and build hierarchy
read -sv benchmarks/custom/simple.sv
hierarchy -top simple

# Interpret design
proc; opt; techmap; opt

show simple

# Run the SAT checker
sat -show-all -all -dump_cnf simple.cnf simple

Here are the outputs of the SAT pass:

Solving problem with 7 variables and 13 clauses..
SAT solving finished - model found:

  Signal Name             Dec       Hex           Bin
  --------------- ----------- --------- -------------
  \a                        0         0             0

Solving problem with 7 variables and 14 clauses..
SAT solving finished - model found:

  Signal Name             Dec       Hex           Bin
  --------------- ----------- --------- -------------
  \a                        1         1             1

The resulting CNF file:

c generated by ezSAT
p cnf 7 13
   1           0
  -2           0
   1           0
   4  -3   5   0
  -5  -4       0
  -5   3       0
   3  -4   6   0
  -6  -3       0
  -6   4       0
   5   6  -7   0
   7  -5       0
   7  -6       0
   7           0

I'm wondering why CNF has 7 variables when my design only had 1 input and 1 output. What are these 7 variables and 13 clauses?

Additionally, how do these 7 variables relate to the input/outputs in the RTL? I'm hoping for an output that essentially says b = ~a, how can I achieve this? Thank you!