Pypb.Pblib - Constants
======================

.. py:module:: pypblib.pblib
   :synopsis: Encoding Pseudo-Boolean Constraints into CNF.


.. _pb-comparator:

Comparators constants
---------------------

Comparator can be less-equal, greater-equal or a combination of both.

.. data:: GEQ
.. data:: LEQ
.. data:: BOTH


.. _pb-config-const:

Configuration constants
-----------------------


.. _pb-encoder-const:

PB Encoder
++++++++++

.. data:: PB_BEST
.. data:: PB_BDD

    Binary Desition Diagrams. BDD-based encodings have  important  advantages,  such  as sharing the  same BDD  for  representing many constraints.
    Requieres additional variables. Exponential.

.. data:: PB_SWC

    Sequential Weight Counter. SWC encoding is a modification of the sequential counter (SEQ) encoding, which translates cardinality constraints into SAT.
    Similar to BDD but useful for incremental encoding.

.. data:: PB_SORTINGNETWORKS

    A  (Boolean)  sorting  network  is  a  circuit  that  receives n Boolean  inputs x1,...,xn, and  permutes  them  to  obtain  the  sorted  outputs y1,...,yn.

.. data:: PB_ADDER

    Linear inequalities can be encoded into CNF in linear time and space,  and uses adders as the  basic  operator.
    Requieres additional varialbes. Polynomial.

.. data:: PB_BINARY_MERGE

    The Binary Merger encoding requires O(n^2 log^2(n) log(w[max])) clauses. If GAC should not be maintained, our encoding requires only O(n log^2(n) log(w[max])).


.. _amk-encoder-const:

AMK Encoder
+++++++++++

.. data:: AMK_BEST
.. data:: AMK_BDD
.. data:: AMK_CARD


.. _amo-encoder-const:

AMO Encoder
+++++++++++

.. data:: AMO_BEST
.. data:: AMO_NESTED
.. data:: AMO_BDD
.. data:: AMO_BIMANDER
.. data:: AMO_COMMANDER
.. data:: AMO_KPRODUCT
.. data:: AMO_BINARY
.. data:: AMO_PAIRWISE


.. _bimander-m-is-const:

BIMANDER M IS
+++++++++++++

.. data:: N_HALF
.. data:: N_SQRT
.. data:: FIXED