Comment un solveur SMT / SAT génère des évaluations pour cet exemple

Question

Tout d'abord, un exemple d'un ensemble de contraintes qui se sont avérés ne pas être résolubles (je ne pense pas):

b < 3 && c + a > 5 && a - b > 2 && c > 1 && b - c > 3

Ma procédure pour résoudre ceci est à peu près: OK OK est inférieur à 3, et C> 1. 1 + A> 5, donc A> 4 dans ce cas. Essayez 4 - 2> 2, non cela ne fonctionne pas, alors peut-être que A est 5, 5 - 2> 2. puis b - c> 3. 2 - 2> 3. Non, donc b doit B supérieur à 3, mais Nous savons que B est inférieur à 3, donc il ne peut pas être résolu.

Puis un exemple plus simple qui peut être résolu.

b < 3 && c + a > 5 && a - b > 2

Alors disons que B est 2. Alors A - 2> 2, alors dites que A est 5. alors C + 5> 5, alors disons C est également 1. Alors a = 5, b = 2, c = 1 résout le problème.

Dans cet exemple, j'ai choisi des nombres qui étaient près de la frontière, en ce qu'ils étaient "juste au-dessus" de la limite inférieure dans la partie>. Mais vous pourriez dire que A est 100 et C est 100. C'est également un exemple particulièrement facile.

Ma question est de savoir comment un solveur de contraintes résout ce problème. J'ai lu sur SAT et SMT, et je n'ai pas encore lu le livre sur les procédures de décision. Cependant, je comprends que les solveurs SAT résolvent les systèmes d'équations booléennes de deux manières: (1) en renvoyant oui / non que le système peut être résolu, ou (2) en attribuant évaluations à chaque variable du système afin qu'il satisfait les contraintes. Je ne sais pas comment ils font cela. Je comprends également que les solveurs SMT sont essentiellement une couche légère au-dessus des solveurs SAT. Ils vous permettent d'avoir des formules booléennes plus riches en utilisant différentes «théories» (telles que la théorie de l'égalité, la théorie des réels, des entiers, des listes, etc.). Ensuite, vous pouvez éventuellement définir comment fusionner ces théories afin que vous puissiez appliquer le solveur SAT sur une expression compliquée impliquant par exemple les réels, les entiers, l'égalité, les booléens et les listes ou les tableaux en même temps. Pour moi, cela semble évident, pourquoi le solveur de contraintes ne fonctionnerait-il pas simplement sur des fonctions et des variables arbitraires, mais je manque probablement quelque chose.

J'aimerais savoir comment implémenter quelque chose comme z3. Je suppose que chaque théorie spécifique (comme le Théorie des cordes) est assez compliqué, donc je ne voulais pas demander comment résoudre génériquement tous les différents types de contraintes. Au lieu de cela, je voulais poser une question simplifiée en utilisant des contraintes de base entières afin que je puisse apprendre les principes fondamentaux du fonctionnement d'un solveur SMT / SAT.

En tant que tel, la question est essentiellement juste, comment un solveur de contraintes résout le deuxième exemple ci-dessus. Un ou deux des algorithmes qu'il pourrait utiliser pour le faire. Plus précisément, je voudrais savoir comment donner à une fonction un ensemble de contraintes et faire en sorte que les évaluations de toutes les variables me redonnent toutes les variables. À cet égard, la question implique également comment le solveur de contraintes choisit ou décide de l'ensemble des valeurs. Je l'ai vu dire qu'il était aléatoire, mais je voudrais éviter cette approche si possible. Mais de toute façon, quand il choisit une valeur, se demandant comment il sait, il en a obtenu un valide. S'il doit recomputer toutes les contraintes à chaque fois, il fait une supposition ou peut faire une sorte d'optimisation. Fondamentalement, le fonctionnement du solveur SAT / SMT.

Pour rester simple, je ne cherche pas une explication complète de la façon dont tous les aspects de la résolution du problème fonctionnent. Juste plus une introduction de haut niveau aux algorithmes et comment ils sont en train de sélectionner les valeurs et de retourner l'évaluation. Une fois que je comprends que je pense que la compréhension des théories les plus compliquées comme la théorie des chaînes aura plus de sens.

Je demande parce que je ne peux pas dire sur la base de ma lecture jusqu'à présent si tout se résume vraiment à appliquer des contraintes dans un solveur SAT, et il y a peut-être 1 ou 2 algorithmes de résolution SAT (DPLL et CDCL que je me familiarise) Pour les contraintes booléennes (plus peut-être quelques autres pour générer les données de test pour résoudre les contraintes). Ou suis-je tort là-bas, et il y a une couche entière de recherches en plus de cela (sur SMT Solvers) où les procédures de décision personnalisées sont les algorithmes que vous souhaitez utiliser, et il y en a des centaines et il n'y a pas de modèle standard pour eux. Dans ce cas, je continue à avoir du mal à imaginer comment il est possible de résoudre un système de contraintes comme celui ci-dessus, ou quelque chose de plus compliqué avec les contraintes de chaîne (correspond à Regex) et d'autres contraintes qui nécessitent des fonctions complexes (comme quelque chose est la version inverse ou triée de autre chose). S'il y a autant de variabilité, l'idée de résoudre des contraintes semble difficile.

Fondamentalement, ce que je recherche, c'est une description d'un la mise en oeuvre. J'ai lu de nombreux articles jusqu'à présent, mais ils ont été pour la plupart trop élevés pour l'appliquer.