Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

But these are about the least friendly variable names possible, so in practice we maintain a dictionary of mappings between the term number and something more descriptive. Of course you never write these by hand. Instead you use the language of your choice to generate the CNF file. While this sounds like we are right back to where we started (using fragile imperative languages), generating a CNF is simple, compact and forgiving.

Mail: (not shown)

Please type this: