Clarification types SMT ; erreur dans la troncature de variable ? ; autoriser Bool*Int

Question

Je ai les questions suivantes:

A. Si je ai une variable x que Je déclare (cas 1) à être Bool (cas 2) à être Int et affirmer x=0 ou x=1 (cas 3) à être Int et affirmer 0<=x<=1. Que se passe-t-il dans Z3, ou plus généralement dans SMT, dans chacun des cas? Est-ce que (cas 1) désiré puisque les choses se produisent au niveau SAT et non SMT? Avez-vous une référence papier ici?

B. J'ai l'énoncé suivant en Python (pour utiliser l'API Python Z3)

    tmp.append(sum([self.a[i * self.nrVM + k] * componentsRequirements[i][1] for i 
    in range(self.nrComp)]) <= self.MemProv[k])

où a est déclaré comme une variable Z3 Int (0 ou 1), componentsRequirements est une variable Python qui doit être considérée comme un flottant, self.MemProv est déclarée comme une variable Z3 Real.

La chose étrange est que pour des valeurs flottantes pour componentsRequirements, par exemple 0.5, la contrainte construite par le solveur le considère comme 0 et non 0.5. Par exemple dans:

    (assert (<= (to_real (+ 0 (* 0 C1_VM2)
            (* 0 C2_VM2)
            (* 2 C3_VM2)
            (* 2 C4_VM2)
            (* 3 C5_VM2)
            (* 1 C6_VM2)
            (* 0 C7_VM2)
            (* 2 C8_VM2)
            (* 1 C9_VM2)
            (* 2 C10_VM2)))
StorageProv2))

le 0 ci-dessus devrait en réalité être 0.5. En changeant a en une valeur Réel alors les flottants sont considérés, mais cela est admis par nous à cause de la sémantique de a. J'ai essayé d'utiliser la commutativité entre a et componentsRequirements mais sans succès.

C. Si je veux utiliser x comme type Bool et le multiplier par un Int, je obtiens, bien sûr, une erreur (Bool*Real/Int non autorisé), dans Z3. Y a-t-il un moyen de surmonter ce problème en gardant les types des deux multiplicateurs? Un exemple en ce sens est le ci-dessus (a - Bool, componentsRequirements - Real/Int): a[i * self.nrVM + k] * componentsRequirements[i][1]

Merci

Answer 1

Je ne peux honnêtement pas répondre pour z3 en particulier, mais je tiens à exprimer mon opinion sur le point A).

En général, la contrainte x=0 v x=1 est abstraite en t1 v t2, où t1 est x=0 et t2 est x=1, au niveau du moteur SAT.

Ainsi, le moteur SAT pourrait essayer d'assigner à la fois t1 et t2 à true lors de la construction d'une assignation de vérité satisfaisable pour la formule d'entrée. Il est important de noter que c'est une contradiction dans la théorie du LAR, mais le moteur SAT n'est pas capable d'un tel raisonnement. Par conséquent, le moteur SAT pourrait continuer sa recherche un moment après avoir pris cette décision.

Lorsque le solveur LAR est enfin invoqué, il va détecter l'insatisfaction du LAR de l'assignation de vérité donnée (éventuellement partielle). En conséquence, il (doit) transmettre la clause not t1 or not t2 au moteur SAT en tant que clause d'apprentissage afin de bloquer la mauvaise assignation de valeurs afin qu'elle ne soit pas générée à nouveau.

S'il y a beaucoup de telles mauvaises assignations, il peut être nécessaire d'appeler plusieurs fois le solveur LAR afin de générer toutes les clauses de blocage nécessaires pour rectifier l'assignation de vérité SAT, éventuellement jusqu'à une pour chacune de ces mauvaises combinaisons.

À la réception de la clause de conflit, le moteur SAT devra faire un retour arrière à l'endroit où il a fait la mauvaise assignation et prendre la bonne décision. De toute évidence, tout le travail effectué par le moteur SAT depuis qu'il a fait la mauvaise assignation de valeurs ne sera pas perdu : toute clause utile apprise entre-temps sera sûrement réutilisée. Cependant, cela peut encore entraîner une baisse notable des performances sur certaines formules.

Comparez toute cette computation en va-et-vient gaspillée avec le simple fait de déclarer x comme un Booléen : maintenant le moteur SAT sait qu'il ne peut lui assigner qu'une des deux valeurs, et ne lui assignera jamais x et non x simultanément.

Dans cette situation spécifique, on pourrait atténuer ce problème en fournissant les clauses de blocage nécessaires directement dans la formule d'entrée. Cependant, il n'est pas trivial de conclure que c'est toujours la meilleure pratique : énumérer explicitement toutes les clauses de blocage connues pourrait entraîner une explosion de la taille de la formule dans certaines situations, et une dégradation encore pire des performances en pratique. Le meilleur conseil est d'essayer différentes approches et de faire une évaluation expérimentale avant d'opter pour un encodage particulier d'un problème.

---

Clause de non-responsabilité : il est possible que certains solveurs SMT soient plus intelligents que d'autres, et génèrent automatiquement des clauses de blocage appropriées pour les variables 0/1 lors de l'analyse de la formule ou évitent cette situation complètement par d'autres moyens (c'est-à-dire, d'après ce que je sais, les solveurs SMT basés sur des modèles ne devraient pas rencontrer le même problème)

Answer 2

Concernant A

Patrick a donné une explication claire pour celui-ci. En pratique, vous devez vraiment essayer et voir ce qui se passe. Différents problèmes peuvent présenter différents comportements en fonction du moment où / comment les heuristiques entrent en jeu. Je ne pense pas qu'il y ait de règle générale ici. Ma préférence personnelle serait de conserver les booléens en tant que booléens et de les convertir si nécessaire, mais cela relève principalement d'une perspective de programmation / maintenance, et non d'efficacité.

Concernant B

Votre problème de "truncation" de votre "division" est très probablement le même que celui-ci : Récupérer une valeur dans Z3Py donne un résultat inattendu

Vous pouvez être explicite et écrire 1.0/2.0, etc.; ou utiliser :

 from __future__ import division

en haut de votre programme.

Concernant C

SMTLib est un langage fortement typé ; vous ne pouvez pas multiplier par un booléen. Vous devez d'abord le convertir en nombre. Quelque chose comme (* (ite b 1 0) x), où b est votre booléen. Ou vous pouvez écrire une fonction personnalisée qui le fait pour vous et appeler celle-ci à la place ; quelque chose comme :

(define-fun mul_bool_int ((b Bool) (i Int)) Int (ite b i 0))
(assert (= 0 (mul_bool_int false 5)))
(assert (= 5 (mul_bool_int true 5)))