Z3 donne une réponse différente à chaque fois en réordonnant les paramètres. Problème d'optimisation

Question

Chaque fois que je lance mon projet, un ordre différent des formules Z3 est généré. Même si la formule est exactement la même, elle est réorganisée dans les différentes exécutions et, par conséquent, les réponses obtenues de Z3 sont différentes à chaque exécution. Cela pose des problèmes car j'ai besoin d'un ensemble optimal qui devrait être exactement le même à chaque exécution.

Par exemple,

1. la première manche est :

   (declare-const l1 ( BitVec 1)) (declare-const l2 ( BitVec 1)) (declare-const l3 ( BitVec 1)) (declare-const l4 ( BitVec 1)) (declare-const l5 ( BitVec 1)) (declare-const l6 ( BitVec 1)) (declare-const l7 ( BitVec 1)) (declare-const l8 ( BitVec 1)) (declare-const l9 ( BitVec 1)) (declare-const l10 ( BitVec 1))

   (minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

   (maximize (bvand (bvor (bvand l3 l4 l1 l2) (bvand l4 l2) (bvand l4 l1 l2) (bvand l2 l3 l4))

       (bvor (bvand l4 l2) (bvand l2 l3 l4)) 
   
       (bvor (bvand l5 l7 l8 l10 l6) (bvand l5 l7 l8 l6) (bvand l5 l7 l8 l9 l6) (bvand l5 l7 l8 l9 l10 l6) (bvand l5 l7 l6) (bvand l5 l7 l9 l10 l6) (bvand l5 l7 l10 l6))
   )

   ) (check-sat) (get-model)

ce qui donne la solution : l7 , l5 , l2 , l4 , l6 , l8 .
6 sont vraies dans ce cas.

2. la deuxième course est :

   (declare-const l1 ( BitVec 1)) (declare-const l2 ( BitVec 1)) (declare-const l3 ( BitVec 1)) (declare-const l4 ( BitVec 1)) (declare-const l5 ( BitVec 1)) (declare-const l6 ( BitVec 1)) (declare-const l7 ( BitVec 1)) (declare-const l8 ( BitVec 1)) (declare-const l9 ( BitVec 1)) (declare-const l10 ( BitVec 1))

   (minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

   (maximize (bvand (bvor (bvand l2 l3 l4) (bvand l2 l4) (bvand l1 l2 l4) (bvand l2 l3 l4 l1))

       (bvor (bvand l2 l3 l4) (bvand l2 l4)) 
   
       (bvor (bvand l10 l6 l5 l7 l9) (bvand l10 l6 l5 l7) (bvand l10 l6 l5 l7 l8 l9) (bvand l10 l6 l5 l7 l8) (bvand l7 l6 l5) (bvand l7 l8 l9 l6 l5) (bvand l7 l8 l6 l5))
   )

   )

   (check-sat) (get-model)

ce qui donne la solution : l7 , l9 , l5 , l2 , l4 , l6 , l8 , l3 .
8 sont vraies dans ce cas.

Pour mon projet, j'ai besoin d'un ensemble optimal et minimisé. J'ai besoin que le plus petit nombre possible de variables soit vrai, en fonction des conditions expliquées précédemment. Pour ces deux séries, la réponse correcte et optimale devrait être : l2 , l4 , l5 , l6 , l7 (5 vrais). En fait, j'ai besoin de minimiser le coût et de satisfaire les conditions à l'intérieur de l'objet de l'analyse. maximize condition.

Cependant, au lieu de toujours donner la solution optimale avec 5 variables vraies, j'obtiens soit 6, 8, 10 valeurs vraies.
J'ai aussi essayé (assert (= (bvand ...) #b1) ) à la place de (maximize (bvand ...) ) en vain.

Comment puis-je obtenir le nombre minimum, optimal, de variables vraies qui satisfasse également la condition et donne le même résultat à chaque fois, même en cas de réorganisation ?

note : Je ne peux pas utiliser Int ou Bool car mes programmes vont probablement être énormes et int/bool ne pourrait pas les gérer.

Answer 1

Il y a plusieurs problèmes ici. Tout d'abord, vous minimisez la somme en utilisant bvadd qui effectue l'arithmétique de la machine. C'est-à-dire qu'il débordera de la taille du vecteur de bits. (C'est-à-dire que la valeur est soit 0 soit 1 à tout moment.) Pour éviter cela, faites l'addition sur une taille de vecteur de bits plus grande :

(define-fun ext ((x (_ BitVec 1))) (_ BitVec 8)
    ((_ zero_extend 7) x))

(minimize (bvadd (ext l1) (ext l2) (ext l3) (ext l4) (ext l5) (ext l6) (ext l7) (ext l8) (ext l9) (ext l10)))

Ici, j'ai étendu les valeurs à 8 bits avant de les ajouter : Puisque vous avez 10 variables, 8-bits est plus que suffisant pour représenter le total de 10 . (Vous pouvez également vous en sortir avec 4 bits dans ce cas, même si cela n'a pas beaucoup d'importance. Assurez-vous simplement qu'il est suffisamment large pour représenter le nombre total de variables que vous ajoutez).

Mais il y a un deuxième problème ici. Vous demandez à z3 de minimiser cette somme, puis de maximiser votre deuxième expression. Z3 fera une optimisation lexicographique, ce qui signifie qu'il traitera d'abord votre première contrainte, puis utilisera la seconde. Mais votre première contrainte fera en sorte que toutes les variables 0 pour minimiser la somme. Pour éviter cela, veillez à intervertir l'ordre des contraintes.

Et comme dernier commentaire : Vous avez explicitement dit que "note : je ne peux pas utiliser Int ou Bool car mes programmes vont probablement être énormes et int/bool serait incapable de le gérer." Je trouve cela très douteux. Pour un problème comme celui-ci, un Bool serait le choix le plus évident et optimal. En particulier, l'optimiseur aura beaucoup plus de facilité à traiter les booléens que les vecteurs de bits et les entiers. Je vous recommande donc de ne pas abandonner cette idée sans l'avoir expérimentée et sans avoir la preuve qu'elle n'est pas adaptée.