`write_cnf` produces unsatisfiable-preserving but not equivalent CNF — primary input disconnected from output when PO is a direct wire from PI

[Gad1001]

write_cnf produces unsatisfiable-preserving but not equivalent CNF — primary input disconnected from output when PO is a direct wire from PI

Summary

write_cnf silently drops the connection between a Primary Input and a Primary Output when the PO is wired directly to the PI (no intervening AND gates). The resulting CNF leaves the PI variable unconstrained, producing a formula with more satisfying assignments than the original.

Minimal Reproducer

# Create trivial CNF: 1 variable, 1 clause (x1 must be true)
mkdir -p /tmp/abc_bug
cat > /tmp/abc_bug/original.cnf << 'EOF'
p cnf 1 1
1 0
EOF

# Round-trip through ABC
abc -c "read_cnf /tmp/abc_bug/original.cnf; strash; write_cnf /tmp/abc_bug/output.cnf"

cat /tmp/abc_bug/output.cnf

Expected output CNF

A CNF equivalent to the original — exactly 1 satisfying assignment.

Actual output CNF

c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 3 2
-3 0
2 0

Variable 2 (output) is forced TRUE, variable 3 (constant node) is forced FALSE, but variable 1 (the original PI) is completely unconstrained — no clause connects it to the output. This gives 2 satisfying assignments instead of 1.

Root Cause

The Tseitin/AIG-to-CNF encoder emits clauses for AND gates, but when a PO is a direct wire from a PI (or its complement) with zero AND gates in between, no equivalence clauses are generated to tie the output variable to the input variable.

Impact

• Model count is not preserved, which breaks any downstream use of write_cnf output for model counting (#SAT), sampling, or any application that depends on the solution space being faithfully represented.
• The bug is silent — no warning is emitted.

Environment

Tested on latest master. The issue is in write_cnf / the CNF package's AIG-to-CNF conversion.