{ "info": { "author": "Po-Wei Wang", "author_email": "poweiw@cs.cmu.edu", "bugtrack_url": null, "classifiers": [ "License :: OSI Approved :: MIT License" ], "description": "# SATNet \u2022 [![PyPi][pypi-image]][pypi] [![colab][colab-image]][colab] [![License][license-image]][license] \n\n[license-image]: https://img.shields.io/badge/License-MIT-yellow.svg\n[license]: LICENSE\n\n[pypi-image]: https://img.shields.io/pypi/v/satnet.svg\n[pypi]: https://pypi.python.org/pypi/satnet\n\n[colab-image]: https://colab.research.google.com/assets/colab-badge.svg\n[colab]: https://colab.research.google.com/\n\n*Bridging deep learning and logical reasoning using a differentiable satisfiability solver.*\n\nThis repository contains the source code to reproduce the experiments in the ICML 2019 paper [SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver](https://icml.cc/Conferences/2019/Schedule?showEvent=3947) by [Po-Wei Wang](https://powei.tw/), [Priya L. Donti](https://priyadonti.com/), [Bryan Wilder](http://teamcore.usc.edu/people/bryanwilder/default.htm), and [J. Zico Kolter](http://zicokolter.com/).\n\n\n## What is SATNet\n\nSATNet is a differentiable (smoothed) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems. This (approximate) solver is based upon a fast coordinate descent approach to solving the semidefinite program (SDP) associated with the MAXSAT problem.\n\n#### How SATNet works\n\nA SATNet layer takes as input the discrete or probabilistic assignments of known MAXSAT variables, and outputs guesses for the assignments of unknown variables via a MAXSAT SDP relaxation with weights *S*. A schematic depicting the forward pass of this layer is shown below. To obtain the backward pass, we analytically differentiate through the SDP relaxation (see the paper for more details).\n\n![Forward pass](https://github.com/locuslab/SATNet/blob/master/images/forward_pass.png)\n\n#### Overview of experiments\n\nWe show that by integrating SATNet into end-to-end learning systems, we can learn the logical structure of challenging problems in a minimally supervised fashion. In particular, we show that we can:\n* Learn the **parity function** using single-bit supervision (a traditionally hard task for deep networks) \n* Learn how to play **9\u00d79 Sudoku (original and permuted)** solely from examples. \n* Solve a **\"visual Sudoku\"** problem that maps images of Sudoku puzzles to their associated logical solutions. (A sample \"visual Sudoku\" input is shown below.)\n\n
\n\n\n\n## Installation\n\n### Via pip\n```bash\npip install satnet\n```\n\n\n### From source\n```bash\ngit clone https://github.com/locuslab/SATNet\ncd SATNet && python setup.py install\n```\n\n#### Package Dependencies\n```\nconda install -c pytorch tqdm\n```\n\n\n### Via Docker image\n```bash\ncd docker\nsh ./build.sh\nsh ./run.sh\n```\n\n## Running experiments\n### Jupyter Notebook and Google Colab\n[Jupyter notebook](https://github.com/locuslab/SATNet/blob/master/notebooks/Learning%20and%20Solving%20Sudoku%20via%20SATNet.ipynb)\nand [Google Colab]()\n\n### Run them manually\n\n#### Getting the datasets\nThe [Sudoku dataset](https://powei.tw/sudoku.zip) and [Parity dataset](https://powei.tw/parity.zip) can be downloaded via\n\n```bash\nwget -cq powei.tw/sudoku.zip && unzip -qq sudoku.zip\nwget -cq powei.tw/parity.zip && unzip -qq parity.zip\n```\n#### Sudoku experiments (original, permuted, and visual)\n```bash\npython exps/sudoku.py\npython exps/sudoku.py --perm\npython exps/sudoku.py --mnist --batchSz=50\n```\n\n#### Parity experiments\n```bash\npython exps/parity.py --seq=20\npython exps/parity.py --seq=40\n```", "description_content_type": "text/markdown", "docs_url": null, "download_url": "", "downloads": { "last_day": -1, "last_month": -1, "last_week": -1 }, "home_page": "https://github.com/locuslab/SATNet", "keywords": "", "license": "", "maintainer": "", "maintainer_email": "", "name": "satnet", "package_url": "https://pypi.org/project/satnet/", "platform": "", "project_url": "https://pypi.org/project/satnet/", "project_urls": { "Homepage": "https://github.com/locuslab/SATNet" }, "release_url": "https://pypi.org/project/satnet/0.1.2/", "requires_dist": null, "requires_python": "", "summary": "Bridging deep learning and logical reasoning using a differentiable satisfiability solver", "version": "0.1.2" }, "last_serial": 5318059, "releases": { "0.1.0": [ { "comment_text": "", "digests": { "md5": "a1e63a490c78741dc7bb88c32cf95bc9", "sha256": "9f4c3054fba8db3a7b005c9e08f7a1b56ec0e71777733812ce9a39c800fe71a7" }, "downloads": -1, "filename": "satnet-0.1.0.tar.gz", "has_sig": false, "md5_digest": "a1e63a490c78741dc7bb88c32cf95bc9", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 8700, "upload_time": "2019-05-25T12:11:24", "url": "https://files.pythonhosted.org/packages/9e/ff/f9a1f44f736c49ea33282f94ee62d2cc2f4d6b83ddce543239fe9f5866dd/satnet-0.1.0.tar.gz" } ], "0.1.1": [ { "comment_text": "", "digests": { "md5": "3ef776138b8874226930c0fce4c498fc", "sha256": "9de8256e703ed84d49a6599982c7cdaa586726ba5d8baa801df9845056f06e59" }, "downloads": -1, "filename": "satnet-0.1.1.tar.gz", "has_sig": false, "md5_digest": "3ef776138b8874226930c0fce4c498fc", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 8764, "upload_time": "2019-05-25T12:18:53", "url": "https://files.pythonhosted.org/packages/69/76/9ff73d02682533192595ac2580584feaeb802135d91f5c240a222c2d6b25/satnet-0.1.1.tar.gz" } ], "0.1.2": [ { "comment_text": "", "digests": { "md5": "84daddf70ff6c9fe5a79a303ccca9388", "sha256": "093606c101d8ee3f4ccc56750cc7841691bfe2d1c89782152eae4008c481397c" }, "downloads": -1, "filename": "satnet-0.1.2.tar.gz", "has_sig": false, "md5_digest": "84daddf70ff6c9fe5a79a303ccca9388", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 9835, "upload_time": "2019-05-26T06:24:08", "url": "https://files.pythonhosted.org/packages/e5/2a/bdd7ae5a6f2890169cf11d2dd1b1b4ade9a226c6e15cf8a489f99c7e8e33/satnet-0.1.2.tar.gz" } ] }, "urls": [ { "comment_text": "", "digests": { "md5": "84daddf70ff6c9fe5a79a303ccca9388", "sha256": "093606c101d8ee3f4ccc56750cc7841691bfe2d1c89782152eae4008c481397c" }, "downloads": -1, "filename": "satnet-0.1.2.tar.gz", "has_sig": false, "md5_digest": "84daddf70ff6c9fe5a79a303ccca9388", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 9835, "upload_time": "2019-05-26T06:24:08", "url": "https://files.pythonhosted.org/packages/e5/2a/bdd7ae5a6f2890169cf11d2dd1b1b4ade9a226c6e15cf8a489f99c7e8e33/satnet-0.1.2.tar.gz" } ] }