Prototype for SAT-based dependency handling. This is a work in progress,
do not expect any API not to change at this point.
Installation
============
To install the python package, simple do as follows::
git clone --recursive https://github.com/enthought/sat-solver
cd sat-solver
pip install -e .
Example usage
=============
TODO
Usage from the CLI
==================
To try things out from the CLI, you need to write a scenario file (yaml
format), see simplesat/tests/simple_numpy.yaml for a simple example.
To print the rules::
python scripts/print_rules.py simplesat/tests/simple_numpy.yaml
To print the operations::
python scripts/solve.py simplesat/tests/simple_numpy.yaml
Comparing with php's composer
=============================
First, clone composer's somewhere on your machine::
git clone https://github.com/composer/composer
Then, use the `scripts/scenario_to_php.py` script to write a php file that will
print the composer's solution for a given scenario::
python scripts/scenario_to_php.py \
--composer-root <path to composer github checkout> \
simplesat/tests/simple_numpy.yaml \
scripts/print_operations.php.in
This will create a `scripts/print_operations.php` script you can simply execute w/
php::
php scripts/print_operations.php
Bibliography
============
- Niklas Eén, Niklas Sörensson: `An Extensible SAT-solver
<http://minisat.se/downloads/MiniSat.pdf>`_. SAT 2003
- Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik:
`Efficient Conflict Driven Learning in a Boolean Satisfiability Solver
<https://www.princeton.edu/~chaff/publication/iccad2001_final.pdf>`_.
Proc. ICCAD 2001, pp. 279-285.
- Donald Knuth: `The art of computer programming
<http://www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz>`_. Vol. 4,
Pre-fascicle 6A, Par. 7.2.2.2. (Satisfiability).
On the use of SAT solvers for managing packages:
- Fosdem 2008 presentation: `Using SAT for solving package dependencies
<https://files.opensuse.org/opensuse/en/b/b9/Fosdem2008-solver.pdf>`_. More
details on the `SUSE wiki
<https://en.opensuse.org/openSUSE:Libzypp_satsolver>`_.
- The `0install project <http://0install.net>`_.
- Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner: `OPIUM: Optimal
Package Install/Uninstall Manager
<https://cseweb.ucsd.edu/~lerner/papers/opium.pdf>`_. Proc. ICSE 2007,
pp. 178-188
``simplesat`` CHANGELOG
=======================
Version 0.9.1
-------------
* Fix the simplesat wheel build (#287)
Version 0.9.0
-------------
* Replace travis CI with Github Actions (#281)
* Run tests for Python 3.11 (#284)
Version 0.8.2
-------------
Released on October 8th, 2019.
* Fix deprecated ``convert`` attribute in ``constraint_modifiers.py`` to
comply with attrs package release 19.2.0 (see also
`<https://www.attrs.org/en/stable/changelog.html>`_). (#270)
* Fix typo in ``InvalidConstraint`` error message. (#266)
* Fix error with ``UndeterminedClausePolicy`` not suggesting best packages. (#268)
Internals
~~~~~~~~~
* Change minimum supported version of attrs to 17.4.0. (#270)
Version 0.8.1
-------------
Released on March 22nd, 2017.
Bug fixes
~~~~~~~~~
* fix edge case in upgrade-all, when no remote candidate is available for an
already installed package (#261)
* fix parsing of requirements that start with a digit (#260)
Version 0.8.0
-------------
Released on March 9th, 2017.
Features
~~~~~~~~
* new upgrade job kind, to update every installed package to the latest (#253)
* new solver method solve_with_hint for a more human-readable message for
unsatisfiable problems (#254)
Internals
~~~~~~~~~
* update runtime dependencies constraints to latest okonomiyaki (#252)
Version 0.7.0
-------------
Released on August 8th, 2016.
Features
~~~~~~~~
* Add function to compute the leaf packages in a set of repositories.
Version 0.6.0
-------------
Released on July 20th, 2016.
Features
~~~~~~~~
* Add support for post-release version number (#239)
* Add package and package id iteration to Pool (#237)
Version 0.5.0
-------------
Released on July 12th, 2016.
Features
~~~~~~~~~
* Return error message text when checking for satisfiability/completeness of
requirements (#231)
* Add `remove` method to ConstraintModifiers that deletes constraints
associated with a particular package (#229)
Version 0.4.0
-------------
Released on 1st June 2016.
Features
~~~~~~~~~
* `ConstraintModifiers` enhancements: Add `update` method; use validator for
modifiers on `Request` (#211)
* Add function to compute some minimal unsatisfiable subsets of a set of
clauses (#219)
* Add `soft-update` job to `Request`. For a soft-update, the policy prefers to
suggest newer versions rather than the installed version. (#220)
Bug fixes
~~~~~~~~~
* Track clauses with only one literal in solver to avoid crash in policy (#209)
* Avoid failure in policy if an installed package has no associated clauses
(#218)
Version 0.3.0
-------------
Released on 5th May 2016.
Features
~~~~~~~~~
* add support for `provides` metadata (#194)
* add new api for simplifying and satisfying requests (#195)
Enhancements
------------
* update `install_requires` to allow `okonomiyaki >= 0.14` (#197)
* Request now uses `attrs` (#196)
* update internal documentation for the various Requirement types (#201)
Bug fixes
~~~~~~~~~
* fix `Repository.add_package` when `Repository.find_packages` was previously
used for non existing packages (#185)
* fix error handling when metadata conflict (#187)
* fix package name parsing in requirement (#193)
* call to `asdict` must be deterministic (#200)
Version 0.2.2
-------------
Released on 29/04/2016.
* update `install_requires` to allow `okonomiyaki >= 0.14` (#198)
Version 0.2.1
-------------
Released on 27/04/2016.
* fix `Repository.add_package` when `Repository.find_packages` was previously
used for non existing packages (#185)
* fix error handling when metadata conflict (#187)
Version 0.2.0
-------------
Enhancements
~~~~~~~~~~~~
* Details relating to unsatisfiable scenarios are captured in an ``UNSAT``
object and attached to the ``SatisifiabilityError`` raised (#101).
* satsolver does not depend on enstaller anymore, and only uses non-Enthought
libraries besides okonomiyaki (#127, #114, #113, #111, #110, #109, #107.
#105)
* support ad-hoc relaxing of dependency requirements (#140)
* added documentation
* handle the case where a package metadata contains reference to non existing
requirements. Those are now by default ignored instead of just crashing the
solver (#156)
* added __version__ and __git_revision__ attributes to satsolver (#173)
Bugs Fixed
~~~~~~~~~~
* ``IPolicy`` constructor now ignores initialization arguments (#101).
* Some sort operations that were using non-unique keys have been fixed (#101).
* Assumptions are now represented as an empty Clause object (#101).
* be stricted about distribution name and version parsing (#146)
* cleanup setup, added missing enum34 as a dependency in setup.py (#169, #170)
Internals
~~~~~~~~~
* internal API to check consistency of a set of requirements (#157)
* fix debug output in scripts/solve.py (#159)
* add utility script to export a scenario into DIMACS format (#162)
* internal API to compute reverse dependencies of a requirement (#175)
Version 0.1.0
~~~~~~~~~~~~~
The initial release of ``simplesat``. While the SAT solver is fully functional,
the infrastructure for building a set of clauses to be solved supports runtime
dependencies specified using only equality constraints, such as ``numpy 1.8.0-1
depends MKL ^= 10.3``.
Features
~~~~~~~~
* Provides a pure python implementation of MiniSAT, supporting directed search
via plugin-style ``Policy`` objects.
* Reads and solves yaml-based scenario descriptions. These may optionally
specify the following:
* available packages
* currently installed packages
* "marked" packages which must be present in a valid solution
* any number of requested package-oriented operations
* installation
* removal
* update
* update-all
* the expected solution as a list of such package operations
* a failure message for scenarios which are expected to be unresolvable.
* Keeps detailed information about the progression of value assignments and
assumptions made throughout the search process.
* Make some effort to prune irrelevant truth values from solutions, i.e. find
the minimal set of values needed to solve a problem.
Raw data
{
"_id": null,
"home_page": "https://github.com/enthought/sat-solver",
"name": "simplesat",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.6",
"maintainer_email": null,
"keywords": null,
"author": "Enthought Inc.",
"author_email": "info@enthought.com",
"download_url": "https://files.pythonhosted.org/packages/a7/03/7ea01cc6ff66345d9926ee4198050401e46608c5cffacba9aea3fa62b076/simplesat-0.9.1.tar.gz",
"platform": null,
"description": "Prototype for SAT-based dependency handling. This is a work in progress,\ndo not expect any API not to change at this point.\n\nInstallation\n============\n\nTo install the python package, simple do as follows::\n\n git clone --recursive https://github.com/enthought/sat-solver\n cd sat-solver\n pip install -e .\n\nExample usage\n=============\n\nTODO\n\nUsage from the CLI\n==================\n\nTo try things out from the CLI, you need to write a scenario file (yaml\nformat), see simplesat/tests/simple_numpy.yaml for a simple example.\n\nTo print the rules::\n\n python scripts/print_rules.py simplesat/tests/simple_numpy.yaml\n\nTo print the operations::\n\n python scripts/solve.py simplesat/tests/simple_numpy.yaml\n\n\nComparing with php's composer\n=============================\n\nFirst, clone composer's somewhere on your machine::\n\n git clone https://github.com/composer/composer\n\nThen, use the `scripts/scenario_to_php.py` script to write a php file that will\nprint the composer's solution for a given scenario::\n\n python scripts/scenario_to_php.py \\\n --composer-root <path to composer github checkout> \\\n simplesat/tests/simple_numpy.yaml \\\n scripts/print_operations.php.in\n\nThis will create a `scripts/print_operations.php` script you can simply execute w/\nphp::\n\n php scripts/print_operations.php\n\nBibliography\n============\n\n- Niklas E\u00e9n, Niklas S\u00f6rensson: `An Extensible SAT-solver\n <http://minisat.se/downloads/MiniSat.pdf>`_. SAT 2003\n- Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik:\n `Efficient Conflict Driven Learning in a Boolean Satisfiability Solver\n <https://www.princeton.edu/~chaff/publication/iccad2001_final.pdf>`_.\n Proc. ICCAD 2001, pp. 279-285.\n- Donald Knuth: `The art of computer programming\n <http://www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz>`_. Vol. 4,\n Pre-fascicle 6A, Par. 7.2.2.2. (Satisfiability).\n\nOn the use of SAT solvers for managing packages:\n\n- Fosdem 2008 presentation: `Using SAT for solving package dependencies\n <https://files.opensuse.org/opensuse/en/b/b9/Fosdem2008-solver.pdf>`_. More\n details on the `SUSE wiki\n <https://en.opensuse.org/openSUSE:Libzypp_satsolver>`_.\n- The `0install project <http://0install.net>`_.\n- Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner: `OPIUM: Optimal\n Package Install/Uninstall Manager\n <https://cseweb.ucsd.edu/~lerner/papers/opium.pdf>`_. Proc. ICSE 2007,\n pp. 178-188\n\n``simplesat`` CHANGELOG\n=======================\n\nVersion 0.9.1\n-------------\n\n* Fix the simplesat wheel build (#287)\n\nVersion 0.9.0\n-------------\n\n* Replace travis CI with Github Actions (#281)\n* Run tests for Python 3.11 (#284)\n\nVersion 0.8.2\n-------------\n\nReleased on October 8th, 2019.\n\n* Fix deprecated ``convert`` attribute in ``constraint_modifiers.py`` to\n comply with attrs package release 19.2.0 (see also\n `<https://www.attrs.org/en/stable/changelog.html>`_). (#270)\n* Fix typo in ``InvalidConstraint`` error message. (#266)\n* Fix error with ``UndeterminedClausePolicy`` not suggesting best packages. (#268)\n\nInternals\n~~~~~~~~~\n\n* Change minimum supported version of attrs to 17.4.0. (#270)\n\n\nVersion 0.8.1\n-------------\n\nReleased on March 22nd, 2017.\n\nBug fixes\n~~~~~~~~~\n\n* fix edge case in upgrade-all, when no remote candidate is available for an\n already installed package (#261)\n* fix parsing of requirements that start with a digit (#260)\n\nVersion 0.8.0\n-------------\n\nReleased on March 9th, 2017.\n\nFeatures\n~~~~~~~~\n\n* new upgrade job kind, to update every installed package to the latest (#253)\n* new solver method solve_with_hint for a more human-readable message for\n unsatisfiable problems (#254)\n\nInternals\n~~~~~~~~~\n\n* update runtime dependencies constraints to latest okonomiyaki (#252)\n\n\nVersion 0.7.0\n-------------\n\nReleased on August 8th, 2016.\n\nFeatures\n~~~~~~~~\n\n* Add function to compute the leaf packages in a set of repositories.\n\nVersion 0.6.0\n-------------\n\nReleased on July 20th, 2016.\n\nFeatures\n~~~~~~~~\n\n* Add support for post-release version number (#239)\n* Add package and package id iteration to Pool (#237)\n\nVersion 0.5.0\n-------------\n\nReleased on July 12th, 2016.\n\nFeatures\n~~~~~~~~~\n\n* Return error message text when checking for satisfiability/completeness of\n requirements (#231)\n* Add `remove` method to ConstraintModifiers that deletes constraints\n associated with a particular package (#229)\n\nVersion 0.4.0\n-------------\n\nReleased on 1st June 2016.\n\nFeatures\n~~~~~~~~~\n\n* `ConstraintModifiers` enhancements: Add `update` method; use validator for\n modifiers on `Request` (#211)\n* Add function to compute some minimal unsatisfiable subsets of a set of\n clauses (#219)\n* Add `soft-update` job to `Request`. For a soft-update, the policy prefers to\n suggest newer versions rather than the installed version. (#220)\n\nBug fixes\n~~~~~~~~~\n\n* Track clauses with only one literal in solver to avoid crash in policy (#209)\n* Avoid failure in policy if an installed package has no associated clauses\n (#218)\n\nVersion 0.3.0\n-------------\n\nReleased on 5th May 2016.\n\nFeatures\n~~~~~~~~~\n\n* add support for `provides` metadata (#194)\n* add new api for simplifying and satisfying requests (#195)\n\nEnhancements\n------------\n\n* update `install_requires` to allow `okonomiyaki >= 0.14` (#197)\n* Request now uses `attrs` (#196)\n* update internal documentation for the various Requirement types (#201)\n\nBug fixes\n~~~~~~~~~\n\n* fix `Repository.add_package` when `Repository.find_packages` was previously\n used for non existing packages (#185)\n* fix error handling when metadata conflict (#187)\n* fix package name parsing in requirement (#193)\n* call to `asdict` must be deterministic (#200)\n\nVersion 0.2.2\n-------------\n\nReleased on 29/04/2016.\n\n* update `install_requires` to allow `okonomiyaki >= 0.14` (#198)\n\nVersion 0.2.1\n-------------\n\nReleased on 27/04/2016.\n\n* fix `Repository.add_package` when `Repository.find_packages` was previously\n used for non existing packages (#185)\n* fix error handling when metadata conflict (#187)\n\nVersion 0.2.0\n-------------\n\nEnhancements\n~~~~~~~~~~~~\n\n* Details relating to unsatisfiable scenarios are captured in an ``UNSAT``\n object and attached to the ``SatisifiabilityError`` raised (#101).\n* satsolver does not depend on enstaller anymore, and only uses non-Enthought\n libraries besides okonomiyaki (#127, #114, #113, #111, #110, #109, #107.\n #105)\n* support ad-hoc relaxing of dependency requirements (#140)\n* added documentation\n* handle the case where a package metadata contains reference to non existing\n requirements. Those are now by default ignored instead of just crashing the\n solver (#156)\n* added __version__ and __git_revision__ attributes to satsolver (#173)\n\nBugs Fixed\n~~~~~~~~~~\n\n* ``IPolicy`` constructor now ignores initialization arguments (#101).\n* Some sort operations that were using non-unique keys have been fixed (#101).\n* Assumptions are now represented as an empty Clause object (#101).\n* be stricted about distribution name and version parsing (#146)\n* cleanup setup, added missing enum34 as a dependency in setup.py (#169, #170)\n\nInternals\n~~~~~~~~~\n\n* internal API to check consistency of a set of requirements (#157)\n* fix debug output in scripts/solve.py (#159)\n* add utility script to export a scenario into DIMACS format (#162)\n* internal API to compute reverse dependencies of a requirement (#175)\n\nVersion 0.1.0\n~~~~~~~~~~~~~\n\nThe initial release of ``simplesat``. While the SAT solver is fully functional,\nthe infrastructure for building a set of clauses to be solved supports runtime\ndependencies specified using only equality constraints, such as ``numpy 1.8.0-1\ndepends MKL ^= 10.3``.\n\nFeatures\n~~~~~~~~\n\n* Provides a pure python implementation of MiniSAT, supporting directed search\n via plugin-style ``Policy`` objects.\n* Reads and solves yaml-based scenario descriptions. These may optionally\n specify the following:\n\n * available packages\n * currently installed packages\n * \"marked\" packages which must be present in a valid solution\n * any number of requested package-oriented operations\n\n * installation\n * removal\n * update\n * update-all\n\n * the expected solution as a list of such package operations\n * a failure message for scenarios which are expected to be unresolvable.\n\n* Keeps detailed information about the progression of value assignments and\n assumptions made throughout the search process.\n* Make some effort to prune irrelevant truth values from solutions, i.e. find\n the minimal set of values needed to solve a problem.\n",
"bugtrack_url": null,
"license": "BSD-3-Clause",
"summary": "Prototype for SAT-based dependency handling. This is a work in progress, do not expect any API not to change at this point.",
"version": "0.9.1",
"project_urls": {
"Homepage": "https://github.com/enthought/sat-solver"
},
"split_keywords": [],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "76d01dd0d4adb376ad1076331e9f5f38641fd58890d134f8050ab00160836988",
"md5": "17eb1bd6ff4839c4a19ac7c8a007987d",
"sha256": "4f7d7a121ba13db987ea635205db8897d7d01220962e8a9c8cfd41b9886e6b8a"
},
"downloads": -1,
"filename": "simplesat-0.9.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "17eb1bd6ff4839c4a19ac7c8a007987d",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.6",
"size": 249486,
"upload_time": "2024-09-09T15:58:40",
"upload_time_iso_8601": "2024-09-09T15:58:40.880979Z",
"url": "https://files.pythonhosted.org/packages/76/d0/1dd0d4adb376ad1076331e9f5f38641fd58890d134f8050ab00160836988/simplesat-0.9.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "a7037ea01cc6ff66345d9926ee4198050401e46608c5cffacba9aea3fa62b076",
"md5": "a558ea95e27572441a281a8e1085a45b",
"sha256": "990115b1bb32a76c30b2416f645e99e61360382c795203e25ab59b26cd173749"
},
"downloads": -1,
"filename": "simplesat-0.9.1.tar.gz",
"has_sig": false,
"md5_digest": "a558ea95e27572441a281a8e1085a45b",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.6",
"size": 224986,
"upload_time": "2024-09-09T15:58:42",
"upload_time_iso_8601": "2024-09-09T15:58:42.756788Z",
"url": "https://files.pythonhosted.org/packages/a7/03/7ea01cc6ff66345d9926ee4198050401e46608c5cffacba9aea3fa62b076/simplesat-0.9.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-09-09 15:58:42",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "enthought",
"github_project": "sat-solver",
"travis_ci": false,
"coveralls": true,
"github_actions": true,
"lcname": "simplesat"
}
JSON
