cnfgen.formula.cnfio module¶

CNF formula with read/write capabilities

class CNFio(clauses=None, description=None)¶

Bases: cnfgen.formula.basecnf.BaseCNF

CNF class with I/O capabilities

read and write DIMACS
write to LaTeX format
communicate with SAT solver

Examples

>>> c=CNFio([[1, 2, -3], [-2, 4]])
>>> print( c.to_dimacs(),end='')
p cnf 4 2
1 2 -3 0
-2 4 0

Methods

`add_clause`(clause[, check])	Add a clause to the CNF.
`add_clauses_from`(clauses[, check])	Add a sequence of clauses to the CNF
`all_variable_labels`([default_label_format])	Produces the labels of all the variables
`clauses`()	Return the list of clauses
`debug`([allow_opposite, allow_repetition])	Check if the formula representation is correct
`from_file`([fileorname])	Reads a DIMACS file into a CNF object
`is_satisfiable`([cmd, sameas])	Determines if the formula is satisfiable of not
`solve`([cmd, sameas, verbose])	Solve the formula with a SAT solver
`to_dimacs`()	Produce the dimacs encoding of the formula
`to_file`([fileorname, fileformat, …])	Save the formula to a file
`to_latex`()	Output a LaTeX version of the CNF formula
`update_variable_number`(new_value)	Raises the number of variable in the formula to new_value
`variables`()	Return the list of variables

number_of_clauses
number_of_variables

classmethod from_file(fileorname=None)¶

Reads a DIMACS file into a CNF object

Parameters:	cnfclass: subclass of cnfgen.basecnf.BaseCNF the type of CNF object to produce fileorname: file object or string (or stdin if None) destination file given either as object or as filename

is_satisfiable(cmd=None, sameas=None)¶

Determines if the formula is satisfiable of not

This method is just a simpler interface to the :py:method:`solve` method.

The formula is passed to a SAT solver, and the method returns True if the solvers claims the formula to be satisfiable, and false otherwise. If there is no solver available the method raises RuntimeError.

For a better description about the (optional) arguments to pass, see the documentation of :py:method:`solve` method.

>>> F.is_satifiable(cmd='minisat-style-solver',sameas='minisat')  # doctest: +SKIP
>>> F.is_satifiable(cmd='dimacs-style-solver',sameas='lingeling') # doctest: +SKIP

Parameters:	cmd : string,optional the actual command line used to invoke the SAT solver sameas : string, optional use the interface of one of the supported solvers. Useful when the solver used in the command line is not supported.
Returns:	boolean True when F is satisfiable, or False otherwise.
Raises:	RuntimeError if it is not possible to correctly invoke the solver needed. ValueError if sameas is set and is not the name of a supported solver.

See also

solve: run a SAT solver on this formula
cnfgen.utils.solver.sat_solve: implementation independent of CNF object.
cnfgen.utils.solver.supported_satsolvers: the SAT solver recognized by cnfgen.

Examples

>>> F.is_satisfiable()                                              # doctest: +SKIP
>>> F.is_satisfiable(cmd='minisat -no-pre')                         # doctest: +SKIP
>>> F.is_satisfiable(cmd='glucose -pre')                            # doctest: +SKIP
>>> F.is_satisfiable(cmd='lingeling --plain')                       # doctest: +SKIP
>>> F.is_satisfiable(cmd='sat4j')                                   # doctest: +SKIP
>>> F.is_satisfiable(cmd='my-hacked-minisat -pre',sameas='minisat') # doctest: +SKIP
>>> F.is_satisfiable(cmd='patched-lingeling',sameas='lingeling')    # doctest: +SKIP

solve(cmd=None, sameas=None, verbose=0)¶

Solve the formula with a SAT solver

The formula is passed to a SAT solver, according to the optional command line cmd. If no command line is specified, the known solvers are tried in succession until one is found.

It is possible to use any drop-in replacement for these solvers, but in this case more information is needed on how to communicate with the solver. In particular minisat does not respect the standard DIMACS I/O conventions, and that holds also for glucose which is a drop-in replacement of minisat.

For the supported solver we can pick the right interface, but for other solvers it is impossible to guess. Nevertheless it is possible to indicate which interface to use, or more specifically which known solver interface to mimic.

