.. include:: ../shared/references.rst .. include:: ../shared/formulas-substitutions.rst .. _CNF-formula: CNF Formula =========== .. py:module:: optilog.formulas :noindex: .. autoclass:: CNF(var_manager=None) .. autoclass:: CNFException :exclude-members: with_traceback |var-manager-redir| .. code:: python :number-lines: >>> from optilog.formulas import CNF >>> cnf = CNF() >>> cnf.extend_vars(2) >>> cnf.max_var() 2 >>> cnf.new_var() 3 >>> cnf.max_var() 3 >>> cnf.add_clause([1,2,3]) >>> cnf.num_clauses() 1 >>> cnf.add_clauses([[-1,-2],[-1,-3],[-2,-3]]) >>> cnf.num_clauses() 4 >>> cnf.clauses [[1,2,3],[-1,-2],[-1,-3],[-2,-3]] >>> cnf.add_comment('a simple test formula') >>> cnf.header() ['a simple test formula'] >>> cnf2 = cnf.copy() >>> cnf2.clauses [[1,2,3],[-1,-2],[-1,-3],[-2,-3]] Methods sumary --------------- .. list-table:: :widths: 60 300 :header-rows: 1 * - Return type - Methods * - int - :py:meth:`CNF.new_var` * - int - :py:meth:`CNF.max_var` * - list(str) - :py:meth:`CNF.header` * - int - :py:meth:`CNF.num_clauses` * - None - :py:meth:`CNF.extend_vars` * - None - :py:meth:`CNF.set_minimum_vars` * - None - :py:meth:`CNF.add_clause` * - None - :py:meth:`CNF.add_clauses` * - bool or None - :py:meth:`CNF.satisfies` * - None - :py:meth:`CNF.add_comment` * - None - :py:meth:`CNF.shuffle` * - None - :py:meth:`CNF.write_dimacs` * - None - :py:meth:`CNF.write_dimacs_file` * - CNF - :py:meth:`CNF.copy` * - Dict - :py:meth:`CNF.statistics` * - str - :py:meth:`CNF.__str__` * - str - :py:meth:`CNF.__repr__` .. rubric:: Footnotes .. [#cnf] SAT solvers commonly use the DIMACS format for CNFs. This format is used by `SAT competitions requirements`_ as originally described in `DIMACS CNF suggested format`_.