[WIP] Introduce priority queue-based policy again... again

CHANGES.rst

@@ -10,6 +10,9 @@ Enhancements
 
 * Details relating to unsatisfiable scenarios are captured in an ``UNSAT``
   object and attached to the ``SatisifiabilityError`` raised (#101).
+* Adds a second policy based on a priority queue (#131)
+* Major speed improvements in the policies and assignment tracker (#131)
+
 
 Bugs Fixed
 ----------
@@ -18,6 +21,7 @@ Bugs Fixed
 * Some sort operations that were using non-unique keys have been fixed (#101).
 * Assumptions are now represented as an empty Clause object (#101).
 
+
 Version 0.1.0
 =============
 

scripts/solve.py

@@ -36,7 +36,9 @@ def solve_and_print(request, remote_repositories, installed_repository,
         print(e.unsat._find_requirement_time.pretty(fmt), file=sys.stderr)
 
     if debug:
-        report = solver._policy._log_report(detailed=(debug > 1))
+        counts, hist = solver._policy._log_histogram()
+        print(hist, file=sys.stderr)
+        report = solver._policy._log_report(with_assignments=debug > 1)
         print(report, file=sys.stderr)
     print(solver._last_rules_time.pretty(fmt), file=sys.stderr)
     print(solver._last_solver_init_time.pretty(fmt), file=sys.stderr)

simplesat/priority_queue.py

@@ -0,0 +1,176 @@
+#!/usr/bin/env python
+# -*- coding: utf-8 -*-
+
+from collections import defaultdict
+from functools import partial
+from heapq import heappush, heappop
+from itertools import count
+
+import six
+
+
+class _REMOVED_TASK(object):
+    pass
+REMOVED_TASK = _REMOVED_TASK()
+
+
+class PriorityQueue(object):
+    """ A priority queue implementation that supports reprioritizing or
+    removing tasks, given that tasks are unique.
+
+    Borrowed from: https://docs.python.org/3/library/heapq.html
+    """
+
+    def __init__(self):
+        # list of entries arranged in a heap
+        self._pq = []
+        # mapping of tasks to entries
+        self._entry_finder = {}
+        # unique id genrator for tie-breaking
+        self._next_id = partial(next, count())
+
+    def __len__(self):
+        return len(self._entry_finder)
+
+    def __bool__(self):
+        return bool(len(self))
+
+    def __contains__(self, task):
+        return task in self._entry_finder
+
+    def clear(self):
+        self._pq = []
+        self._entry_finder = {}
+
+    def push(self, task, priority=0):
+        "Add a new task or update the priority of an existing task"
+        return self._push(priority, self._next_id(), task)
+
+    def peek(self):
+        """ Return the task with the lowest priority.
+
+        This will pop and repush if a REMOVED task is found.
+        """
+        if not self._pq:
+            raise KeyError('peek from an empty priority queue')
+        entry = self._pq[0]
+        if entry[-1] is REMOVED_TASK:
+            entry = self._pop()
+        self._push(*entry)
+        return entry[-1]
+
+    def pop(self):
+        'Remove and return the lowest priority task. Raise KeyError if empty.'
+        _, _, task = self._pop()
+        return task
+
+    def pop_many(self, n=None):
+        """ Return a list of length n of popped elements. If n is not
+        specified, pop the entire queue. """
+        if n is None:
+            n = len(self)
+        result = []
+        for _ in range(n):
+            result.append(self.pop())
+        return result
+
+    def discard(self, task):
+        "Remove an existing task if present. If not, do nothing."
+        try:
+            self.remove(task)
+        except KeyError:
+            pass
+
+    def remove(self, task):
+        "Remove an existing task. Raise KeyError if not found."
+        entry = self._entry_finder.pop(task)
+        entry[-1] = REMOVED_TASK
+
+    def _pop(self):
+        while self._pq:
+            entry = heappop(self._pq)
+            if entry[-1] is not REMOVED_TASK:
+                del self._entry_finder[entry[-1]]
+                return entry
+        raise KeyError('pop from an empty priority queue')
+
+    def _push(self, priority, task_id, task):
+        if task in self:
+            o_priority, _, o_task = self._entry_finder[task]
+            # Still check the task, which might now be REMOVED
+            if priority == o_priority and task == o_task:
+                # We're pushing something we already have, do nothing
+                return
+            else:
+                # Make space for the new entry
+                self.remove(task)
+        entry = [priority, task_id, task]
+        self._entry_finder[task] = entry
+        heappush(self._pq, entry)
+
+
+class GroupPrioritizer(object):
+
+    """ A helper for assigning hierarchical priorities to items
+    according to priority groups. """
+
+    def __init__(self, order_key_func=lambda x: x):
+        """
+        Parameters
+        ----------
+        `order_key_func` : callable
+            used to sort items in each group.
+        """
+        self.key_func = order_key_func
+        self._priority_groups = defaultdict(set)
+        self._item_priority = {}
+        self.known = frozenset()
+        self.dirty = True
+
+    def __contains__(self, item):
+        return item in self._item_priority
+
+    def __getitem__(self, item):
+        "Return the priority of an item."
+        if self.dirty:
+            self._prioritize()
+        return self._item_priority[item]
+
+    def get(self, item, default=None):
+        if item in self:
+            return self[item]
+        return default
+
+    def items(self):
+        "Return an (item, priority) iterator for all items."
+        if self.dirty:
+            self._prioritize()
+        return six.iteritems(self._item_priority)
+
+    def update(self, items, group):
+        """Add `items` to the `group`, remove `items` from all other groups,
+        and update all priority values."""
+        self.known = self.known.union(items)
+        for _group, _items in self._priority_groups.items():
+            if _group != group:
+                _items.difference_update(items)
+        self._priority_groups[group].update(items)
+        self.dirty = True
+
+    def group(self, group):
+        "Return the set of items in `group`."
+        if group not in self._priority_groups:
+            raise KeyError(repr(group))
+        return self._priority_groups[group]
+
+    def _prioritize(self):
+        item_priority = {}
+
+        for group, items in six.iteritems(self._priority_groups):
+            ordered_items = sorted(items, key=self.key_func)
+            for rank, item in enumerate(ordered_items):
+                priority = (group, rank)
+                item_priority[item] = priority
+
+        self._item_priority = item_priority
+        self.dirty = False

simplesat/sat/assignment_set.py

@@ -1,77 +1,89 @@
 #!/usr/bin/env python
 # -*- coding: utf-8 -*-
 
-from collections import OrderedDict
-
 import six
 
 
-class _MISSING(object):
-    def __str__(self):
-        return '<MISSING>'
-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._data = {}
         self._orig = {}
+        self._seen = set()
         self._cached_changelog = None
-        self._assigned_literals = set()
+        self._assigned_ids = set()
+        self.new_keys = set()
         for k, v in (assignments or {}).items():
             self[k] = v
 
     def __setitem__(self, key, value):
-        assert key > 0
 
-        prev_value = self.get(key)
+        abskey = abs(key)
 
-        if prev_value is not None:
-            self._assigned_literals.difference_update((key, -key))
+        if abskey not in self._seen:
+            self.new_keys.add(abskey)
 
-        if value is not None:
-            self._assigned_literals.add(key if value else -key)
+        if value is None:
+            del self[key]
+        else:
+            self._update_diff(key, value)
+            self._data[key] = value
+            self._data[-key] = not value
+            self._assigned_ids.add(abs(key))
 
-        self._update_diff(key, value)
-        self._data[key] = value
+        self._seen.add(abskey)
 
     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))
+        self._seen.discard(abs(key))
+        if key not in self._data:
+            return
+        self._update_diff(key, None)
+        del self._data[key]
+        del self._data[-key]
+        self._assigned_ids.discard(abs(key))
 
     def __getitem__(self, key):
-        return self._data[key]
+        val = self._data.get(key)
+        if val is None and abs(key) not in self._seen:
+            raise KeyError(key)
+        return val
 
     def get(self, key, default=None):
         return self._data.get(key, default)
 
     def __len__(self):
-        return len(self._data)
+        return len(self._seen)
+
+    def __iter__(self):
+        return iter(self.keys())
 
     def __contains__(self, key):
-        return key in self._data
+        return abs(key) in self._seen
 
     def items(self):
-        return list(self._data.items())
+        return sorted(
+            (k, self._data.get(k))
+            for k in self._seen)
 
     def iteritems(self):
-        return six.iteritems(self._data)
+        return iter(self.items())
 
     def keys(self):
-        return list(self._data.keys())
+        return [k for k, _ in self.items()]
 
     def values(self):
-        return list(self._data.values())
+        return [v for _, v in self.items()]
 
     def _update_diff(self, key, value):
-        prev = self._data.get(key, MISSING)
+        # This must be called before _data is updated
+        if key < 0 and value is not None:
+            key = -key
+            value = not value
+        prev = self._data.get(key)
         self._orig.setdefault(key, prev)
         # If a value changes, dump the cached changelog
         self._cached_changelog = None
@@ -81,7 +93,7 @@ def get_changelog(self):
             self._cached_changelog = {
                 key: (old, new)
                 for key, old in six.iteritems(self._orig)
-                for new in [self._data.get(key, MISSING)]
+                for new in [self._data.get(key)]
                 if new != old
             }
         return self._cached_changelog
@@ -90,24 +102,33 @@ def consume_changelog(self):
         old = self.get_changelog()
         self._orig = {}
         self._cached_changelog = {}
+        self.new_keys.clear()
         return old
 
     def copy(self):
         new = AssignmentSet()
         new._data = self._data.copy()
         new._orig = self._orig.copy()
-        new._assigned_literals = self._assigned_literals.copy()
+        new._seen = self._seen.copy()
+        new._assigned_ids = self._assigned_ids.copy()
+        new.new_keys = self.new_keys.copy()
         return new
 
+    def to_dict(self):
+        return dict(self.items())
+
     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
+        """ Return the value of literal. """
+        return self._data.get(lit)
 
     @property
     def num_assigned(self):
-        return len(self._assigned_literals)
+        return len(self._assigned_ids)
+
+    @property
+    def assigned_ids(self):
+        return self._assigned_ids
+
+    @property
+    def unassigned_ids(self):
+        return self._seen.difference(self._assigned_ids)

simplesat/sat/policy/__init__.py

@@ -4,5 +4,9 @@
 from .undetermined_clause_policy import (
     LoggedUndeterminedClausePolicy, UndeterminedClausePolicy
 )
+from .priority_queue_policy import (
+    LoggedPriorityQueuePolicty, PriorityQueuePolicy
+)
 
-InstalledFirstPolicy = LoggedUndeterminedClausePolicy
+#  InstalledFirstPolicy = LoggedUndeterminedClausePolicy
+InstalledFirstPolicy = LoggedPriorityQueuePolicty

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 = (