gophersat
1.0.0
Il s'agit de Gophersat, un solveur SAT et pseudo-booléen écrit uniquement en Go. Gophersat a été développé par le CRIL (Centre de Recherche en Informatique de Lens) de l'Université d'Artois et du CNRS. Il est publié sous licence MIT. Gophersat est plutôt efficace, c'est-à-dire que sur les benchmarks SAT typiques, il fonctionne environ 2 à 5 fois plus lentement que les solveurs de haut niveau (à savoir glucose ou minisat) dont il s'inspire fortement. Il peut également résoudre des problèmes MAXSAT ainsi que des problèmes de décision et d'optimisation pseudo-booléens.
La dernière version stable de Gophersat est la version 1.4. Il inclut la stratégie facultative de résolution des plans de coupe.
Certains problèmes, comme le fameux problème du casier, prennent beaucoup de temps à être résolus par un raisonnement logique pur.
Le problème des casiers peut s'exprimer ainsi : est-il possible de mettre n pigeons dans m casiers, où m = n-1, sans mettre plusieurs pigeons dans le même casier et sans mettre tous les pigeons dans un casier ? La réponse est évidente : si vous avez 4 pigeons dans 3 trous, vous ne pouvez pas tous les mettre dans un trou différent. Mais comment prouver cela ? Un solveur SAT ou PB le prouvera en essayant toutes les combinaisons possibles, et le nombre de combinaisons possibles augmente de façon exponentielle. Ainsi, essayer de résoudre le problème avec n = 20 n’est pas réalisable en pratique, même si le problème a une réponse évidente.
Certains solveurs PB implémentent une stratégie alternative : la stratégie des plans coupants. Elle ne sera pas décrite en détail dans ce document, mais cette stratégie peut être extrêmement efficace sur certains problèmes, comme le problème du casier qui ne peut pas être résolu efficacement par un raisonnement logique pur, mais sera plus lent sur la plupart des problèmes.
Il est désormais possible d'utiliser les plans coupants avec Gophersat. Utilisez simplement l'option de ligne de commande -cp . Donc au lieu d'appeler :
gophersat problem.opb
Appelez simplement :
gophersat -cp problem.opb
La dernière version stable de Gophersat est la version 1.3. Il s'agit d'une mise à jour mineure, ajoutant la possibilité d'accéder au solveur sous-jacent lors du traitement de problèmes MAXSAT.
Gophersat version 1.2 inclut un moyen de comprendre les instances UNSAT, à la fois en fournissant des certificats RUP lorsqu'un problème est UNSAT et en offrant la possibilité d'extraire des sous-ensembles insatisfaisants de la formule. De nombreux bugs ont également été corrigés et la prise en charge de la résolution incrémentielle de SAT a été améliorée.
Pour en savoir plus sur ces fonctionnalités, vous pouvez consulter le tutoriel sur les certificats UNSAT et les MUS.
Pour générer un certificat avec l'exécutable gophersat, appelez simplement :
gophersat -certified problem.cnf
Le certificat sera ensuite imprimé sur la sortie standard, en utilisant la notation RUP. Le certificat est généré à la volée, sachez donc qu'un certificat partiel et inutile sera généré même si le problème est réellement résoluble. C'est une pratique courante dans la communauté, et bien que les clauses générées soient un bruit inutile, en pratique ce n'est pas un problème.
Pour extraire un MUS d'une instance UNSAT, appelez simplement :
gophersat -mus problem.cnf
Le MUS sera ensuite imprimé sur la sortie standard. Si le problème n'est pas UNSAT, un message d'erreur s'affichera.
Pour l'instant, ces fonctionnalités ne sont disponibles que pour des problèmes SAT purs (c'est-à-dire pas des problèmes pseudo-booléens).
Depuis sa version 1.1, Gophersat inclut un nouveau solveur de base plus efficace pour les problèmes SAT purs et un package traitant des problèmes MAXSAT. Il comprend également une nouvelle API pour l'optimisation et le comptage de modèles, dans laquelle les nouveaux modèles sont écrits dans les canaux dès qu'ils sont trouvés.
Depuis la version 1.0, l'API de Gophersat est considérée comme stable, ce qui signifie qu'elle est garantie de rester rétrocompatible jusqu'à un changement de version majeur. Autrement dit, si votre programme fonctionne avec la version 1.0 de gophersat, il fonctionnera toujours avec la version 1.1 ou supérieure, mais pas nécessairement avec les versions supérieures à 2.0.
Notez que, par « fonctionne toujours », nous entendons uniquement « compilera et produira le même résultat », et non « aura les mêmes performances en termes de mémoire ou de temps ». Il s'agit d'une distinction importante : lors de mises à niveau de versions mineures, de nouvelles heuristiques ou types de données peuvent être introduits, ce qui signifie que certains problèmes donnés peuvent être résolus plus rapidement ou plus lentement qu'auparavant.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat peut être utilisé comme solveur autonome (lecture de fichiers DIMACS CNF) ou comme bibliothèque dans n'importe quel programme go.
Pour résoudre un fichier DIMACS, vous pouvez appeler gophersat avec la syntaxe suivante :
gophersat --verbose file.cnf
où --verbose est un paramètre facultatif qui permet au solveur d'afficher des informations pendant le processus de résolution.
Gophersat est également capable de lire et de résoudre des formules booléennes plus générales, et pas seulement des problèmes représentés dans le format DIMACS peu convivial. Il traite également nativement les contraintes de cardinalité, c'est-à-dire les clauses qui doivent avoir au moins n littéraux vrais, avec n > 1.
Gophersat peut être utilisé comme solveur autonome (lecture de fichiers OPB) ou comme bibliothèque dans n'importe quel programme go.
Pour résoudre un problème pseudo-booléen (qu'il s'agisse d'un problème de décision ou d'optimisation), vous pouvez appeler gophersat avec la syntaxe suivante :
gophersat --verbose file.opb
où --verbose est un paramètre facultatif qui permet au solveur d'afficher des informations pendant le processus de résolution.
Pour l'instant, il ne peut résoudre que les problèmes dits DEC-SMALLINT-LIN et OPT-SMALLINT-LIN, c'est à dire des problèmes de décision (y a-t-il une solution ou non), pour des contraintes linéaires (une somme de littéraux pondérés) sur des petits entiers. (n < 2^30), ou des problèmes d'optimisation (quelle est la meilleure solution, minimisant une fonction de coût donnée), pour des contraintes linéaires sur de petits entiers.
Grâce au package maxsat , Gophersat peut désormais résoudre les problèmes de MAXSAT.
Pour résoudre un problème MAXSAT pondéré, vous pouvez appeler gophersat avec la syntaxe suivante :
gophersat --verbose file.wcnf
où --verbose est un paramètre facultatif qui permet au solveur d'afficher des informations pendant le processus de résolution. Le fichier est censé être représenté au (format WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT, qui signifie Boolean Satisfiability Problem , est le problème canonique NP-complet, c'est-à-dire un problème pour lequel il n'existe pas de solution connue qui ne prenne pas un temps exponentiel dans le pire des cas. En quelques mots, un solveur SAT essaie de trouver, pour une formule propositionnelle donnée, une affectation pour toutes ses variables qui la rende vraie, si une telle affectation existe.
Bien qu'il soit trivial d'implémenter un solveur SAT utilisant un algorithme naïf, une telle implémentation serait très inefficace en pratique. Gophersat implémente des fonctionnalités de pointe et est donc assez efficace, ce qui le rend utilisable en pratique dans les programmes Go nécessitant un moteur d'inférence efficace.
Bien que ce ne soit pas toujours la meilleure décision pour des raisons pratiques, tout problème NP-complet peut être traduit en problème SAT et résolu par Gophersat. Ces problèmes incluent le problème du voyageur de commerce, la programmation par contraintes, le problème du sac à dos, la planification, la vérification du modèle, la vérification de l'exactitude du logiciel, etc.
Pour en savoir plus sur le problème SAT, consultez l'article de Wikipédia sur SAT.
Vous pouvez également trouver des informations sur la façon de représenter vos propres formules booléennes afin qu'elles puissent être utilisées par gophersat dans le tutoriel "SAT pour les noobs".
MAXSAT est l'équivalent d'optimisation du problème de décision SAT. Alors qu'un solveur SAT pur renverra soit un modèle satisfaisant toutes les clauses, soit UNSAT si aucun modèle de ce type n'existe, un solveur MAXSAT renverra un modèle qui satisfait autant de clauses que possible.
Il existe des extensions à MAXSAT.
MAXSAT partiel signifie que, même si nous souhaitons satisfaire autant de clauses que possible, certaines clauses (appelées clauses dures ) doivent être satisfaites, quoi qu'il arrive. Un problème MAXSAT partiel peut ainsi être déclaré insatisfaisant.
Par exemple, générer un emploi du temps pour une école est un problème partiel de MAXSAT : il y a à la fois des problèmes doux (nous voulons avoir le moins de cours possible commençant après 16 heures, par exemple) et difficiles (deux enseignants ne peuvent pas être à deux endroits différents à la même heure). en même temps) contraintes.
Le MAXSAT pondéré signifie que les clauses sont associées à un coût : bien que facultatives, certaines clauses sont jugées plus importantes que d'autres. Par exemple, si la clause C1 a un coût de 3 et que les clauses C2 et C3 ont toutes deux un coût de 1, une solution satisfaisant C1 mais ni C2 ni C3 sera considérée comme meilleure qu'une solution satisfaisant à la fois C2 et C3 mais pas C1, tous les autres toutes choses étant égales.
MAXSAT à pondération partielle signifie qu'il y a à la fois des clauses souples et dures dans le problème, et que les clauses souples sont pondérées. À cet égard, MAXSAT « pur » est un cas particulier du MAXSAT à pondération partielle plus générique : un problème MAXSAT « pur » est un problème MAXSAT à pondération partielle où toutes les clauses sont des clauses souples associées à un poids de 1.
Les problèmes pseudo-booléens sont, en quelque sorte, une généralisation des problèmes SAT : toute clause propositionnelle peut être écrite comme une seule contrainte pseudo-booléenne, mais représenter une contrainte pseudo-booléenne peut nécessiter un nombre exponentiel de clauses propositionnelles.
Une expression pseudo-booléenne (linéaire) est une expression du type :
w1 l1 + w2 x2 + ... + wn xn ≥ y
où y et tous wi sont des constantes entières et tous li sont des littéraux booléens.
Par exemple, pour que l'expression suivante soit vraie
2 ¬x1 + x2 + x3 ≥ 3
la variable booléenne x1 doit être fausse et au moins l'un de x2 et x3 doit être vrai. Ceci est équivalent à la formule propositionnelle
¬x1 ∧ (x2 ∨ x3)
Les expressions pseudo-booléennes sont une généralisation des clauses propositionnelles : toute clause
x1 ∨ x2 ∨ ... ∨ xn
peut être réécrit comme
x1 + x2 + ... + xn ≥ 1
La description d’un problème pseudo-booléen peut être exponentiellement plus petite que celle de son homologue propositionnel, mais la résolution d’un problème pseudo-booléen reste NP-complète.
Gophersat résout à la fois les problèmes de décision (y a-t-il une solution au problème) et les problèmes d'optimisation. Un problème d'optimisation est un problème pseudo-booléen associé à une fonction de coût, c'est à dire une somme de termes qu'il faut minimiser. Plutôt que d'essayer simplement de trouver un modèle qui satisfait aux contraintes données, Gophersat tentera alors de trouver un modèle garantissant à la fois la satisfaction des contraintes et la minimisation de la fonction de coût.
Lors de la recherche de ces solutions optimales, Gophersat fournira des solutions sous-optimales (c'est-à-dire des solutions qui résolvent toutes les contraintes mais ne sont pas encore garanties comme étant optimales) dès qu'il les trouvera, afin que l'utilisateur puisse soit obtenir une solution sous-optimale dans un temps donné limite, ou attendre plus longtemps pour obtenir la solution optimale garantie.
Oui et non. Il est beaucoup plus rapide que les implémentations naïves, suffisamment rapide pour être utilisé sur des problèmes du monde réel, mais plus lent que les solveurs de haut niveau, hautement optimisés et de pointe.
Gophersat n’a pas pour objectif d’être le solveur SAT/PB le plus rapide disponible. Le but est de donner accès aux technologies SAT et PB aux gophers, sans recourir à des interfaces vers des solveurs écrits dans d'autres langages (typiquement C/C++).
Cependant, dans certains cas, l’interface avec un solveur écrit dans un autre langage constitue le meilleur choix pour votre application. Si vous avez beaucoup de petits problèmes à résoudre, Gophersat sera l’alternative la plus rapide. Pour les problèmes plus importants, si vous souhaitez avoir le moins de dépendances possible au détriment du temps de résolution, Gophersat est également une bonne solution. Si vous avez besoin de résoudre des problèmes difficiles et que cela ne vous dérange pas d'utiliser cgo ou d'utiliser un programme externe, Gophersat n'est probablement pas la meilleure option.
Il existe quelques autres solveurs SAT dans Go, principalement go-sat et gini. Les performances de Gini sont à peu près comparables à celles de Gophersat, bien qu'un peu plus lentes en moyenne, selon les tests que nous avons effectués.
Gophersat fournit également des fonctionnalités intéressantes qui ne sont pas toujours disponibles avec d'autres solveurs (un format d'entrée convivial, par exemple), il peut donc être utilisé comme un outil pour décrire et résoudre des problèmes NP-difficiles qui peuvent facilement être réduits à un SAT/PB. problème.
Non. Le package bf (pour « formule booléenne ») fournit des fonctionnalités permettant de traduire n'importe quelle formule booléenne en CNF.
C'est ce qu'on appelle le comptage de modèles, et oui, il existe une fonction pour cela : solver.Solver.CountModels .
Vous pouvez également compter les modèles depuis la ligne de commande, avec
gophersat --count filename
où le nom de fichier peut être un fichier .opb ou .cnf.
