cnfgen.formula.cnf module¶
Build and manipulate CNF formulas
The module `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.
The module implements the CNF object, which is the main entry point to the cnfgen library.
Copyright (C) 2012-2021 Massimo Lauria <lauria.massimo@gmail.com> https://github.com/MassimoLauria/cnfgen.git
-
class
CNF(clauses=None, description=None)¶ Bases:
cnfgen.formula.mapping.CNFMapping,cnfgen.formula.cnfio.CNFio,cnfgen.formula.linear.CNFLinearPropositional formulas in conjunctive normal form.
A CNF formula is a sequence of clauses, which are sequences of literals. Each literal is either a variable or its negation.
Use
add_clauseto add new clauses to CNF. Clauses will be added multiple times in case of multiple insertion of the same clauses.For documentation purpose it is possible use have an additional comment header at the top of the formula, which will be optionally exported to LaTeX or dimacs.
Implementation: for efficiency reason clauses and variable can only be added, and not deleted. Furthermore order matters in the representation.
Examples
>>> c=CNF([[1, 2, -3], [-2, 4]]) >>> print( c.to_dimacs(),end='') p cnf 4 2 1 2 -3 0 -2 4 0 >>> c.add_clause([-3, 4, -5]) >>> print( c.to_dimacs(),end='') p cnf 5 3 1 2 -3 0 -2 4 0 -3 4 -5 0 >>> print(c[1]) [-2, 4]
Methods
add_clause(clause[, check])Add a clause to the CNF. add_clauses_from(clauses[, check])Add a sequence of clauses to the CNF add_linear(lits, op, constant[, check])Add a linear constraint to the formula add_loose_majority(lits[, check])Clauses encoding a “at least half” constraint add_loose_minority(lits[, check])Clauses encoding a “at most half” constraint add_parity(lits, constant[, check])Adds the CNF encoding of a parity constraint add_strict_majority(lits[, check])Clauses encoding a “strict majority” constraint add_strict_minority(lits[, check])Clauses encoding a “at most half” constraint 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 force_complete_mapping(f)Enforce the mapping f to be complete force_functional_mapping(f)Enforce the mapping f to be functional force_injective_mapping(f)Enforce the mapping f to be injective force_nondecreasing_mapping(f)Enforce the mapping f to be non decreasing force_surjective_mapping(f)Enforce the mapping f to be surjective from_file([fileorname])Reads a DIMACS file into a CNF object is_satisfiable([cmd, sameas])Determines if the formula is satisfiable of not new_binary_mapping(n, m[, label])Adds variables for a mapping from n to m encoded in binary new_bipartite_edges(G[, label])Create a new group variables from the edges of a bipartite graph new_block(*ranges[, label])Create a new group of indexed variables new_combinations(n, k[, label])Create a new group of variables indexed by k-subsets of [n] new_combinations_with_replacement(n, k[, label])Create a new group of variables indexed by k-subsets of [n] new_digraph_edges(G[, label, sortby])Create a new group variables from the edges of a bipartite graph new_graph_edges(G[, label])Create a new group variables from the edges of a bipartite graph new_mapping(n, m[, label])Adds variables for a mapping from n to m new_permutations(n[, k, label])Create a new group of variables indexed by k-permutations of [n] new_sparse_mapping(B[, label])Adds variables for a sparse mapping new_variable([label])Create a new variable new_words(n, k[, label])Create a new group of variables indexed by sequences [n]^k 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