simplesat 0.9.2
Prototype for SAT-based dependency handling. This is a work in progress, do not expect any API not to change at this point.
License: BSD-3-Clause
Requires Python: >=3.8

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.2
-------------

* Support Python 3.12 (#296)
* Provide better error message when cyclic dependencies are detected (#297)
* Sign wheels when uploading to pypi (#298)

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.