#!/usr/bin/env python
#
# Corso di Laurea di Matematica
# Progetto di Logica Computazionale
#
# Implementazione di una variante dell'algoritmo di Davis Putnam per la
# risoluzione dei problemi SAT.
#
# Le caratteristiche principali di questa implementazione sono:
#       1) Codice corto e leggibile:
#            il linguaggio di programmazione ad alto livello Python consente di
#          scrivere il codice dell'implementazione in maniera sintetica ed
#          intuitiva. Il codice sorgente e' di sole ~560 righe (inclusi i
#          commenti!).
#       2) Non-chronological backtracking:
#            la procedura di ricerca ritorna indietro solo nei livelli decisionali che
#          hanno causato il conflitto. Cosi' facendo si evitano inutili
#          assegnamenti nei livelli che non contribuiscono al conflitto.
#       3) Learning:
#            dopo ogni conflitto, una nuova clausola che lo codifica viene immessa 
#          nel database. Questa tecnica permette di "indirizzare" la procedura
#          di ricerca memorizzando le decisioni che non devono essere piu'
#          prese. Inoltre, consente di dedurre le nuove implicazioni in
#          maniera piu' rapida.
#       4) Euristica per la scelta delle variabili da assegnare:
#            la variabile piu' "attiva" e' quella che viene assegnata ad ogni
#          decisione. L'attivita' delle variabili viene calcolata in base al
#          numero dei conflitti che le hanno coinvolte.
#
#
# Andrea Lo Pumo   ( alopumo@gmail.com )
# Febbraio 2009
#

import sys
from data import Unsatisfable, TrueClause, Clause, Var, GV, TRUE, FALSE, UNDEF
from misc import unique
from solver import init_zero_level, solve
from debug import DEBUG

def main():
        zero_level_clauses=[]
       
        ###
        # Leggi l'input da file oppure da stdin. Il formato dell'input e' una
        # rappresentazione python di lista di liste:
        #       [
        #         [ Z11, Z12, ... ],
        #         [ Z21, Z22, ...],
        #         ...
        #       ]
        # Ogni Zij e' un intero (positivo o negativo, diverso da zero). Vedi
        # help(Clause) per piu' informazioni.
        #
        if len(sys.argv) >=2:
                f=file(sys.argv[1])
                CLstr=f.read()
                f.close()
        else:
                CLstr=sys.stdin.read()
        # Per fare il parsing dell'input e' sufficiente usare eval()
        CL=eval(CLstr)
        ###

        #Rimuovi i duplicati di clausole
        CL2=unique([unique(C) for C in CL])
        
        # Aggiungi le clausole e le variabili nel database
        for C in CL2:
                for l in C:
                        l=abs(l)
                        if not l in GV.vars and l != TRUE:
                                GV.vars[l]=Var(name=l)
                try:
                        cl=Clause(lit=C)
                except Unsatisfable:
                        print 'Il problema e\' insoddisfacibile (clausola vuota)'
                except TrueClause:
                        # Scartiamo la clausola
                        del cl
                        continue

                if cl.undefs==1:
                        # La clausola ha un solo elemento
                        zero_level_clauses.append(cl)

        GV.vars_N=len(GV.vars)
       
        # Entra nel loop principale
        try:
                init_zero_level(zero_level_clauses)
                solve()
        except Unsatisfable:
                print 'Il problema e\' insoddisfacibile'
                if DEBUG: print '\n'.join([str(v) for v in GV.vars.itervalues() if v.level==0 and v.value != UNDEF])
                sys.exit(0)
        
        print 'Una soluzione e\': '
        if DEBUG: print '\n'.join([str(v) for v in GV.vars.itervalues() ])
        one=[v.name for v in GV.vars.itervalues() if v.value == TRUE]
        zero=[v.name for v in GV.vars.itervalues() if v.value == FALSE]
        print 'TRUE: ', one
        print 'FALSE: ', zero

if __name__ == '__main__':
        if DEBUG:
                import random
                random.seed(16)
        main()