def Std.Sat.CNF.dimacs (cnf : CNF Nat) : String

This function turns cnf into a DIMACS String.

Note: This function will add 1 to all literal identifiers by default. This is because 0 is an illegal identifier in the DIMACS format and we can avoid producing invalid DIMACs like this.

Equations

• One or more equations did not get rendered due to their size.

def Std.Sat.CNF.dimacs.go (cnf : CNF Nat) : Std.Sat.CNF.DimacsM✝ String

Equations

• One or more equations did not get rendered due to their size.