.. include:: ../shared/references.rst
.. include:: ../shared/formulas-substitutions.rst


.. _WCNF-formula:

WCNF Formula
============

.. py:module:: optilog.formulas
    :noindex:

.. autoclass:: WCNF(var_manager=None)

.. autoclass:: WCNFException
  :exclude-members: with_traceback

|var-manager-redir|

.. code:: python
  :number-lines:

  >>> from optilog.formulas import WCNF
  >>> wcnf = WCNF()
  >>> wcnf.extend_vars(2)
  >>> wcnf.max_var()
  2
  >>> wcnf.new_var()
  3
  >>> wcnf.max_var()
  3
  >>> wcnf.add_clause([1,2,3])
  >>> wcnf.add_clauses([[1],[2],[3]], 1)
  >>> wcnf.num_clauses()
  4
  >>> wcnf.soft_clauses
  [(1, [1]), (1, [2]), (1, [3])]
  >>> wcnf.hard_clauses
  [1,2,3]
  >>> wcnf.sum_soft_weights()
  3
  >>> wcnf.top_weight()
  4
  >>> wcnf.add_comment('a simple WCNF test formula')
  >>> wcnf.header()
  ['a simple WCNF test formula']
  >>> wcnf2 = wcnf.copy()
  >>> wcnf2.soft_clauses, wcnf.hard_clauses
  ([(1, [1]), (1, [2]), (1, [3])], [[1, 2, 3]])
  >>> wcnf2 = WCNF()
  >>> wcnf2.max_var()
  0
  >>> wcnf2.soft_clauses, wcnf2.hard_clauses
  ([], [])


Methods sumary
---------------

.. list-table::
    :widths: 60 300
    :header-rows: 1

    * - Return type
      - Methods
    * - int
      - :py:meth:`WCNF.new_var`
    * - int
      - :py:meth:`WCNF.max_var`
    * - list(str)
      - :py:meth:`WCNF.header`
    * - int
      - :py:meth:`WCNF.num_clauses`
    * - int or float
      - :py:meth:`WCNF.top_weight`
    * - None
      - :py:meth:`WCNF.extend_vars`
    * - None
      - :py:meth:`WCNF.set_minimum_vars`
    * - None
      - :py:meth:`WCNF.add_clause`
    * - None
      - :py:meth:`WCNF.add_clauses`
    * - bool or None
      - :py:meth:`WCNF.feasible`
    * - int or float
      - :py:meth:`WCNF.cost`
    * - None
      - :py:meth:`WCNF.add_comment`
    * - None
      - :py:meth:`WCNF.shuffle`
    * - None
      - :py:meth:`WCNF.write_dimacs`
    * - None
      - :py:meth:`WCNF.write_dimacs_file`
    * - WCNF
      - :py:meth:`WCNF.copy`
    * - str
      - :py:meth:`WCNF.__str__`
    * - str
      - :py:meth:`WCNF.__repr__`