Dependency Resolution with SAT [Symfony Live 2011 Paris]
4 likes2,220 views
This document discusses using a SAT solver to resolve software dependencies when installing, updating, or removing packages from a system. It explains how dependency rules can be expressed as Boolean logic statements and solved using techniques like unit propagation and backtracking. The libzypper package manager from SUSE uses a SAT solver for dependency resolution as it is fast, reliable, and can provide understandable explanations.
Dependency Resolution with SAT [Symfony Live 2011 Paris]
- 1. Dependency Resolution with a SAT Solver Nils Adermann March 4th 2011
- 2. SAT? Boolean Satisfiability Problem: Can (A|B)&(C|D|(E&(A|D))&E be true? D(isjunctive)NF: (A&B)|(C&D&A)|(B&D)|C C(onjunctive)NF: (A|B)&(C|D|A)&(B|D)&C
- 3. NP? hard problems nondeterministic polynomial time no known algorithm which: - can solve all instances of the problem - does not need to try all combinations SAT is NP-complete (Cook's theorem)
- 4. Package Management Pool Repositories Package Name & Version requires, conflicts, provides
- 5. Dependency Resolution User wants to: - install some packages - update some packages - remove some packages - keep some packages
- 6. Dependency Resolution EDOS Project Workpackage 2 Team. Report on formal management of software dependencies. EDOS Project Deliverable Work Package 2, Deliverable 2, March 2006. http://www.edos- project.org/xwiki/bin/Main/Deliverables.
- 9. Dependency Resolution No solution: APT Portage Poor solution: smart Urpmi
- 10. Dependency Resolution with SAT SUSE's libzypper (Michael Schroeder) Goals: Fast Complete & Reliable Understandable messages & explanations Based on ideas from minisat
- 11. Rule Generation Job Rules: Install A: (A) Remove A: (-A)
- 12. Rule Generation Dependency Rules: A requires B: (-A|B1|B2) A conflicts with B: (-A|-B1), (-A|-B2) C and D provide A: A requires C or D Policy Rules: B1 can be updated to B2: (B1|B2)
- 13. Solving Rules Unit Propagation: (A|B|C), (-C), (-A|C) (-C) C: false (-A|C) A: false (-A: true) (A|B|C) B: true
- 14. Rule Solving Algorithm Unit Propagation Contradiction? Add Rule -X or unsolvable Backtrack to previous assignment Assign undecided variable X (free choice) Repeat until solved
- 15. Free Choices Keep installed packages installed Do not install unecessary packages Pick newest version
- 16. Thank you! and Michael Schr旦der at Novell for his slides http://files.opensuse.org/opensuse/en/b/b9/Fosdem2008-solver.pdf http://www.mancoosi.org/edos/manager/ http://en.opensuse.org/openSUSE:Libzypp_satsolver