solver3: Store clauses as the reasons for decisions

So far we only stored the last reason why something was decided,
for example, if "A depends B | C" and we assigned B=false, C=false,
we'd store "(not) C" as the reason for "(not) A".

This gives us only a partial implication graph; after all "C" was
not the *sole* reason for not installing A. This has two implications:

1. We cannot do conflict-driven clause learning
2. We cannot print excellent information about why packages cannot be
   installed (or removed)

This commit is incomplete in addressing both; in particular, we always
store a clause as a reason for something that is not a root object;
whereas MiniSAT would only store a clause on propagation. That is,
if A depends B | C, and we install A, then we have to make a choice
between B|C. Let's say we pick B, we store 'A depends B|C' as the
reason whereas MiniSAT would not store a reason (because it picked
the "next best" unassigned literal).

Hopefully this is not going to be an issue. The reason is used to
calculate the assignments that caused the decision in MiniSAT, but
the idea is that we can just treat reason clauses with unassigned
values as "no reason".

The conflict explanation (WhyStr) has been changed to print the
strongest reason; which produces the same result as the previous
solution for the test suite. What does this mean?

If we look at A depends B|C, let's analyse:

    Why not A?
        We return the first assigned value for B|C, likely B.
        We might have returned C here before as it was the
        last assignment, but we might also return C here,
        if B is not assigned.

    Why B? We return A.

If we look at A conflicts B:

    Why not A? Well B
    Why not B? Well A

Thanks to the structure of the implication graph this is quite
simple, but also generalizing this to the CNF format should not
be hard.

A future version will extend clauses with backlinks to
pkgCache::Dependency*, allowing us to print useful information
to uses such as "A Depends B | C | D (>= 2)" in the real form, rather
than the expanded form which may be "A -> B | C | D=3 | D=2".

0 files changed, 0 insertions, 0 deletions