cnfformula.cnfgen module

Utilities to build CNF formulas interesting for proof complexity.

The module cnfgen contains facilities to generate cnf formulas, in order to be printed in dimacs or LaTeX formats. Such formulas are ready to be fed to sat solvers. In particular the module implements both a library of CNF generators and a command line utility.

Create the CNFs:

>>> from . import CNF
>>> c=CNF([ [(True,"x1"),(True,"x2"),(False,"x3")],           [(False,"x2"),(True,"x4")] ])
>>> print( c.dimacs(export_header=False) )
p cnf 4 2
1 2 -3 0
-2 4 0

You can add clauses later in the process:

>>> c.add_clause( [(False,"x3"),(True,"x4"),(False,"x5")] )
>>> print( c.dimacs(export_header=False))
p cnf 5 3
1 2 -3 0
-2 4 0
-3 4 -5 0

command_line_utility(argv=['/home/docs/checkouts/readthedocs.org/user_builds/cnfgen/envs/stable/bin/sphinx-build', '-T', '-b', 'readthedocs', '-d', '_build/doctrees-readthedocs', '-D', 'language=en', '.', '_build/html'])

CNFgen main command line interface

This function provide the main interface to CNFgen. It sets up the command line, parses the command line arguments, builds the appropriate formula and outputs its representation.

It must not raise exceptions, but fail with error messages for the user.

Parameters:

argv: list, optional

The list of token with the command line arguments/options.

search_cmdline_input_file(list_args)

Look for input file arguments in the command line

Parameters:

list_args : list of parsed command lines

setup_command_line_args(parser)

Setup general command line options

Arguments: - parser: parser to fill with options

signal_handler(insignal, frame)