J'ai un simple ensemble de contraintes qui Z3 est pas en mesure de faire face à:Z3 retourne inconnu
est-il un moyen de modifier les contraintes afin d'obtenir le résultat? Ceci est un exemple simple d'un plus grand ensemble de contraintes (milliers) mais Je suis en quelque sorte troublé qu'il ne fonctionne pas même sur un tel exemple simple
Merci d'avance !!
Votre problème comporte des contraintes non linéaires. Alors que Z3 peut les traiter dans la plupart des cas, le mélange de Int s et Real semble le mettre au-delà de ses capacités actuelles. Si vous utilisez simplement Real s pour vos variables s_0_1, s_0_2 etc, je crois que Z3 sera en mesure de résoudre le problème. (Vous semblez avoir assez de contraintes de valeur, donc je crois qu'il n'y aura pas de problème de modélisation.)
Je pense que Leonardo a exprimé plusieurs fois que les prochaines versions auront un meilleur support pour les théories combinées en présence de non-linéaire. contraintes.
Levent est correct, le problème est l'utilisation d'un nombre entier mixte et d'une arithmétique non linéaire réelle. Je vois deux solutions de contournement possibles. Nous pouvons remplacer toutes les variables entières par des variables réelles, cela est correct, car les variables entières peuvent seulement supposer des valeurs 0 ou 1 dans votre problème (voici la solution: http://rise4fun.com/Z3Py/ICFA). Dans ce cas, le nouveau solveur nlsat de Z3 sera utilisé. Une autre option consiste à remplacer les variables entières par des variables booléennes et à linéariser le problème en utilisant 'If's. Voici le lien pour cette solution http://rise4fun.com/Z3Py/egCe. La deuxième solution devrait mieux évoluer. –