Author: kkaempf
Date: Tue May 13 18:10:56 2008
New Revision: 10079
URL: http://svn.opensuse.org/viewcvs/zypp?rev=10079&view=rev
Log:
In the beginning, there was nothing.
On the first weekend, an initial documentation was created.
Added:
trunk/sat-solver/doc/SOLVER
Added: trunk/sat-solver/doc/SOLVER
URL: http://svn.opensuse.org/viewcvs/zypp/trunk/sat-solver/doc/SOLVER?rev=10079&view=auto
==============================================================================
--- trunk/sat-solver/doc/SOLVER (added)
+++ trunk/sat-solver/doc/SOLVER Tue May 13 18:10:56 2008
@@ -0,0 +1,209 @@
+How the sat-solver works
+------------------------
+
+I. Data structure
+-----------------
+ Id p; /* first literal in rule */
+ Id d; /* Id offset into 'list of providers */
+ /* terminated by 0' as used by whatprovides; pool->whatprovides + d */
+ /* in case of binary rules, d == 0, w1 == p, w2 == other literal */
+ /* in case of disabled rules: ~d, aka -d - 1 */
+ Id w1, w2; /* watches, literals not-yet-decided */
+ /* if !w2, assertion, not rule */
+ Id n1, n2; /* next rules in linked list, corresponding to w1,w2 */
+
+
+ r->n1 = solv->watches[nsolvables + r->w1];
+ solv->watches[nsolvables + r->w1] = r - solv->rules;
+
+ r->n2 = solv->watches[nsolvables + r->w2];
+ solv->watches[nsolvables + r->w2] = r - solv->rules;
+
+
+ * Assertion
+ * keepinstalled (A), install
+ p=A, d=0, w1=p, w2=0
+ * uninstallable (-A), remove
+ p=-A, d=0, w1=p, w2=0
+ *
+ * Binary rules:
+ * (A|B)
+ p=A, d=0, w1=p, w2=B
+ * (-A|B)
+ p=-A, d=0, w1=p, w2=B
+ *
+ * A requires B : !A | provider1(B) | provider2(B)
+ p=-A, d=, w1=, w2=
+
+ * B updates A : A | provider1(B) | provider2(B)
+ p=A, d=, w1=, w2=
+
+ *
+ * A conflicts B : (!A | !provider1(B)) & (!A | !provider2(B)) ...
+ p=-A, d=-B1, w1=, w2=
+ p=-A, d=-B2, w1=, w2=
+ p=-A, d=-B3, w1=, w2=
+ ...
+ *
+ * 'not' is encoded as a negative Id
+ *
+
+Action | p | d | w1 | w2
+--------------+----+---------+-------+--------
+Assert A | A | 0 | A | 0
+Assert -A |-A | 0 |-A | 0
+Binary A,B | A | 0 | A | B
+Binary -A,B |-A | 0 |-A | B
+A requires B |-A | prov(B) |-A | whatprovidesdata(B)
+B updates A | A | prov(B) | A | whatprovidesdata(B)
+A conflicts B |-A | -B |-A |-B
+
+
+addrule(p, d)
+
+
+/*
+* add rule
+* p = direct literal; always < 0 for installed rpm rules
+* d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
+*
+*
+* A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
+*
+* p < 0 : pkg id of A
+* d > 0 : Offset in whatprovidesdata (list of providers of b)
+*
+* A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
+* p < 0 : pkg id of A
+* d < 0 : Id of solvable (e.g. B1)
+*
+* d == 0: unary rule, assertion => (A) or (-A)
+*
+* Install: p > 0, d = 0 (A) user requested install
+* Remove: p < 0, d = 0 (-A) user requested remove
+* Requires: p < 0, d > 0 (-A|B1|B2|...) d: <list of providers for requirement of p>
+* Updates: p > 0, d > 0 (A|B1|B2|...) d: <list of updates for solvable p>
+* Conflicts: p < 0, d < 0 (-A|-B1),(-A|-B2),... either p (conflict issuer) or d (conflict provider) (binary rule)
+* Obsoletes: p < 0, d < 0 (-A|-B1),(-A|-B2),... A: uninstalled, Bx = provider of obsoletes
+* ? p > 0, d < 0 (A|-B)
+* No-op: p = 0, d = 0 (null) (used as policy rule placeholder)
+* install one of: p =-SYS, d > 0
+*
+* resulting watches:
+* ------------------
+* Direct assertion (no watch needed)( if d <0 ) --> d = 0, w1 = p, w2 = 0
+* Binary rule: p = first literal, d = 0, w2 = second literal, w1 = p
+* every other : w1 = p, w2 = whatprovidesdata[d];
+* Disabled rule: d < 0, w1 = 0
+*
+* always returns a rule for non-rpm rules
+*/
+
+enablerule:
+ if (d < 0): d = -d - 1
+disablerule
+ if (d >= 0): d = -d - 1
+
+
+Watches
+-------
+
+Watches 'link' rules involving the same literal
+Only for n-ary (n >= 2) rules, not for assertions
+
+
+Watches start at solv->watches[nsolvables]
+
+watches[nsolvables+s] == rule installing s
+watches[nsolvables-s] == rule removing s
+
+'watches trigger when literal goes false'
+
+watches[A] = rule involving A
+ rule->n1 = next rule involving A
+watches[B] = rule involving B
+ rule->n2 = next rule involving B
+
+
+Propagation
+-----------
+
+This distributes decisions among affected rules and checks that rules
+evaluate to 'true'.
+
+Since rules are in CNF (conjunctive normal form), it is sufficient for
+one sub-term (x or y in x|y) to become 'true'.
+
+The interesting case is a 'false' sub-term (x or y in x|y) because
+this requires the 'other' side to become true.
+
+
+
+II. Algorithm
+-------------
+
+- set up rules for installed packages
+if (installed)
+ foreach(installed): addrpmrulesforsolvable
+ convert dependencies of solvable into rules
+ run through the complete graph of dependencies spawned the solvable
+ foreach(installed): addrpmrulesforupdaters
+ add rules to allow updates: A | upates(A)
+
+- set up rules for solvables mentioned in job
+ foreach (install request)
+ addrpmrulesforsolvable
+ foreach (update request)
+ addrpmrulesforupdaters
+ /* dont look at removals */
+
+- addrpmrulesforweak
+ if suggests: add dependency rule
+ else if freshens: add dependency rule
+ else if enhances: add dependency rule
+
+- add feature rules
+
+- add update rules
+
+- add job rules
+
+During solving, we only look at those rules affected by the job or a
+decision. By use of the linked-list rooted at 'watches', the solver is
+able to wade through all the rules and pick the right ones.
+
+And only those have to evaluate to 'true' during propagation.
+
+Actual solving works as follows
+-------------------------------
+
+- ensure the SYSTEM solvable gets installed
+- look through the job rules for 'unit' rules
+ (i.e. rules directly installing/removing a solvable)
+
+- These two define the 'initial decisions' which now get propagated
+- propagation either results in other decisions (i.e. one sub-term
+ false requires the other one to become true) or 'free' literals
+ (which are decided by policy heuristics)
+
+- The solver has a 'decisionq' which record decisions (> 0 for
+ 'install', < 0 for 'remove')
+ Every decision has an 'index' (== position in decisionq)
+ There are two 'pointers'
+ - decisionq.count == total number of made decision
+ - propagate_index == number of already propagated decisions
+
+ Decisions are also recorded in decisionmap, indexed by the solvable
+ Id. This is a fast access to decisions (instead of searching in the
+ queue)
+
+ And there is 'decisionq_why', indexed by the decision number (level)
+ returning the rule leading to the decision.
+
+ propagate() now tries to advance propagate_index to decisionq.count
+ in order to propagate all decisions to all (affected) rules.
+ propagate() also ensures that decisions are consistent (else its a
+ solver conflict) and all affected rules evaluate to 'true'.
+
+ When rules are reduced to 'unit' (only one undecided literal, all
+ others 'false'), the last literal must be decided to 'true'.
--
To unsubscribe, e-mail: zypp-commit+unsubscribe@opensuse.org
For additional commands, e-mail: zypp-commit+help@opensuse.org
