from data import (GV, Conflict, sgn, adjust_activity, UNDEF, TRUE, FALSE, PyTrue, PyFalse, Unsatisfable, Clause) from debug import DEBUG, DEBUG_FORCED from misc import unique import random class G: set_vars_N=0 # Numero di variabili assegnate. Se set_vars_N == GV.vars_N, # abbiamo trovato la soluzione. decision_stack=[[],] # formato: [[],L1, L2, ...], dove ogni L e' un livello di # decisione. L=[v1, v2, ...], con v instanza di una # variabile assegnata in quel livello. # Il livello zero e' sempre vuoto ([]). decision_level=0 if DEBUG: def count_set_vars_N(): '''Funzione di DEBUG: conta brutalmente il numero di variabili non assegnate''' return sum([1 for v in GV.vars.itervalues() if v.value != UNDEF]) def most_active_var(): '''Ritorna la variabile non assegnata piu' attiva''' if DEBUG_FORCED: for vname in sorted(GV.vars.iterkeys()): if GV.vars[vname].value == UNDEF: return GV.vars[vname] raise Exception, 'Errore, non ho ci sono piu variabili' mav=None mav_activity=0 for v in GV.vars.itervalues(): if v.value != UNDEF: continue if mav == None or v.activity > mav_activity: mav=v mav_activity=v.activity return mav def new_level(var, value, zero_level=PyFalse): '''Assegna il valore `value' alla variabile `var' e ricerca clausole unitarie. Ricursivamente assegna ogni implicazione derivata da clausole unitarie. Il decision_stack viene aggiornato solo nel caso in cui zero_level=PyFalse. Nota: assumiamo che `var' sia una variabile UNDEF''' if zero_level: level=0 else: G.decision_level+=1 G.decision_stack.append([var]) level=G.decision_level implied = var.set_value(val=value, level=level) if DEBUG: print 'new_level', level, var G.set_vars_N+=1 while implied != []: C,l,v=implied.pop(0) if C.ones: # La clausola C e' stata resa TRUE da # qualche assegnamento avvenuto in un ciclo # precedente. Adesso e' inutile considerarla. continue if DEBUG: print 'v:'+str(v.name), v.clause_list[C], 'impliedby', C try: im = v.set_value(val=v.clause_list[C], impliedby=C, level=level) if im: # aggiungi le nuove implicazioni nella queue implied+=im if level > 0: G.decision_stack[level].append(v) G.set_vars_N+=1 except Conflict: # abbiamo trovato un conflitto, risolviamolo. resolve_conflict(var=v, impliedby=C) return def resolve_conflict(var, impliedby): '''`var' e' la variabile che e' entrata in conflitto a causa della clausola `impliedby'. Le due clausole che concorrono al conflitto sono `var.impliedby' e `impliedby'. resolve_conflict() fa il raise di Unsatisfable se il problema non e' soddisfacibile, altrimenti aggiusta il decision_level e il decision_stack e aggiunge la nuova clausola di learning nel database. ''' if DEBUG: print 'conflict! var:', var, 'impliedby1:', var.impliedby, 'impliedby2:', impliedby if len(impliedby.lit)==1: # Il conflitto e' stato generato da una clausola con un solo elemento. # Il problema e' quindi non soddisfacibile. if DEBUG: print 'UNSAT: decisione preliminare, clausola unitaria' raise Unsatisfable # Assumiamo che var sia stata assegnata da un'implicazione e non da # una decisione. [E' un assunzione valida perche' trattiamo le clausole # contenenti un solo elemento in modo diverso] if DEBUG: assert var.impliedby != None ## # Consideriamo tutte le variabili che hanno partecipato al conflitto V=[ GV.vars[abs(l)] for l in var.impliedby.lit+impliedby.lit ] if DEBUG: assert var in V Vimp=[] for v in V: Vimp+=v.get_root_implications(alreadyseen=[]) # escludiamo le variabili di livello zero: sono immutabili, e' quindi # inutile includerle nella clausola di learning Vimp=[v for v in Vimp if v.level > 0] if DEBUG: print 'Vimp', [str(v) for v in V], unique([str(v) for v in Vimp]) ## # Calcoliamo tutti i livelli che dovranno essere resettati L=sorted(unique([ v.level for v in Vimp if v.level > 0 ])) if L == []: # Il conflitto e' stato generato da variabili di livello zero. # Non c'e' niente che possiamo tentare di cambiare, quindi il # problema e' non-soddisfacibile if DEBUG: print 'UNSAT: nulla da poter decidere' raise Unsatisfable # Aggiungiamo la clausole di learning nel database learned_clause=Clause([v.name*(-v.value) for v in Vimp]) if DEBUG: print 'learned_clause', learned_clause if len(learned_clause.lit)==1: # Poiche' stiamo aggiungendo una decisione nel livello zero, # resetta tutti i livelli (tranne lo zero) L=[1] # Resetta i livelli for l in reversed(L): # Resettiamo tutte le variabili dei livelli >= l # NOTA: e' proprio questo il punto in cui avviene il non-chronological backtracking for i in reversed(xrange(l, G.decision_level+1)): if DEBUG: print 'resetting level', i, str(G.decision_stack[i][0]) ds=G.decision_stack.pop() while ds != []: G.set_vars_N-=1 v=ds.pop() v.reset() G.decision_level=l-1 # Adesso che i livelli sono stati resettati, aggiorna il contatore di # variabili non assegnate learned_clause.adjust_undefs() if len(learned_clause.lit)==1: # La clausola di learning contiene un solo elemento. Per # questo motivo la aggiungiamo direttamente nel livello zero. init_zero_level([learned_clause]) def init_zero_level(zero_level_clauses): '''`zero_level_clauses' e' una lista di clausole con un solo elemento.''' for C in zero_level_clauses: if DEBUG: assert len(C.lit)==1 v=GV.vars[abs(C.lit[0])] new_level(v, sgn(C.lit[0]), zero_level=PyTrue) def solve(): '''Il loop principale della procedura di ricerca''' while G.set_vars_N != GV.vars_N: if DEBUG: assert count_set_vars_N() == G.set_vars_N # Decisione: scegli la variabile da assegnare var=most_active_var() val=random.choice([TRUE, FALSE]) if 0: #if DEBUG: import sys print 'scegli var: ' var=GV.vars[int(sys.stdin.readline())] print 'scegli value: ' val=int(sys.stdin.readline()) # crea un nuovo livello decisionale new_level(var, val) # Aggiorna i contatori di attivita' adjust_activity()