You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
103 lines
3.5 KiB
103 lines
3.5 KiB
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'))
|