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.

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. SAT 2003

• Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. Proc. ICCAD 2001, pp. 279-285.

• Donald Knuth: The art of computer programming. 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. More details on the SUSE wiki.

• The 0install project.

• Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner: OPIUM: Optimal Package Install/Uninstall Manager. 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.