{
    "info": {
        "author": "Alexander Feldman",
        "author_email": "alex@llama.gs",
        "bugtrack_url": null,
        "classifiers": [
            "Development Status :: 4 - Beta",
            "Intended Audience :: Developers",
            "Operating System :: OS Independent",
            "Programming Language :: C",
            "Programming Language :: Python :: 2",
            "Programming Language :: Python :: 3",
            "Topic :: Scientific/Engineering :: Artificial Intelligence",
            "Topic :: Utilities"
        ],
        "description": "===========================================\npydepqbf: bindings to DepQBF (a QBF solver)\n===========================================\n\nAuthors:\n--------\n\nA lot of Python binding code and documentation has been lifted from PycoSAT\n<https://pypi.python.org/pypi/pycosat>\n\nDepQBF is owned by Florian Lonsing <http://lonsing.github.io/depqbf/>\n\nThe pydepqbf Python module is distributed under the same terms as DepQBF.\n\nAbstract\n--------\n\n`DepQBF <http://lonsing.github.io/depqbf/>`_ is an efficient\n`QBF <https://en.wikipedia.org/wiki/True_quantified_Boolean_formula>`_ solver\nwritten by Florian Lonsing in pure C.\nThis package provides efficient Python bindings to DepQBF on the C level,\ni.e., when importing pydepqbf, the DepQBF solver becomes part of the\nPython process itself.\n\nUsage\n-----\n\nThe ``pydepqbf`` module has one function: ``solve``.\n\nThe function ``solve`` returns a tuple containing two elements. The\nfirst element is an integer, that is either QDPLL_RESULT_SAT or\nQDPLL_RESULT_UNSAT or QDPLL_RESULT_UNKNOWN. The second element\ncontains a partial certificate for the input problem. If the outermost\n(leftmost) quantifier block of a satisfiable QBF is existentially\nquantified, then the partial certificate is an assignment to the\nvariables of this block (and dual for unsatisfiable QBFs and universal\nvariables from the outermost block, if that block is universally\nquantified). The partial certificate is None if the outermost block of\na satisfiable QBF is universally quantified or if the outermost block\nof an unsatisfiable QBF is existentially quantified.\n\nExample\n-------\n\nLet us consider the following problem, represented by using\nthe QDIMACS `QDIMACS <http://www.qbflib.org/qdimacs.html>`_\nformat::\n\n   p cnf 5 3\n   a 1 2 0\n   e 3 4 0\n   -1 -3 0\n   1 2 4 0\n   1 -4 0\n\nHere, we have 4 variables and 3 clauses, the first clause being\n(not x\\ :sub:`1`  or not x\\ :sub:`3`).\nIn Python, each clause is\nmost conveniently represented as a list of integers.  Naturally, it makes\nsense to represent each solution also as a list of integers, where the sign\ncorresponds to the Boolean value (+ for True and - for False) and the\nabsolute value corresponds to i\\ :sup:`th` variable::\n\n   >>> from pydepqbf import solve, QDPLL_QTYPE_FORALL, QDPLL_QTYPE_EXISTS\n   >>> quantifiers = ((QDPLL_QTYPE_FORALL, (1, 2)), (QDPLL_QTYPE_EXISTS, (3, 4)))\n   >>> clauses = ((-1, -3), (1, 2, 4), (1, -4))\n   >>> solve(quantifiers, clauses)\n   (20, [-1, -2])\n\nThe first element of the resulting pair is 20 (defined as\nQDPLL_RESULT_UNSAT in the pydepqbf package) and the partial\ncertificate translates to: x\\ :sub:`1` = x\\ :sub:`2` = False.",
        "description_content_type": "",
        "docs_url": null,
        "download_url": "",
        "downloads": {
            "last_day": -1,
            "last_month": -1,
            "last_week": -1
        },
        "home_page": "https://github.com/abfeldman/pydepqbf",
        "keywords": "",
        "license": "MIT",
        "maintainer": "",
        "maintainer_email": "",
        "name": "pydepqbf",
        "package_url": "https://pypi.org/project/pydepqbf/",
        "platform": "",
        "project_url": "https://pypi.org/project/pydepqbf/",
        "project_urls": {
            "Homepage": "https://github.com/abfeldman/pydepqbf"
        },
        "release_url": "https://pypi.org/project/pydepqbf/0.0.2/",
        "requires_dist": null,
        "requires_python": "",
        "summary": "bindings to depqbf (a QBF solver)",
        "version": "0.0.2"
    },
    "last_serial": 4022298,
    "releases": {
        "0.0.2": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "aa7c341ed6ccdf6ef8caf78184f235db",
                    "sha256": "7f762764a19db42fbe154216d75eca07953abe29905f4d0b6ff2af8fbf93e802"
                },
                "downloads": -1,
                "filename": "pydepqbf-0.0.2.tar.gz",
                "has_sig": false,
                "md5_digest": "aa7c341ed6ccdf6ef8caf78184f235db",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 325615,
                "upload_time": "2018-07-02T10:04:47",
                "url": "https://files.pythonhosted.org/packages/5b/c6/b56208db66b807eeaa8151a9085955e058a1991b5f43f9f21f0bfaf1a37d/pydepqbf-0.0.2.tar.gz"
            }
        ]
    },
    "urls": [
        {
            "comment_text": "",
            "digests": {
                "md5": "aa7c341ed6ccdf6ef8caf78184f235db",
                "sha256": "7f762764a19db42fbe154216d75eca07953abe29905f4d0b6ff2af8fbf93e802"
            },
            "downloads": -1,
            "filename": "pydepqbf-0.0.2.tar.gz",
            "has_sig": false,
            "md5_digest": "aa7c341ed6ccdf6ef8caf78184f235db",
            "packagetype": "sdist",
            "python_version": "source",
            "requires_python": null,
            "size": 325615,
            "upload_time": "2018-07-02T10:04:47",
            "url": "https://files.pythonhosted.org/packages/5b/c6/b56208db66b807eeaa8151a9085955e058a1991b5f43f9f21f0bfaf1a37d/pydepqbf-0.0.2.tar.gz"
        }
    ]
}