constraints.py
Go to the documentation of this file.
00001 # -*- coding: utf-8 -*-
00002 
00003 import itertools
00004 
00005 import pddl
00006 
00007 class NegativeClause(object):
00008     # disjunction of inequalities
00009     def __init__(self, parts):
00010         self.parts = parts
00011         assert len(parts)
00012 
00013     def __str__(self):
00014         disj = " or ".join(["(%s != %s)" % (v1, v2) 
00015                             for (v1, v2) in self.parts])
00016         return "(%s)" % disj
00017 
00018     def is_satisfiable(self):
00019         for part in self.parts:
00020             if part[0] != part[1]:
00021                 return True
00022         return False
00023 
00024     def apply_mapping(self, m):
00025         new_parts = [(m.get(v1, v1), m.get(v2, v2)) for (v1, v2) in self.parts]
00026         return NegativeClause(new_parts)
00027 
00028 
00029 class Assignment(object):
00030     def __init__(self, equalities):
00031         self.equalities = tuple(equalities)
00032         # represents a conjunction of expressions ?x = ?y or ?x = d
00033         # with ?x, ?y being variables and d being a domain value
00034 
00035         self.consistent = None
00036         self.mapping = None
00037         self.eq_classes = None
00038 
00039     def __str__(self):
00040         conj = " and ".join(["(%s = %s)" % (v1, v2) 
00041                             for (v1, v2) in self.equalities])
00042         return "(%s)" % conj
00043     
00044     def _compute_equivalence_classes(self):
00045         eq_classes = {}
00046         for (v1, v2) in self.equalities:
00047             c1 = eq_classes.setdefault(v1, set([v1]))
00048             c2 = eq_classes.setdefault(v2, set([v2]))
00049             if c1 is not c2:
00050                 if len(c2) > len(c1):
00051                     v1, c1, v2, c2 = v2, c2, v1, c1
00052                 c1.update(c2)
00053                 for elem in c2:
00054                     eq_classes[elem] = c1
00055         self.eq_classes = eq_classes
00056     
00057     def _compute_mapping(self):
00058         if not self.eq_classes:
00059             self._compute_equivalence_classes()
00060 
00061         # create mapping: each key is mapped to the smallest
00062         # element in its equivalence class (with objects being
00063         # smaller than variables)
00064         mapping = {}
00065         for eq_class in self.eq_classes.itervalues():
00066             variables = [item for item in eq_class 
00067                          if isinstance(item, pddl.Variable)]
00068             constants = [item for item in eq_class 
00069                          if not isinstance(item, pddl.Variable)]
00070             if len(constants) >= 2:
00071                 self.consistent = False
00072                 self.mapping = None
00073                 return
00074             if constants:
00075                 set_val = constants[0]
00076             else:
00077                 set_val = min(variables)
00078             for entry in eq_class:
00079                 mapping[entry] = set_val
00080         self.consistent = True
00081         self.mapping = mapping
00082 
00083     def is_consistent(self):
00084         if self.consistent is None:
00085             self._compute_mapping()
00086         return self.consistent
00087 
00088     def get_mapping(self):
00089         if self.consistent is None:
00090             self._compute_mapping()
00091         return self.mapping
00092 
00093 
00094 class ConstraintSystem(object):
00095     def __init__(self):
00096         self.combinatorial_assignments = []
00097         self.neg_clauses = []
00098     
00099     def __str__(self):
00100         combinatorial_assignments = []
00101         for comb_assignment in self.combinatorial_assignments:
00102             disj = " or ".join([str(assig) for assig in comb_assignment])
00103             disj = "(%s)" % disj 
00104             combinatorial_assignments.append(disj)
00105         assigs = " and\n".join(combinatorial_assignments)
00106         
00107         neg_clauses = [str(clause) for clause in self.neg_clauses]
00108         neg_clauses = " and ".join(neg_clauses)
00109         return assigs + "(" + neg_clauses + ")"
00110 
00111     def _all_clauses_satisfiable(self, assignment):
00112         mapping = assignment.get_mapping()
00113         for neg_clause in self.neg_clauses:
00114             clause = neg_clause.apply_mapping(mapping)
00115             if not clause.is_satisfiable():
00116                 return False
00117         return True
00118     
00119     def _combine_assignments(self, assignments):
00120         new_equalities = []
00121         for a in assignments:
00122             new_equalities.extend(a.equalities)
00123         return Assignment(new_equalities)
00124 
00125     def add_assignment(self, assignment):
00126         self.add_assignment_disjunction([assignment])
00127 
00128     def add_assignment_disjunction(self, assignments):
00129         self.combinatorial_assignments.append(assignments)
00130 
00131     def add_negative_clause(self, negative_clause):
00132         self.neg_clauses.append(negative_clause)
00133 
00134     def combine(self, other):
00135         """Combines two constraint systems to a new system"""
00136         combined = ConstraintSystem()
00137         combined.combinatorial_assignments = (self.combinatorial_assignments +
00138                                               other.combinatorial_assignments)
00139         combined.neg_clauses = self.neg_clauses + other.neg_clauses
00140         return combined
00141 
00142     def copy(self):
00143         other = ConstraintSystem()
00144         other.combinatorial_assignments = list(self.combinatorial_assignments)
00145         other.neg_clauses = list(self.neg_clauses)
00146         return other
00147 
00148     def dump(self):
00149         print "AssignmentSystem:"
00150         for comb_assignment in self.combinatorial_assignments:
00151             disj = " or ".join([str(assig) for assig in comb_assignment])
00152             print "  ASS: ", disj
00153         for neg_clause in self.neg_clauses:
00154             print "  NEG: ", str(neg_clause)
00155         
00156     def is_solvable(self):
00157         """Check whether the combinatorial assignments include at least
00158            one consistent assignment under which the negative clauses
00159            are satisfiable"""
00160         for assignments in itertools.product(*self.combinatorial_assignments):
00161             combined = self._combine_assignments(assignments)
00162             if not combined.is_consistent():
00163                 continue
00164             if self._all_clauses_satisfiable(combined):
00165                 return True
00166         return False
00167 
00168 
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Defines


tfd_modules
Author(s): Maintained by Christian Dornhege (see AUTHORS file).
autogenerated on Tue Jan 22 2013 12:25:02