How the SAT solver works

Theory

CNF - Conjunktive Normal Form

Boolean expression of the form (x|y) & (-a|b|c) & ... a,b,c,x,y are LITERALS There a positive literals (x,y) and negative literals (-a, -b) Terms in parentheses are CLAUSES

Goal: Make the whole expression TRUE

Useful shortcuts:

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=<whatprovides_offset>, w1=, w2=
 
 B updates A : A | provider1(B) | provider2(B)
   p=A, d=<whatprovides_offset>, 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
   Learnt:     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 are usually on literals that are not FALSE (either TRUE or UNDEF) Execept: If one watch is on a TRUE (set first), the other can be on a FALSE (set later). This is useful on a backtrack.

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 (aka A, B, C,... in CNF clause) watches[nsolvables-s] == rule removing s (aka -A, -B, -C, ... in CNF clause)

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

Iterating over installed

The pool marks the minimum and maximum Id of installed solvables. There might be other (non-installed) solvables in-between.

Algorithm

doxygen