.. include:: ../shared/references.rst

Formula Loading utilities
==========================

OptiLog provides three functions to load Boolean formulas, :py:func:`load_cnf`, :py:func:`load_wcnf` and :py:func:`load_qcnf`.

.. automodule:: optilog.formulas.loaders
    :imported-members: 

.. 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`_.

.. [#wcnf] Solvers for weighted (partial) MaxSAT commonly use an extended DIMACS format for CNFs.
    In particular, this format adds weights to each clause and a way to specify hard constraints
    (for partial MaxSAT). This extended format is used and described by `MaxSAT competitions requirements`_.

.. [#qcnf] Based on the `QDIMACS standard <http://www.qbflib.org/qdimacs.html>`_