from itertools import product from typing import List, Tuple, Generator, Iterable, Optional def card(b: int):# -> Generator[Tuple[int]]""" """Exercice 1""" p = [(0, 1)] * b return product(*p) def evaluer_clauses(clauses: Iterable[int], valeurs: List[int]) -> int: """Exercice 2""" for clause in clauses: idx = abs(clause) - 1 val = valeurs[idx] if clause < 0: val = 1 - val if val == 1: return val return 0 def generer_table(clauses: Iterable[int]) -> List[str]: """Exercice 3""" table = [] for valeurs in card(max(map(abs, clauses))): table.append(str(valeurs) + ' ' + str(evaluer_clauses(clauses, valeurs))) return table def lire_dimacs(filename: str = 'toy.cnf') -> Tuple[int, int, List[List[int]]]: """Exercice 4, lecture de fichier""" cnf = [[]] with open(filename, 'r') as f: for line in f: tokens = line.split() if len(tokens) == 0 or tokens[0].lower() == 'c': continue if tokens[0].lower() == 'p': nombreVariables = int(tokens[2]) nombreClauses = int(tokens[3]) else: for token in tokens: int_token = int(token) if int_token == 0: cnf.append([]) else: cnf[-1].append(int_token) cnf.pop() return nombreVariables, nombreClauses, cnf def resultat_cnf(cnf: List[List[int]], valeurs: List[int]) -> int: """Exercice 4, résultat interméditaire d'une CNF""" for clauses in cnf: if evaluer_clauses(clauses, valeurs) == 0: return 0 return 1 def table_verite_lire_dimacs(filename: str) -> List[Tuple[List[int], int]]: """Exercice 4""" nombreVariables, nombreClauses, cnf = lire_dimacs(filename) table = [] for valeurs in card(nombreVariables): table.append((valeurs, resultat_cnf(cnf, valeurs))) return table Modele = Optional[List[int]] ContreModele = Optional[List[int]] def chercher_modeles(filename: str) -> Tuple[Modele, ContreModele]: """Exercice 5, cherche modèles et contre modèles""" modele: Modele = None contre_modele: ContreModele = None for valeurs, res in table_verite_lire_dimacs(filename): if res == 1: modele = valeurs else: contre_modele = valeurs return modele, contre_modele def interpreter_chercher_modeles(modele: Modele, contre_modele: ContreModele): """Exercice 5""" if modele is None: print('Aucun modèle : formule invalide (totologie)') elif contre_modele is None: print('Aucun contre modèle : formule valide (totologie)') else: print('Formule satisfaisable et insatisfaisable :') print('Exemple de modèle :', modele) print('Exemple de contre modèle :', contre_modele) if __name__ == '__main__': #print(list(card(3))) #print(evaluer_clauses([-1, 2, -3], [1, 0, 1])) #for ligne in generer_table([-1, 2, -3]): # print(ligne) #print(table_verite_lire_dimacs('toy.cnf')) #for ligne in table_verite_lire_dimacs('toy.cnf'): # print(ligne) interpreter_chercher_modeles(*chercher_modeles('toy.cnf')) print('==========') interpreter_chercher_modeles(*chercher_modeles('totologie_0.cnf')) print('==========') interpreter_chercher_modeles(*chercher_modeles('totologie_1.cnf')) print('==========') interpreter_chercher_modeles(*chercher_modeles('reines.cnf'))