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

Yes, there is even a debugger! It is meant to be used when the SAT solver informs you that there are no solutions to the problem. It will selectively block out chunks of the CNF file until a solution exists and then reports which section was responsible. This is done by providing reference points in the form of comments to delineate where sections begin and end. Typically there will be two sections that conflict with each other - one will be correct and the other will have a typo. It is also in the library, and is called

Mail: (not shown)

Please type this: