{ "info": { "author": "F\u00c1BI\u00c1N Tam\u00e1s L\u00e1szl\u00f3", "author_email": "giganetom@gmail.com", "bugtrack_url": null, "classifiers": [ "Development Status :: 5 - Production/Stable", "Environment :: Plugins", "Intended Audience :: Developers", "Intended Audience :: Science/Research", "License :: OSI Approved :: BSD License", "Operating System :: OS Independent", "Programming Language :: Python", "Topic :: Scientific/Engineering :: Mathematics", "Topic :: Software Development :: Libraries" ], "description": "SATisPy\n=======\n\nSatispy is a Python library that aims to be an interface to various\nSAT (boolean satisfiability) solver applications.\n\nSupported solvers:\n\n * [MiniSAT](http://minisat.se/) (Linux)\n * [Lingeling](http://fmv.jku.at/lingeling/) (Linux, Cygwin)\n\nSupport for other solvers should be fairly easy as long as they accept the\n[DIMACS CNF SAT format](http://www.satcompetition.org/2009/format-benchmarks2009.html).\n\nInstalling\n----------\n\nYou can grab the current version from pypi:\n\n $ sudo pip install satispy\n\nOr you can download a copy from https://github.com/netom/satispy, and\nruns\n\n $ sudo ./setup.py install\n\nin the directory of the project.\n\nIf you want to develop on the library, use:\n\n\t$ ./setup.py develop\n\nYou can run the tests found in the test folder by running run_tests.py.\n\nHow it works\n------------\n\nYou need a SAT solver and numpy to be installed on your machine for this to work.\n\nLet's see an example:\n\n from satispy import Variable, Cnf\n from satispy.solver import Minisat\n \n v1 = Variable('v1')\n v2 = Variable('v2')\n v3 = Variable('v3')\n \n exp = v1 & v2 | v3\n \n solver = Minisat()\n \n solution = solver.solve(exp)\n \n if solution.success:\n print \"Found a solution:\"\n print v1, solution[v1]\n print v2, solution[v2]\n print v3, solution[v3]\n else:\n print \"The expression cannot be satisfied\"\n\nThis program tries to satisfy the boolean expression\n\nv1 & v2 | v3\n\nYou can make this true by assigning true to all variables for example,\nbut there are other solutions too. This program finds a single arbitrary\nsolution.\n\nFirst, the program imports the various classes so we can build an expression\nand try to solve it.\n\nEvery expression is in CNF form, but we don't have to enter the expression\nin it. The Cnf class takes care of the proper arranging of the boolean\nterms.\n\nExpressions can be built by creating variables and gluing them together\narbitrarily with boolean operators:\n\n* NOT: - (unary)\n* AND: &\n* OR: |\n* XOR: ^\n* IMPLICATION >>\n\nThe solver class Minisat is used to solve the formula.\n\nNote: the Minisat class creates two temporary files, so it needs write\naccess to the system's temporary directory\n\nThe returned solution can be checked by reading the \"success\" boolean\nflag.\n\nThen, the solution can be queried for variable assignments by using it\nlike a dictionary. Note that Variable objects are used, not strings.\n\n(This very example can be found in the examples directory)\n", "description_content_type": null, "docs_url": null, "download_url": "https://github.com/netom/satispy/tarball/1.0a5#egg=satispy-1.0a5", "downloads": { "last_day": -1, "last_month": -1, "last_week": -1 }, "home_page": "https://github.com/netom/satispy/", "keywords": null, "license": "BSD License", "maintainer": null, "maintainer_email": null, "name": "satispy", "package_url": "https://pypi.org/project/satispy/", "platform": "OS Independent", "project_url": "https://pypi.org/project/satispy/", "project_urls": { "Download": "https://github.com/netom/satispy/tarball/1.0a5#egg=satispy-1.0a5", "Homepage": "https://github.com/netom/satispy/" }, "release_url": "https://pypi.org/project/satispy/1.0/", "requires_dist": null, "requires_python": null, "summary": "An interface to SAT solver tools (like minisat)", "version": "1.0" }, "last_serial": 4179347, "releases": { "1.0": [ { "comment_text": "", "digests": { "md5": "079895f49ae81d76e2ff07e536e9c78a", "sha256": "ada198d95ea9fdaf4f827cbd17c9d0556b46abcfa56bc93cc4bf60fc3eba7b11" }, "downloads": -1, "filename": "satispy-1.0.tar.gz", "has_sig": false, "md5_digest": "079895f49ae81d76e2ff07e536e9c78a", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 8024, "upload_time": "2015-04-25T15:04:18", "url": "https://files.pythonhosted.org/packages/30/72/0b5920cb28f282ca6ad143bde1cd2dd90a6845ab1a78c8c8c0b4add02a06/satispy-1.0.tar.gz" } ], "1.0a1": [], "1.0a2": [], "1.0a3": [], "1.0a4": [ { "comment_text": "", "digests": { "md5": "a959d1bd4a3414b6c9ad3401138fe02a", "sha256": "284634fc52d40b1b1684e045afbdddc2a24922f74284f2beae0016f373b5f9f9" }, "downloads": -1, "filename": "satispy-1.0a4.tar.gz", "has_sig": false, "md5_digest": "a959d1bd4a3414b6c9ad3401138fe02a", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 9442, "upload_time": "2013-06-04T08:46:57", "url": "https://files.pythonhosted.org/packages/ed/e1/11182a76331ff2b83528febc76cb67414f85395bb51a920cad04bdaa2d9e/satispy-1.0a4.tar.gz" } ], "1.0a5": [ { "comment_text": "", "digests": { "md5": "358fe907753daa6bd5096151691c98aa", "sha256": "6a2bcbc612c9b65692465f90783e5901e20dab696072a2c86de4385b8337db15" }, "downloads": -1, "filename": "satispy-1.0a5.tar.gz", "has_sig": false, "md5_digest": "358fe907753daa6bd5096151691c98aa", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 8019, "upload_time": "2015-04-25T14:47:18", "url": "https://files.pythonhosted.org/packages/15/78/d404afd2a4764694aa07995a85a5c2bbc49e9398a22ee09093a360144b6a/satispy-1.0a5.tar.gz" } ], "1.1b1": [ { "comment_text": "", "digests": { "md5": "24385c3989120492ab7daaae47779521", "sha256": "925d97de02df3f8d566e5f1b3bfff7657c45d8550f9c5b0dff81d0916cb5e107" }, "downloads": -1, "filename": "satispy-1.1b1-py3-none-any.whl", "has_sig": false, "md5_digest": "24385c3989120492ab7daaae47779521", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 7313, "upload_time": "2018-08-17T08:31:03", "url": "https://files.pythonhosted.org/packages/32/9e/b58169e374bc7436f7b2c99cf54f858f006e11429f264aa69fb7dc5822a8/satispy-1.1b1-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "b628466a604620349a1efe2b759985a0", "sha256": "73a2d6f9f36b9cd243ff75bd56d4b0b222797cdb838dd162c45a6bd3360dc996" }, "downloads": -1, "filename": "satispy-1.1b1.tar.gz", "has_sig": false, "md5_digest": "b628466a604620349a1efe2b759985a0", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 6461, "upload_time": "2018-08-17T08:31:04", "url": "https://files.pythonhosted.org/packages/fd/70/7787b397ab13c4f7a9bd01ee7604ff31dca6850d617e53d217026e0dd09b/satispy-1.1b1.tar.gz" } ] }, "urls": [ { "comment_text": "", "digests": { "md5": "079895f49ae81d76e2ff07e536e9c78a", "sha256": "ada198d95ea9fdaf4f827cbd17c9d0556b46abcfa56bc93cc4bf60fc3eba7b11" }, "downloads": -1, "filename": "satispy-1.0.tar.gz", "has_sig": false, "md5_digest": "079895f49ae81d76e2ff07e536e9c78a", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 8024, "upload_time": "2015-04-25T15:04:18", "url": "https://files.pythonhosted.org/packages/30/72/0b5920cb28f282ca6ad143bde1cd2dd90a6845ab1a78c8c8c0b4add02a06/satispy-1.0.tar.gz" } ] }