Abstrakt. Propositionell modellräkning (#SAT), dvs. att räkna antalet tillfredsställande uppdrag av en propositionell formel, är ett problem av betydande teoretiskt och praktiskt intresse. På grund av problemets inneboende komplexitet föreslogs ungefärlig modellräkning, som räknar antalet tillfredsställande uppdrag inom given tolerans- och konfidensnivå, som ett praktiskt alternativ till exakt modellräkning. Ändå har ungefärlig modellräkning i huvudsak endast studerats teoretiskt. Det enda rapporterade genomförandet av ungefärlig modellräkning, på grund av Karp och Luby, fungerade endast för DNF formler. Några få befintliga verktyg för CNF-formler begränsar modellräknare; de kan hantera realistiska problemstorlekar, men inte ge räkningar inom given tolerans och förtroende, och därmed är inte ungefärliga modellräknare. Vi presenterar här en ny algoritm, samt en referensimplementation, som är den första skalbara approximativa modellräknaren för CNF-formler. Algoritmen fungerar genom att utfärda ett polynomtal samtal till en SAT-lösare. Vårt verktyg, CaMC, skalar till formler med tiotusentals variabler. Noggranna experimentella jämförelser visar att CaMC rapporterar, med stort förtroende, gränser som ligger nära den exakta räkningen, och också lyckas rapportera gränser med liten tolerans och högt förtroende i fall som är för stora för beräkning exakta modell räknas.
Med utgångspunkt i Bellare, Goldreich och Petrank (2000) föreslog REF den första skalbara ungefärliga modellen för att räkna algoritmer för promotionella formler, CaMC.
A Scalable Approximate Model Counter
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Mathematics', 'Computer Science']}