From 4a1136a6e50294aad1eb0c38c4344c88f2ff72c2 Mon Sep 17 00:00:00 2001 From: Aleksey Lim Date: Wed, 19 Feb 2014 03:35:25 +0000 Subject: Embed 0install SAT solver to avoid fetching the entire ZI disribution --- diff --git a/.gitmodules b/.gitmodules index a442a55..361a8d7 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,3 @@ -[submodule "sugar_network/lib/zeroinstall"] - path = sugar_network/lib/zeroinstall - url = git://git.sugarlabs.org/network/0install.git [submodule "sugar_network/lib/pylru"] path = sugar_network/lib/pylru url = https://github.com/jlhutch/pylru.git diff --git a/AUTHORS b/AUTHORS index 0fc0c77..d0f1401 100644 --- a/AUTHORS +++ b/AUTHORS @@ -7,7 +7,19 @@ This work was initially started as an international research initiative in late 2011 within the `Sugar Labs Perú`_ in order to attend the needs identified during field work on Perú from 2007 to date. +**SAT solver** + +The SAT solver was inherited from the `Zero Install`_ project (until switching +its code base from Python) and adapted to Sugar Network needs. The original +code was licensed under the term of the :doc:`GPL-3.0 `. + +**Artwork** + +Images are based on `Font Awesome`_ vector icons licensed under the terms +of the :doc:`OTF 1.1 `. + **Contributors** + (In alphabetical order) * Aleksey Lim `original idea and implementation` @@ -18,11 +30,7 @@ identified during field work on Perú from 2007 to date. Aleksey Lim -**Artwork** - -* Images are based on `Font Awesome`_ vector icons licensed under the terms - of the :doc:`OTF 1.1 `. - .. _Sugar Labs Perú: http://pe.sugarlabs.org/ +.. _Zero Install: http://0install.net/ .. _Font Awesome: http://fortawesome.github.io/Font-Awesome/ diff --git a/sugar_network/lib/zeroinstall b/sugar_network/lib/zeroinstall deleted file mode 160000 -Subproject b1d59788bfc54ccdb0c8bd4dc5f90921c244de8 diff --git a/sugar_network/toolkit/sat.py b/sugar_network/toolkit/sat.py new file mode 100644 index 0000000..a908dd7 --- /dev/null +++ b/sugar_network/toolkit/sat.py @@ -0,0 +1,583 @@ +# Copyright (C) 2010 Thomas Leonard +# Copyright (C) 2014 Aleksey Lim +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# The design of this solver is very heavily based on the one described in +# the MiniSat paper "An Extensible SAT-solver [extended version 1.2]" +# http://minisat.se/Papers.html +# +# The main differences are: +# +# - We care about which solution we find (not just "satisfiable" or "not"). +# - We take care to be deterministic (always select the same versions given +# the same input). We do not do random restarts, etc. +# - We add an _AtMostOneClause (the paper suggests this in the Excercises, and +# it's very useful for our purposes). + +import logging +from collections import deque + +from sugar_network.toolkit import enforce + + +_logger = logging.getLogger('sat') + + +def solve(clauses, at_most_one_clauses, decide): + if not clauses: + _logger.info('No clauses') + return None + + max_var = 0 + for clause in clauses: + max_var = max(max_var, max([abs(i) for i in clause])) + for clause in at_most_one_clauses.values(): + max_var = max(max_var, max([abs(i) for i in clause])) + problem = _Problem(max_var) + + for clause in clauses: + if problem.add_clause(clause) is False: + _logger.info('The %r clause is unresolved', clause) + return None + clauses = {} + for name, clause in at_most_one_clauses.items(): + clauses[name] = problem.at_most_one(clause) + + if not problem.run_solver(lambda: decide(clauses)): + return None + + result = {} + for name, clause in clauses.items(): + if clause.current is not None: + result[name] = clause.current + return result + + +class _AtMostOneClause(object): + + def __init__(self, problem, varset): + self.problem = problem + self.varset = varset + + # The single literal from our set that is True. + # We store this explicitly because the decider needs to know quickly. + self.current = None + + def propagate(self, v): + # Re-add ourselves to the watch list. + # (we we won't get any more notifications unless we backtrack, + # in which case we'd need to get back on the list anyway) + self.problem.watch(v, self) + + # value[v] has just become True + assert self.problem.value(v) is True + + # If we already propagated successfully when the first + # one was set then we set all the others to False and + # anyone trying to set one True will get rejected. And + # if we didn't propagate yet, current will still be + # None, even if we now have a conflict (which we'll + # detect below). + assert self.current is None + + self.current = v + + # If we later backtrace, call our undo function to unset current + self.problem.undo[abs(v)].append(self) + + for v_ in self.varset: + value = self.problem.value(v_) + if value is True and v_ != v: + # Due to queuing, we might get called with current = None + # and two versions already selected. + _logger.trace('CONFLICT already selected %s', v_) + return False + if value is None: + # Since one of our varset is already true, all unknown ones + # can be set to False. + if not self.problem.enqueue(-v_, self): + _logger.trace('CONFLICT enqueue failed for %s', v_) + return False # Conflict; abort + + return True + + def undo(self, v): + _logger.trace('Undo %s', v) + assert v == self.current + self.current = None + + # Why is v True? + # Or, why are we causing a conflict (if v is None)? + def calc_reason(self, v): + if v is None: + # Find two True literals + trues = [] + for v_ in self.varset: + if self.problem.value(v_) is True: + trues.append(v_) + if len(trues) == 2: + return trues + else: + for v_ in self.varset: + if v_ != v and self.problem.value(v_) is True: + return [v_] + # Find one True literal + assert 0 # don't know why! + + def best_undecided(self): + for v in self.varset: + if self.problem.value(v) is None: + _logger.trace('Best undecided %r from %r', v, self.varset) + return v + return None + + def __repr__(self): + return "" % self.varset + + +class _UnionClause(object): + + def __init__(self, problem, varset): + self.problem = problem + self.varset = varset + + # Try to infer new facts. + # We can do this only when all of our literals are False except one, + # which is undecided. That is, + # False... or X or False... = True => X = True + # + # To get notified when this happens, we tell the solver to + # watch two of our undecided literals. Watching two undecided + # literals is sufficient. When one changes we check the state + # again. If we still have two or more undecided then we switch + # to watching them, otherwise we propagate. + # + # Returns False on conflict. + def propagate(self, v): + # value[get(v)] has just become False + + # For simplicity, only handle the case where self.varset[1] + # is the one that just got set to False, so that: + # - value[varset[0]] = None | True + # - value[varset[1]] = False + # If it's the other way around, just swap them before we start. + if self.varset[0] == -v: + self.varset[0], self.varset[1] = self.varset[1], self.varset[0] + + if self.problem.value(self.varset[0]) is True: + # We're already satisfied. Do nothing. + self.problem.watch(v, self) + return True + + assert self.problem.value(self.varset[1]) is False + + # Find a new literal to watch now that varset[1] is resolved, + # swap it with varset[1], and start watching it. + for i in range(2, len(self.varset)): + value = self.problem.value(self.varset[i]) + if value is not False: + # Could be None or True. If it's True then we've already done + # our job, so this means we don't get notified + # unless we backtrack, which is fine. + self.varset[1], self.varset[i] = self.varset[i], self.varset[1] + self.problem.watch(-self.varset[1], self) + return True + + # Only varset[0], is now undefined. + self.problem.watch(v, self) + return self.problem.enqueue(self.varset[0], self) + + def undo(self, v): + pass + + # Why is v True? + # Or, why are we causing a conflict (if v is None)? + def calc_reason(self, v): + assert v is None or v == self.varset[0] + + # The cause is everything except v. + return [-v_ for v_ in self.varset if v_ != v] + + def __repr__(self): + return "" % self.varset + + +class _Problem(object): + + def __init__(self, max_var): + # True/False/None + self._vars = [None] + # constraints to check when _vars[i] becomes True + self._pos_watch = [None] + # constraints to check when _vars[i] becomes False + self._neg_watch = [None] + # Constraints to update if we become unbound for every _vars[i] + self.undo = [None] + # The decision level at which we got a value for _vars[i] + self._levels = [None] + # The constraint that implied _vars, if True or False + self._reasons = [None] + # order of assignments + self._trail = [] + # decision levels (len(_trail) at each decision) + self._trail_lim = [] + # propagation queue + self._propQ = deque() + + count = max_var - len(self._vars) + 1 + self._vars.extend([None] * count) + self._pos_watch.extend([[] for __ in range(count)]) + self._neg_watch.extend([[] for __ in range(count)]) + self.undo.extend([[] for __ in range(count)]) + self._levels.extend([-1] * count) + self._reasons.extend([None] * count) + + def watch(self, v, cb): + (self._neg_watch[-v] if v < 0 else self._pos_watch[v]).append(cb) + + def value(self, v): + assert v + if v > 0: + return self._vars[v] + else: + value = self._vars[-v] + if value is None: + return None + else: + return not value + + def add_clause(self, varset): + _logger.trace('Add clause %r', varset) + + if any(self.value(v) is True for v in varset): + # Trivially true already. + return True + varset_ = set(varset) + for v in varset: + if -v in varset_: + # X or not(X) is always True. + return True + # Remove duplicates and values known to be False + varset = [v for v in varset_ if self.value(v) is not False] + + return self._add_clause(varset, learnt=False, reason="input fact") + + def at_most_one(self, varset): + _logger.trace('At most one of %r', varset) + + # If we have zero or one literals then we're trivially true + # and not really needed for the solve. However, Zero Install + # monitors these objects to find out what was selected, so + # keep even trivial ones around for that. + # + #if len(varset) < 2: + # return True # Trivially true + + # Ensure no duplicates + assert len(set(varset)) == len(varset), varset + + # Ignore any literals already known to be False. + # If any are True then they're enqueued and we'll process them + # soon. + varset = [v for v in varset if self.value(v) is not False] + + clause = _AtMostOneClause(self, varset) + for v in varset: + self.watch(v, clause) + + return clause + + def run_solver(self, decide): + """@rtype: bool""" + + while True: + # Use logical deduction to simplify the clauses + # and assign literals where there is only one possibility. + conflicting_clause = self._propagate() + if not conflicting_clause: + _logger.trace('New state: %r', self._vars[1:]) + if all(i is not None for i in self._vars[1:]): + # Everything is assigned without conflicts + _logger.trace('SUCCESS!') + return True + else: + # Pick a variable and try assigning it one way. + # If it leads to a conflict, we'll backtrack and + # try it the other way. + v = decide() + assert v is not None, "decide function returned None!" + assert self.value(v) is None + self._trail_lim.append(len(self._trail)) + r = self.enqueue(v, reason="considering") + assert r is True + else: + if self._decision_level == 0: + _logger.trace('FAIL: conflict found at top level') + return False + else: + # Figure out the root cause of this failure. + learnt, backtrack_level = self._analyse(conflicting_clause) + + self._cancel_until(backtrack_level) + + clause = self._add_clause(learnt, learnt=True, + reason=conflicting_clause) + if clause is not True: + # Everything except the first literal in learnt + # is known to be False, so the first must be True. + enforce(self.enqueue(learnt[0], clause) is True) + + # v is now True + # Returns False if this immediately causes a conflict. + def enqueue(self, v, reason): + _logger.trace('Enqueue %r', v) + + old_value = self.value(v) + if old_value is not None: + if old_value is False: + # Conflict + return False + else: + # Already set (shouldn't happen) + return True + + v_abs = abs(v) + self._vars[v_abs] = v > 0 + self._levels[v_abs] = self._decision_level + self._reasons[v_abs] = reason + self._trail.append(v) + self._propQ.append(v) + + return True + + @property + def _decision_level(self): + return len(self._trail_lim) + + # Pop most recent assignment from self._trail + def _undo_one(self): + v = self._trail[-1] + + _logger.trace('Pop %s', v) + + v_abs = abs(v) + self._vars[v_abs] = None + self._levels[v_abs] = -1 + self._reasons[v_abs] = None + self._trail.pop() + + undo = self.undo[v_abs] + while undo: + undo.pop().undo(v) + + def _cancel_until(self, level): + while self._decision_level > level: + n_this_level = len(self._trail) - self._trail_lim[-1] + _logger.trace('Cancel at level %d (%d assignments)', + self._decision_level, n_this_level) + while n_this_level != 0: + self._undo_one() + n_this_level -= 1 + self._trail_lim.pop() + + # Process the propQ. + # Returns None when done, or the clause that caused a conflict. + def _propagate(self): + while self._propQ: + watches_ = [] + v = self._propQ.popleft() + if v < 0: + watches, self._neg_watch[-v] = self._neg_watch[-v], watches_ + else: + watches, self._pos_watch[v] = self._pos_watch[v], watches_ + + _logger.trace('%s -> True : watches: %r', v, watches) + + for i, clause in enumerate(watches): + if clause.propagate(v): + continue + # Conflict, re-add remaining watches + watches_.extend(watches[i + 1:]) + # No point processing the rest of the queue as + # we'll have to backtrack now. + self._propQ.clear() + return clause + + return None + + # Returns the new clause if one was added, True if none was added + # because this clause is trivially True, or False if the clause is + # False. + def _add_clause(self, varset, learnt, reason): + if len(varset) == 1: + # A clause with only a single literal is represented + # as an assignment rather than as a clause. + return self.enqueue(varset[0], reason) + + clause = _UnionClause(self, varset) + + if learnt: + # varset[0] is None because we just backtracked. + # Start watching the next literal that we will + # backtrack over. + best_level = -1 + best_i = 1 + for i in range(1, len(varset)): + level = self._levels[abs(varset[i])] + if level > best_level: + best_level = level + best_i = i + varset[1], varset[best_i] = varset[best_i], varset[1] + + # Watch the first two literals in the clause (both must be + # undefined at this point). + for v in varset[:2]: + self.watch(-v, clause) + + return clause + + def _analyse(self, cause): + # After trying some assignments, we've discovered a conflict. + # e.g. + # - we selected A then B then C + # - from A, B, C we got X, Y + # - we have a rule: not(A) or not(X) or not(Y) + # + # The simplest thing to do would be: + # 1. add the rule "not(A) or not(B) or not(C)" + # 2. unassign C + # + # Then we we'd deduce not(C) and we could try something else. + # However, that would be inefficient. We want to learn a more + # general rule that will help us with the rest of the problem. + # + # We take the clause that caused the conflict ("cause") and + # ask it for its cause. In this case: + # + # A and X and Y => conflict + # + # Since X and Y followed logically from A, B, C there's no + # point learning this rule; we need to know to avoid A, B, C + # *before* choosing C. We ask the two varset deduced at the + # current level (X and Y) what caused them, and work backwards. + # e.g. + # + # X: A and C => X + # Y: C => Y + # + # Combining these, we get the cause of the conflict in terms of + # things we knew before the current decision level: + # + # A and X and Y => conflict + # A and (A and C) and (C) => conflict + # A and C => conflict + # + # We can then learn (record) the more general rule: + # + # not(A) or not(C) + # + # Then, in future, whenever A is selected we can remove C and + # everything that depends on it from consideration. + + # The general rule we're learning + learnt = [None] + # The deepest decision in learnt + learnt_level = 0 + # The literal we want to expand now + p = None + # The varset involved in the conflict + seen = [False] * len(self._vars) + counter = 0 + + while True: + # cause is the reason why p is True (i.e. it enqueued it). + # The first time, p is None, which requests the reason + # why it is conflicting. + if p is None: + p_reason = cause.calc_reason(p) + _logger.trace('%s failed because of %r', cause, p_reason) + else: + p_reason = cause.calc_reason(p) + _logger.trace('%s => %s because of %r', cause, p, p_reason) + + # p_reason is in the form (A and B and ...) + # p_reason => p + + # Check each of the varset in p_reason that we haven't + # already considered: + # - if the variable was assigned at the current level, + # mark it for expansion + # - otherwise, add it to learnt + + for v in p_reason: + v_abs = abs(v) + if seen[v_abs]: + continue + seen[v_abs] = True + level = self._levels[v_abs] + if level == self._decision_level: + # We deduced this var since the last decision. + # It must be in self._trail, so we'll get to it + # soon. Remember not to stop until we've processed it. + counter += 1 + elif level > 0: + # We won't expand v, just remember it. + # (we could expand it if it's not a decision, but + # apparently not doing so is useful) + learnt.append(-v) + learnt_level = max(learnt_level, level) + + # At this point, counter is the number of assigned + # varset in self._trail at the current decision level that + # we've seen. That is, the number left to process. Pop + # the next one off self._trail (as well as any unrelated + # varset before it; everything up to the previous + # decision has to go anyway). + + # On the first time round the loop, we must find the + # conflict depends on at least one assignment at the + # current level. Otherwise, simply setting the decision + # variable caused a clause to conflict, in which case + # the clause should have asserted not(decision-variable) + # before we ever made the decision. + # On later times round the loop, counter was already > + # 0 before we started iterating over p_reason. + assert counter > 0 + + while True: + p = self._trail[-1] + cause = self._reasons[abs(p)] + self._undo_one() + if seen[abs(p)]: + break + _logger.trace('(irrelevant)') + counter -= 1 + + if counter <= 0: + assert counter == 0 + # If counter = 0 then we still have one more + # literal (p) at the current level that we + # could expand. However, apparently it's best + # to leave this unprocessed (says the minisat + # paper). + break + + # p is the literal we decided to stop processing on. It's either + # a derived variable at the current level, or the decision that + # led to this level. Since we're not going to expand it, add it + # directly to the learnt clause. + learnt[0] = -p + + return learnt, learnt_level diff --git a/tests/__init__.py b/tests/__init__.py index b93e388..81c8b4e 100644 --- a/tests/__init__.py +++ b/tests/__init__.py @@ -24,7 +24,6 @@ from sugar_network.db import files from sugar_network.client import IPCConnection, journal, routes as client_routes from sugar_network.client.routes import ClientRoutes, _Auth from sugar_network import db, client, node, toolkit, model -from sugar_network.client import solver from sugar_network.model.user import User from sugar_network.model.context import Context from sugar_network.model.post import Post @@ -116,9 +115,6 @@ class Test(unittest.TestCase): http._RECONNECTION_NUMBER = 0 toolkit.cachedir.value = tmpdir + '/tmp' journal._ds_root = tmpdir + '/datastore' - solver.nodeps = False - solver._stability = None - solver._conn = None downloads._POOL_SIZE = 256 gbus.join() diff --git a/tests/units/toolkit/__main__.py b/tests/units/toolkit/__main__.py index 68cb254..0e33682 100644 --- a/tests/units/toolkit/__main__.py +++ b/tests/units/toolkit/__main__.py @@ -13,6 +13,7 @@ from spec import * from router import * from gbus import * from i18n import * +from sat import * if __name__ == '__main__': tests.main() diff --git a/tests/units/toolkit/sat.py b/tests/units/toolkit/sat.py new file mode 100755 index 0000000..4202789 --- /dev/null +++ b/tests/units/toolkit/sat.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python +# sugar-lint: disable + +from __init__ import tests + +from sugar_network.toolkit import sat + + +class SAT(tests.Test): + + def test_AtMostOne(self): + self.assertEqual( + {'c': 1}, + sat.solve([[1]], {'c': [1]}, decide)) + self.assertEqual( + {'c': 1}, + sat.solve([[1, 2]], {'c': [1, 2]}, decide)) + self.assertEqual( + {'c': 1}, + sat.solve([[1, 2, 3]], {'c': [1, 2, 3]}, decide)) + + def test_DeepSolve(self): + self.assertEqual({ + 'c1': 1, + 'c2': 2, + 'c3': 3, + 'c4': 5, + }, + sat.solve( + [ + [1, 6], [-1, 2], + [-2, 3], + [-3, 5], + ], + { + 'c1': [1, 6], + 'c2': [2], + 'c3': [3], + 'c4': [4, 5], + }, + decide)) + + def test_SwitchToAnotherBranch(self): + self.assertEqual({ + 'c1': 6, + 'c4': 4, + }, + sat.solve( + [ + [1, 6], [-1, 2], [-6, 4], + [-2, 3], [-2, 4], + [-3, 5], + ], + { + 'c1': [1, 6], + 'c2': [2], + 'c3': [3], + 'c4': [4, 5], + }, + decide)) + + def __test_zi(self): + from zeroinstall.injector import sat + + problem = sat.Problem() + + v1 = problem.add_variable(1) + v2 = problem.add_variable(2) + v3 = problem.add_variable(3) + v4 = problem.add_variable(4) + v5 = problem.add_variable(5) + v6 = problem.add_variable(6) + + c1 = problem.at_most_one([v1, v6]) + problem.add_clause([v1, v6]) + problem.add_clause([sat.neg(v1), v2]) + problem.add_clause([sat.neg(v6), v4]) + + c2 = problem.at_most_one([v2]) + problem.add_clause([sat.neg(v2), v3]) + problem.add_clause([sat.neg(v2), v4]) + + c3 = problem.at_most_one([v3]) + problem.add_clause([sat.neg(v3), v5]) + + c4 = problem.at_most_one([v4, v5]) + + assert problem.run_solver(lambda: decide({'c1': c1, 'c2': c2, 'c3': c3, 'c4': c4})) + self.assertEqual(v6, c1.current) + self.assertEqual(None, c2.current) + self.assertEqual(None, c3.current) + self.assertEqual(v4, c4.current) + + +def decide(clauses): + for i in clauses.values(): + if i.current is None: + r = i.best_undecided() + if r is not None: + return r + + +if __name__ == '__main__': + tests.main() -- cgit v0.9.1