FR
Un échantillonneur GPU trouve des entrées de circuit valides en parallèle
SAT Sampling at Scale via GPU-based Boolean Constraint Propagation · arXiv:2610.28805
En termes simples
Pour tester un circuit, il faut trouver des configurations d’entrée valides qui lui font produire les sorties souhaitées, y compris celles que des entrées aléatoires atteignent rarement. Cet article présente Gpap-S, un échantillonneur sur GPU qui essaie en parallèle de nombreuses affectations aléatoires et ne conserve que celles qui aboutissent en respectant les règles du circuit.
Dans les tests sur plusieurs collections de circuits, Gpap-S a produit des échantillons plus vite que les échantillonneurs GPU à gradient comparés pour les cibles rares. Demotic n’a produit aucun échantillon dans cinq de ses sept instances testées à cible rare.
Un test statistique distinct a accepté Gpap-S sur 65 instances conservées ; c’est un indice fourni par ce test, pas une garantie d’uniformité parfaite.
La recherche
La vérification des circuits exige des entrées valides qui conduisent une conception aux sorties souhaitées, y compris des configurations rares que les entrées aléatoires atteignent peu souvent.
Un GPU peut-il en générer beaucoup sans perdre des échantillons utiles lorsque les méthodes fondées sur le gradient arrondissent leurs résultats en affectations booléennes ?
Gpap-S échantillonne des entrées de circuit valides en lançant en parallèle sur GPU de nombreuses tentatives aléatoires de propagation et en conservant les affectations qui aboutissent.
Gpap-S lance sur GPU de nombreuses tentatives aléatoires de choix de variables et de propagation, abandonne les contradictions et conserve les affectations satisfaisantes qui aboutissent. Ses échantillons sont ainsi valides sans arrondi ni correction.
Dans les lignes rapportées selon les ensembles de circuits, les cibles et les profondeurs, Gpap-S affichait des débits d’échantillonnage en régime établi supérieurs à ceux de CMSGen, l’échantillonneur sur CPU.
Ses débits dépassaient aussi ceux des échantillonneurs GPU à gradient comparés pour les cibles rares, mais ces comparaisons portaient sur la collection de circuits propre à chaque outil et ne comptaient que les instances où les deux outils ont produit des échantillons.
Les résultats proviennent d’un ensemble limité de tests de circuits et comparent les outils avec le matériel, les réglages et les règles de chronométrage indiqués. Barbarik a accepté Gpap-S sur 65 instances conservées, mais ce résultat statistique ne garantit pas formellement que ses échantillons sont uniformes.
Ce que montrent les preuves
- Le problème des entrées rares
L’article présente Gpap-S, une méthode sur GPU qui échantillonne des entrées valides pour des circuits. La question est de savoir comment générer de nombreuses entrées satisfaisantes, y compris celles qui conduisent à des sorties rares.
Les échantillonneurs SAT sur CPU peuvent trouver des affectations valides, tandis que les échantillonneurs GPU à gradient peuvent perdre des résultats utiles lorsque peu d’affectations arrondies satisfont une cible rare.
- Un autre échantillonneur GPU
Gpap-S s’appuie sur Gpap, un moteur qui propage de nombreuses affectations partielles indépendantes sur une même formule. À chaque tentative, il attribue des valeurs à des variables et en suit les conséquences.
Les affectations qui aboutissent satisfont la formule et deviennent des échantillons ; les tentatives qui aboutissent à une contradiction sont abandonnées. Chaque échantillon produit est ainsi valide, sans arrondi ni correction d’affectation.
- Des débits supérieurs à ceux de CMSGen
Dans les comparaisons avec CMSGen, l’échantillonneur sur CPU, Gpap-S affichait un débit soutenu d’échantillons par seconde supérieur dans les lignes rapportées pour les ensembles de circuits, les cibles et les profondeurs.
Les deux outils recevaient le même circuit et la même profondeur, et disposaient d’un budget d’échantillonnage de 60 secondes. Toutefois, l’encodeur de Gpap-S répétait la simplification du circuit et ajoutait ensuite une étape dc2.
Gpap-S fonctionnait sur GPU et CMSGen sur un cœur de CPU. Les moyennes par ligne ne comprennent que les instances où les deux outils ont produit des échantillons.
- Cibles rares et qualité des échantillons
Les comparaisons avec les échantillonneurs GPU à gradient portaient sur la collection de circuits propre à chaque outil. Pour les cibles d’origine, Gpap-S affichait des débits rapportés supérieurs ; pour les cibles rares, son avantage sur Recurrent était plus grand, tandis que Demotic n’a produit aucun échantillon dans cinq de ses sept instances à cible rare.
Un test statistique a aussi accepté Gpap-S et CMSGen dans les 65 instances conservées. Cette acceptation renseigne sur la qualité des échantillons selon les critères du test, mais ne prouve pas leur uniformité.
- Le travail abandonné limite les gains
L’avantage de débit a un coût pour les cibles rares des circuits séquentiels. Gpap-S abandonne les tentatives contradictoires sans en tirer de nouvelles clauses, et peut donc effectuer beaucoup plus de travail de propagation par échantillon produit que CMSGen, qui apprend des contradictions et revient en arrière.
Les auteurs ont mesuré un travail supérieur d’un facteur de 6,41 et de 6,59 à celui de CMSGen par échantillon, respectivement à 25 et 50 cycles. Ces lignes correspondent aussi aux gains de vitesse mesurés les plus faibles de Gpap-S face à CMSGen.
Détails
- Auteurs de l’article original
- Alexander Nadel, Yogev Shalmon, Ofer Strichman
- Soumis à arXiv
- Licence
- CC BY 4.0