Prototype for SAT-based dependency handling. This is a work in progress, do not expect any API not to change at this point.
Verified details
These details have been verified by PyPIProject links
GitHub Statistics
Maintainers
Project description
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.
