Je pense à démarrer un cluster de serveurs qui fonctionnera exclusivement Z3 pour résoudre les formules SMT.Distribué Z3 et meilleur matériel pour chaque nœud
Existe-t-il un moyen de regrouper plusieurs serveurs pour rejoindre la puissance de calcul et résoudre les formules SMT de manière distribuée? Quelles sont les caractéristiques de recommandation d'un système qui exécutera Z3 pour être le plus rapide possible (en ce qui concerne le matériel)?
Merci!
Les solveurs SAT/SMT sont généralement très lourds en mémoire en raison des faibles résultats de cache. Par conséquent, vous ne pouvez pas exécuter beaucoup de processus sur un processeur, sinon ils commenceront bientôt à dégrader les performances les uns des autres (c'est-à-dire, exécuter un processus par cœur n'est pas une bonne idée si vous voulez benchmark).
Je ne peux donner aucune recommandation spécifique, mais je choisirais des processeurs qui ont moins de cœurs (disons 4) et de bande passante élevée. De nos jours, les processeurs ont un TDP fixe et moins les processeurs sont puissants, et moins de conflits pour la mémoire.
Vous voulez également vous en tenir aux architectures little-endian. À l'heure actuelle, Z3 ne joue pas bien avec les archers big-endian (tels que de nombreux ARM, MIPS, SPARC, etc). En outre, pour ce que j'ai vu, 64 bits aide habituellement.
Merci. Savez-vous si je peux utiliser Z3 de manière distribuée? merci – user1618465
vous ne pouvez pas. Il existe cependant un mode parallèle (avec OpenMP), mais les accélérations peuvent aller de <1 à quelques%, selon le type de problèmes que vous voulez résoudre. Ne vaut pas la peine si vous avez assez de problèmes pour garder vos machines occupées. –