IT
Un sampler GPU trova in parallelo ingressi validi per i circuiti
SAT Sampling at Scale via GPU-based Boolean Constraint Propagation · arXiv:2610.28805
In parole semplici
Chi verifica un circuito ha bisogno di ingressi validi che gli facciano produrre uscite scelte, comprese quelle che gli ingressi casuali raggiungono di rado. Questo articolo presenta Gpap-S, un sampler su GPU che prova molte assegnazioni randomizzate in parallelo e conserva solo quelle completate che rispettano i vincoli del circuito.
Nei test sulle raccolte di circuiti, Gpap-S ha prodotto campioni più velocemente dei sampler a gradienti su GPU confrontati per gli obiettivi rari; Demotic non ne ha prodotti in cinque delle sette istanze rare testate. Un test statistico separato ha accettato Gpap-S su 65 istanze mantenute: è un’evidenza secondo i criteri del test, non una garanzia di uniformità perfetta.
La ricerca
La verifica dei circuiti richiede ingressi validi che portino un progetto a produrre uscite scelte, comprese quelle rare che gli ingressi casuali raggiungono di rado.
Una GPU può generare molti di questi ingressi validi senza perdere campioni utili, come può accadere quando i metodi basati sui gradienti arrotondano i risultati ad assegnazioni booleane?
Gpap-S campiona ingressi validi per i circuiti eseguendo in parallelo su GPU molti tentativi randomizzati di propagazione e conservando le assegnazioni completate.
Gpap-S esegue su GPU molti tentativi randomizzati di scelta e propagazione, scarta le contraddizioni e conserva le assegnazioni soddisfacenti completate come campioni. In questo modo produce risultati validi senza arrotondamenti o correzioni.
Nelle righe riportate per raccolta di circuiti, obiettivo e profondità, Gpap-S ha avuto velocità di campionamento a regime superiori a quelle del sampler su CPU CMSGen.
Le sue velocità hanno superato anche quelle dei sampler a gradienti su GPU confrontati per gli obiettivi rari, ma il confronto riguardava la raccolta di circuiti propria di ciascun sampler e includeva solo le istanze in cui entrambi i metodi hanno prodotto campioni.
I risultati provengono da un insieme circoscritto di test sui circuiti e confrontano gli strumenti con l’hardware, le impostazioni e le regole di misurazione dichiarati.
Barbarik ha accettato Gpap-S su 65 istanze mantenute, ma questo risultato statistico non fornisce una garanzia formale che i campioni siano uniformi.
Cosa mostrano le prove
- Il problema degli ingressi rari
L’articolo presenta Gpap-S, un metodo su GPU per campionare ingressi validi per i circuiti. La domanda è come generarne molti, compresi quelli che portano a uscite rare.
I sampler SAT su CPU possono trovare assegnazioni valide, mentre i sampler a gradienti su GPU possono perdere risultati utili quando poche assegnazioni arrotondate soddisfano un obiettivo raro.
- Un sampler GPU diverso
Gpap-S usa Gpap, un motore che propaga molte assegnazioni parziali indipendenti applicandole a un’unica formula condivisa. Per ogni tentativo assegna variabili e ne segue le conseguenze.
Le assegnazioni completate soddisfano la formula e diventano campioni; i tentativi che portano a una contraddizione vengono scartati. Così ogni campione prodotto è valido senza dover arrotondare o correggere un’assegnazione.
- Velocità superiori a CMSGen
Nei confronti con CMSGen, il sampler SAT su CPU, Gpap-S ha avuto velocità a regime più alte in campioni al secondo nelle righe riportate per raccolta di circuiti, obiettivo e profondità. Entrambi hanno ricevuto lo stesso circuito e la stessa profondità e hanno avuto un budget di campionamento di 60 secondi, ma il codificatore di Gpap-S ha ripetuto la semplificazione del circuito e aggiunto un passaggio dc2.
Gpap-S è stato eseguito su GPU e CMSGen su un singolo core CPU. Le medie per riga includono solo le istanze in cui entrambi gli strumenti hanno prodotto campioni.
- Obiettivi rari e qualità dei campioni
I confronti con i sampler a gradienti su GPU hanno usato le raccolte di circuiti proprie di ciascun metodo. Sugli obiettivi originali Gpap-S ha avuto velocità riportate più alte; sugli obiettivi rari, il vantaggio su Recurrent è stato maggiore, mentre Demotic non ha prodotto campioni in cinque delle sette istanze rare.
Un test statistico ha inoltre accettato sia Gpap-S sia CMSGen su tutte le 65 istanze mantenute. È un’evidenza sulla qualità dei campioni secondo i criteri del test, non una prova di uniformità.
- Il lavoro scartato limita i guadagni
Sugli obiettivi sequenziali rari, il vantaggio in velocità ha un costo. Gpap-S scarta i tentativi in conflitto senza apprendere da essi, quindi può spendere molto più lavoro di propagazione per ogni campione prodotto rispetto a CMSGen, che apprende dai conflitti e usa il backtracking.
Gli autori hanno misurato un lavoro pari a 6,41 e 6,59 volte quello di CMSGen per campione, rispettivamente a 25 e 50 cicli. In queste righe sono stati registrati anche i minori aumenti di velocità misurati per Gpap-S rispetto a CMSGen.
Dettagli
- Autori del paper originale
- Alexander Nadel, Yogev Shalmon, Ofer Strichman
- Inviato ad arXiv
- Licenza
- CC BY 4.0