Lyon, le 03/06/2021

SATisfieur

Problems in DIMACS-CNF format:

Version 15
URL des CNF définies :
Evolutions : ici
C'est un travail en cours, directement inspiré du problème "SAT".
L'algorithme est conçu pour se terminer en un temps polynomial. Cependant, il lui arrive de qualifier certains problàmes SAT de non satisfaisables alors qu'ils le sont. Cela dit, si tel n'était pas le cas, je serais milliononaire, cet algorithme étant directement lié à l'un des sept problèmes du prix du millénaire :-)
Par ailleurs, sa performance reste à améliorer sensiblement pour qu'il puisse se frotter aux solveurs SAT qu'on peut trouver ici et là. Le temps important qu'il met pour résoudre les problèmes SAT est essentiellement dû à l'utilisation d'une (toute petite) librairie que j'ai développée, permettant de faire un type de calculs très particulier, à savoir le calcul sur des nombres entre 0 et 1 dans leurs développement décimal en base 2, avec un nombre arbitraire de décimales. L'exemple ci-dessous montre que sur un certain type de calculs, Wolfram échoue là où ma libriarie réussit :

Pour vous en convaincre, vous pouvez taper la ligne de commande suivante dans la console de votre navigateur :

retour