A faster Installed-First policy

simplesat/dependency_solver.py

@@ -52,12 +52,7 @@ def _create_rules(self, request):
             pool.package_id(package)
             for package in pool.what_provides(requirement)
         ]
-        self._policy.add_packages_by_id(requirement_ids)
-
-        # Add installed packages.
-        self._policy.add_packages_by_id(
-            [pool.package_id(package) for package in installed_repository]
-        )
+        self._policy.add_requirements(requirement_ids)
 
         installed_map = collections.OrderedDict()
         for package in installed_repository:

simplesat/sat/assignment_set.py

@@ -0,0 +1,113 @@
+#!/usr/bin/env python
+# -*- coding: utf-8 -*-
+
+
+import six
+
+from collections import OrderedDict
+
+
+class _MISSING(object):
+    pass
+MISSING = _MISSING()
+
+
+class AssignmentSet(object):
+
+    """A collection of literals and their assignments."""
+
+    def __init__(self, assignments=None):
+        # Changelog is a dict of id -> (original value, new value)
+        # FIXME: Verify that we really need ordering here
+        self._data = OrderedDict()
+        self._orig = {}
+        self._cached_changelog = None
+        self._assigned_literals = set()
+        for k, v in (assignments or {}).items():
+            self[k] = v
+
+    def __setitem__(self, key, value):
+        assert key > 0
+
+        prev_value = self.get(key)
+
+        if prev_value is not None:
+            self._assigned_literals.difference_update((key, -key))
+
+        if value is not None:
+            self._assigned_literals.add(key if value else -key)
+
+        self._update_diff(key, value)
+        self._data[key] = value
+
+    def __delitem__(self, key):
+        self._update_diff(key, MISSING)
+        prev = self._data.pop(key)
+        if prev is not None:
+            self._assigned_literals.difference_update((key, -key))
+
+    def __getitem__(self, key):
+        return self._data[key]
+
+    def get(self, key, default=None):
+        return self._data.get(key, default)
+
+    def __len__(self):
+        return len(self._data)
+
+    def __contains__(self, key):
+        return key in self._data
+
+    def items(self):
+        return list(self._data.items())
+
+    def iteritems(self):
+        return six.iteritems(self._data)
+
+    def keys(self):
+        return list(self._data.keys())
+
+    def values(self):
+        return list(self._data.values())
+
+    def _update_diff(self, key, value):
+        prev = self._data.get(key, MISSING)
+        self._orig.setdefault(key, prev)
+        # If a value changes, dump the cached changelog
+        self._cached_changelog = None
+
+    def get_changelog(self):
+        if self._cached_changelog is None:
+            self._cached_changelog = {
+                key: (old, new)
+                for key, old in six.iteritems(self._orig)
+                for new in [self._data.get(key, MISSING)]
+                if new != old
+            }
+        return self._cached_changelog
+
+    def consume_changelog(self):
+        old = self.get_changelog()
+        self._orig = {}
+        self._cached_changelog = {}
+        return old
+
+    def copy(self):
+        new = AssignmentSet()
+        new._data = self._data.copy()
+        new._orig = self._orig.copy()
+        new._assigned_literals = self._assigned_literals.copy()
+        return new
+
+    def value(self, lit):
+        """ Return the value of literal in terms of the positive. """
+        if lit in self._assigned_literals:
+            return True
+        elif -lit in self._assigned_literals:
+            return False
+        else:
+            return None
+
+    @property
+    def num_assigned(self):
+        return len(self._assigned_literals)

simplesat/sat/clause.py

@@ -2,8 +2,6 @@
 
 from collections import OrderedDict
 
-from .utils import value
-
 
 class Constraint(object):
     pass
@@ -13,6 +11,7 @@ class Clause(Constraint):
 
     def __init__(self, lits, learned=False):
         self.learned = learned
+        # This maintains the ordering while removing duplicate values
         self.lits = list(OrderedDict.fromkeys(lits).keys())
 
     def rewatch(self, assignments, lit):
@@ -41,15 +40,15 @@ def rewatch(self, assignments, lit):
         if lits[0] == -lit:
             lits[0], lits[1] = lits[1], -lit
 
-        if value(lits[0], assignments) is True:
+        if assignments.value(lits[0]) is True:
             # This clause has been satisfied, add it back to the watch list. No
             # unit information can be deduced.
             return None
 
         # Look for another literal to watch, and switch it with lit[1] to keep
         # the assumption on the watched literals in place.
         for n, other in enumerate(lits[2:]):
-            if value(other, assignments) is not False:
+            if assignments.value(other) is not False:
                 # Found a new literal that could serve as a watch.
                 lits[1], lits[n + 2] = other, -lit
                 return None

simplesat/sat/minisat.py

@@ -8,9 +8,9 @@
 
 from six.moves import range
 
+from .assignment_set import AssignmentSet
 from .clause import Clause
 from .policy import DefaultPolicy
-from .utils import value
 
 
 class MiniSATSolver(object):
@@ -41,7 +41,7 @@ def __init__(self, policy=None):
         self.clauses = []
         self.watches = defaultdict(list)
 
-        self.assignments = OrderedDict()
+        self.assignments = AssignmentSet()
 
         # A list of literals which become successively true (because of direct
         # assignment, or by unit propagation).
@@ -64,7 +64,6 @@ def __init__(self, policy=None):
         # Whether the system is satisfiable.
         self.status = None
 
-        #
         self._policy = policy or DefaultPolicy()
 
     def add_clause(self, clause):
@@ -116,7 +115,7 @@ def propagate(self):
                 if unit is not None:
                     # TODO Refactor this to take into account the return value
                     # of enqueue().
-                    if value(unit, self.assignments) is False:
+                    if self.assignments.value(unit) is False:
                         # Conflict. Clear the queue and re-insert the remaining
                         # unwatched clauses into the watch list.
                         self.prop_queue.clear()
@@ -130,7 +129,7 @@ def propagate(self):
     def enqueue(self, lit, cause=None):
         """ Enqueue a new true literal.
         """
-        status = value(lit, self.assignments)
+        status = self.assignments.value(lit)
         if status is not None:
             # Known fact. Don't enqueue, but return whether this fact
             # contradicts the earlier assignment.
@@ -176,7 +175,7 @@ def search(self):
     def validate(self, solution_map):
         """Check whether a given set of assignments solves this SAT problem.
         """
-        solution_literals = {(+1 if status else -1) * variable
+        solution_literals = {variable if status else -variable
                              for variable, status in solution_map.items()}
         for clause in self.clauses:
             if len(set(clause.lits) & solution_literals) == 0:
@@ -285,8 +284,7 @@ def assume(self, lit):
     def number_assigned(self):
         """ Return the number of currently assigned variables.
         """
-        return len([value for value in self.assignments.values()
-                    if value is not None])
+        return self.assignments.num_assigned
 
     @property
     def number_variables(self):