>>> F.solve(cmd='minisat-style-solver',sameas='minisat')  # doctest: +SKIP
>>> F.solve(cmd='dimacs-style-solver',sameas='lingeling') # doctest: +SKIP

Parameters:	cmd : string,optional the actual command line used to invoke the SAT solver sameas : string, optional use the interface of one of the supported solvers. Useful when the solver used in the command line is not supported. verbose: int 0 or less means no output. 1 shows the command line actually run. 2 outputs the solver output. (default: 0)
Returns:	(boolean,assignment or None) A pair (answer,witness) where answer is either True when F is satisfiable, or False otherwise. If F is satisfiable the witness is a satisfiable assignment in form of a dictionary, otherwise it is None.
Raises:	RuntimeError if it is not possible to correctly invoke the solver needed. ValueError if sameas is set and is not the name of a supported solver. TypeError if F is not a CNF object.

See also

cnfgen.utils.solver.sat_solve: implementation independent of CNF object.
cnfgen.utils.solver.supported_satsolvers: the SAT solver recognized by cnfgen.

Examples

>>> F.solve()                                              # doctest: +SKIP
>>> F.solve(cmd='minisat -no-pre')                         # doctest: +SKIP
>>> F.solve(cmd='glucose -pre')                            # doctest: +SKIP
>>> F.solve(cmd='lingeling --plain')                       # doctest: +SKIP
>>> F.solve(cmd='sat4j')                                   # doctest: +SKIP
>>> F.solve(cmd='my-hacked-minisat -pre',sameas='minisat') # doctest: +SKIP
>>> F.solve(cmd='patched-lingeling',sameas='lingeling')    # doctest: +SKIP

to_dimacs()¶

Produce the dimacs encoding of the formula

The formula is rendered in the DIMACS format for CNF formulas, which is a particularly popular input format for SAT solvers [1].

Note

By default the DIMACS output is ascii encoded, with non-ascii characters replaced.

Returns:	string the string contains the Dimacs code

References

[1]	http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps

Examples

>>> c=CNFio([[-1, 2, -3], [-2,-4], [2, 3, -4]])
>>> print(c.to_dimacs(),end='')
p cnf 4 3
-1 2 -3 0
-2 -4 0
2 3 -4 0

>>> c=CNFio()
>>> print(c.to_dimacs(),end='')
p cnf 0 0

to_file(fileorname=None, fileformat=None, export_header=True, export_varnames=False, extra_text='')¶

Save the formula to a file

The formula is saved on file, in either as a DIMACS file, or as a LaTeX document.

If fileformat is either dimacs or tex then the output is saved in the corresponding format.

If fileformat is None, then DIMACS format is the default output format unless the file name ends with ‘.tex’.

Parameters:

fileorname: file name or file object: where to print the file (default: <stdout>)
fileformat: ‘tex’, ‘dimacs’ or None: format of the output file
export_header: bool: print some additional information on the output file (default: True)
export_varnames: bool: add the variable ID –> name information in the dimacs (default: True)
extra_text: str: additional text to be included in the LaTeX output document

to_latex()¶

Output a LaTeX version of the CNF formula

The CNF formula is translated into the LaTeX markup language [1], using the names of the variable literally. The formula is rendered in the align environment, with one clause per row. Negated literals are rendered using the \neg command.

The output string is ready to be included in a document, but it does not include neither a preamble nor is nested inside \begin{document} … \end{document}.

Note

By default the LaTeX document in output is UTF-8 encoded.

Returns:	string the string contains the LaTeX code

References

[1]	http://www.latex-project.org/

Examples

>>> c=CNFio([[-1, 2, -3], [-2, -4], [2, 3, -4]])
>>> print(c.to_latex())
\begin{align}
&       \left( {\overline{x}_1} \lor            {x_2} \lor {\overline{x}_3} \right) \\
& \land \left( {\overline{x}_2} \lor {\overline{x}_4} \right) \\
& \land \left(            {x_2} \lor            {x_3} \lor {\overline{x}_4} \right)
\end{align}
>>> c=CNFio()
>>> print(c.to_latex())
\begin{align}
   \top
\end{align}

guess_output_format(fileorname, fileformat_request)¶

Try to guess the appropriate file format

If fileformat is either dimacs or tex then the output is saved in the corresponding format.

If fileformat is None, then DIMACS format is the default output format unless the file name ends with ‘.tex’.