MAINT: speed up the UndeterminedClausePolicy

simplesat/sat/policy/policy.py

@@ -37,7 +37,7 @@ class DefaultPolicy(IPolicy):
     def add_requirements(self, assignments):
         pass
 
-    def get_next_package_id(self, assignments, _):
+    def get_next_package_id(self, assignments, *_):
         # Given a dictionary of partial assignments, get an undecided variable
         # to be decided next.
         undecided = (

simplesat/sat/policy/policy_logger.py

@@ -10,7 +10,7 @@ class PolicyLogger(IPolicy):
     def __init__(self, policy, args=None, kwargs=None):
         self._policy = policy
         self._log_pool = args[0]
-        self._log_installed = getattr(policy, '_installed_ids', set()).copy()
+        self._log_installed = set(getattr(policy, '_installed_ids', ()))
         self._log_preferred = getattr(policy, '_preferred_ids', set()).copy()
         self._log_args = args
         self._log_kwargs = kwargs
@@ -27,7 +27,6 @@ def get_next_package_id(self, assignments, clauses):
 
     def add_requirements(self, package_ids):
         self._log_required.extend(package_ids)
-        self._log_preferred.difference_update(package_ids)
         self._log_installed.difference_update(package_ids)
         self._policy.add_requirements(package_ids)
 
@@ -36,7 +35,7 @@ def _log_histogram(self, pkg_ids=None):
             pkg_ids = map(abs, self._log_suggestions)
         c = Counter(pkg_ids)
         lines = (
-            "{:>25} {}".format(self._log_pretty_pkg_id(k), v)
+            "{:>25} {:>5}".format(self._log_pretty_pkg_id(k), v)
             for k, v in c.most_common()
         )
         pretty = '\n'.join(lines)
@@ -52,7 +51,7 @@ def _log_pretty_pkg_id(self, pkg_id):
             repo = 'installed'
         return "{:{fill}<30} {:3} {}".format(name_ver, pkg_id, repo, fill=fill)
 
-    def _log_report(self, detailed=True):
+    def _log_report(self, detailed=True, with_assignments=True):
 
         def pkg_name(pkg_id):
             return pkg_key(pkg_id)[0]
@@ -64,22 +63,37 @@ def pkg_key(pkg_id):
         ids = map(abs, self._log_suggestions)
         report = []
         changes = []
-        if self._log_assignment_changes:
+        if self._log_assignment_changes and with_assignments:
             for pkg, change in self._log_assignment_changes[0].items():
                 name = self._log_pretty_pkg_id(pkg)
                 if change[1] is not None:
                     changes.append("{} : {}".format(name, change[1]))
             report.append('\n'.join(changes))
 
         required = set(self._log_required)
-        preferred = set(self._log_preferred)
         installed = set(self._log_installed)
         for (i, sugg) in enumerate(ids):
             pretty = self._log_pretty_pkg_id(sugg)
             R = 'R' if sugg in required else ' '
-            P = 'P' if sugg in preferred else ' '
             I = 'I' if sugg in installed else ' '
-            changes = []
+            change_str = ""
+            if with_assignments:
+                try:
+                    changes = []
+                    items = self._log_assignment_changes[i + 1].items()
+                    sorted_items = sorted(items, key=lambda p: pkg_key(p[0]))
+                    for pkg, change in sorted_items:
+                        if pkg_name(pkg) != pkg_name(sugg):
+                            _pretty = self._log_pretty_pkg_id(pkg)
+                            fro, to = map(str, change)
+                            msg = "{:10} - {:10} : {}"
+                            changes.append(msg.format(fro, to, _pretty))
+                    if changes:
+                        change_str = '\n\t'.join([''] + changes)
+                except IndexError:
+                    pass
+            msg = "{:>4} {}{} - {}{}"
+            report.append(msg.format(i, R, I, pretty, change_str))
             try:
                 change_items = self._log_assignment_changes[i + 1].items()
                 if detailed:
@@ -95,10 +109,11 @@ def pkg_key(pkg_id):
                     changes = '\n\t\t'.join([''] + changes)
                 else:
                     changes = ""
+                if any(v[1] is None
+                       for v in self._log_assignment_changes[i + 1].values()):
+                    report.append("BACKTRACKED\n")
             except IndexError:
-                changes = ""
-            msg = "{:>4} {}{}{} - {}{}"
-            report.append(msg.format(i, R, P, I, pretty, changes))
+                pass
         return '\n'.join(report)
 
 

simplesat/sat/policy/undetermined_clause_policy.py

@@ -1,6 +1,8 @@
 #!/usr/bin/env python
 # -*- coding: utf-8 -*-
 
+from collections import defaultdict
+
 import six
 
 from simplesat.utils import DefaultOrderedDict
@@ -17,15 +19,20 @@ class UndeterminedClausePolicy(IPolicy):
     def __init__(self, pool, installed_repository, prefer_installed=True):
         self._pool = pool
         self.prefer_installed = prefer_installed
-        self._installed_ids = set(
-            pool.package_id(package) for package in installed_repository
+        by_version = six.functools.partial(pkg_id_to_version, self._pool)
+        self._installed_ids = sorted(
+            (pool.package_id(package) for package in installed_repository),
+            key=by_version
         )
         self._preferred_package_ids = {
             self._package_key(package_id): package_id
             for package_id in self._installed_ids
         }
         self._decision_set = set()
         self._requirements = set()
+        self._unsatisfied_clauses = set()
+        self._id_to_clauses = defaultdict(list)
+        self._all_ids = set()
 
     def _package_key(self, package_id):
         package = self._pool._id_to_package[package_id]
@@ -34,30 +41,47 @@ def _package_key(self, package_id):
     def add_requirements(self, package_ids):
         self._requirements.update(package_ids)
 
+    def _update_cache_from_assignments(self, assignments):
+        changelog = assignments.consume_changelog()
+        for key in six.iterkeys(changelog):
+            for clause in self._id_to_clauses[key]:
+                if not any(assignments.value(l) for l in clause.lits):
+                    self._unsatisfied_clauses.add(clause)
+                else:
+                    self._unsatisfied_clauses.discard(clause)
+
+    def _build_id_to_clauses(self, clauses):
+        table = defaultdict(list)
+        for c in clauses:
+            for l in c.lits:
+                table[abs(l)].append(c)
+        self._all_ids = set(six.iterkeys(table))
+        return dict(table)
+
     def get_next_package_id(self, assignments, clauses):
         """Get the next unassigned package.
         """
+        if assignments.new_keys:
+            self._id_to_clauses = self._build_id_to_clauses(clauses)
+            self._refresh_decision_set(assignments)
         candidate_id = None
         best = self._best_candidate
 
         if self.prefer_installed:
-            candidate_id = best(self._installed_ids, assignments)
+            candidate_id = self._best_sorted_candidate(
+                self._installed_ids, assignments)
 
-        candidate_id = (
-            candidate_id or
-            self._best_candidate(self._requirements, assignments) or
-            self._best_candidate(self._decision_set, assignments)
-        )
+        if candidate_id is None:
+            candidate_id = best(self._requirements, assignments)
+
+        if candidate_id is None:
+            candidate_id = best(self._decision_set, assignments, update=True)
 
         if candidate_id is None:
-            self._decision_set.clear()
-            candidate_id = \
-                self._handle_empty_decision_set(assignments, clauses)
+            self._refresh_decision_set(assignments)
+            candidate_id = best(self._decision_set, assignments)
             if candidate_id is None:
-                candidate_id = self._best_candidate(
-                    self._decision_set,
-                    assignments
-                )
+                candidate_id = best(self._all_ids, assignments)
 
         assert assignments.get(candidate_id) is None, \
             "Trying to assign to a variable which is already assigned."
@@ -70,14 +94,19 @@ def get_next_package_id(self, assignments, clauses):
         return candidate_id
 
     def _without_assigned(self, package_ids, assignments):
-        return set(
-            pkg_id for pkg_id in package_ids
-            if assignments.get(pkg_id) is None
-        )
+        return package_ids.difference(assignments.assigned_ids)
+
+    def _best_sorted_candidate(self, package_ids, assignments):
+        for p_id in package_ids:
+            if p_id not in assignments.assigned_ids:
+                return p_id
 
-    def _best_candidate(self, package_ids, assignments):
+    def _best_candidate(self, package_ids, assignments, update=False):
         by_version = six.functools.partial(pkg_id_to_version, self._pool)
         unassigned = self._without_assigned(package_ids, assignments)
+        if update:
+            package_ids.clear()
+            package_ids.update(unassigned)
         try:
             return max(unassigned, key=by_version)
         except ValueError:
@@ -86,51 +115,26 @@ def _best_candidate(self, package_ids, assignments):
     def _group_packages_by_name(self, decision_set):
         installed_packages = []
         new_package_map = DefaultOrderedDict(list)
+        installed_ids = set(self._installed_ids)
 
         for package_id in sorted(decision_set):
             package = self._pool._id_to_package[package_id]
-            if package_id in self._installed_ids:
+            if package_id in installed_ids:
                 installed_packages.append(package)
             else:
                 new_package_map[package.name].append(package)
 
         return installed_packages, new_package_map
 
-    def _handle_empty_decision_set(self, assignments, clauses):
-        # TODO inefficient and verbose
-
-        unassigned_ids = set(
-            literal for literal, status in six.iteritems(assignments)
-            if status is None
+    def _refresh_decision_set(self, assignments):
+        self._update_cache_from_assignments(assignments)
+        self._decision_set.clear()
+        self._decision_set.update(
+            abs(lit)
+            for clause in self._unsatisfied_clauses
+            for lit in clause.lits
         )
-        assigned_ids = set(assignments.keys()) - unassigned_ids
-
-        signed_assignments = set()
-        for variable in assigned_ids:
-            if assignments[variable]:
-                signed_assignments.add(variable)
-            else:
-                signed_assignments.add(-variable)
-
-        for clause in clauses:
-            # TODO Need clause.undecided_literals property
-            if not signed_assignments.isdisjoint(clause.lits):
-                # Clause is true
-                continue
-
-            variables = map(abs, clause.lits)
-            undecided = unassigned_ids.intersection(variables)
-            self._decision_set.update(lit for lit in undecided)
-
-        if len(self._decision_set) == 0:
-            # This will happen if the remaining packages are irrelevant for
-            # the set of rules that we're trying to satisfy. In that case,
-            # just return one of the undecided IDs.
-
-            # We use min to ensure determinisism
-            return min(unassigned_ids)
-        else:
-            return None
+        self._decision_set.difference_update(assignments.assigned_ids)
 
 
 LoggedUndeterminedClausePolicy = LoggedPolicy(UndeterminedClausePolicy)