Pobieranie #SAT Solver

21

Czy ktoś mógłby wskazać jedną lub więcej stron internetowych, z których można pobrać działającą implementację solvera #SAT? Interesują mnie osoby zwracające dokładną liczbę rozwiązań, a nie przybliżenie.

ds.algorithms sat software Giorgio Camerani
źródło
2
Cześć Walter, twoje pytanie jest blisko granicy tego, co byłoby oficjalnie „na temat” dla tej strony. Jeśli jednak nie masz gdzie zadać tego pytania, a my możemy na nie odpowiedzieć, być może nie jest tak źle ... (Ponieważ strona jest wciąż w fazie rozwoju, myślę, że jesteśmy bardziej otwarci niż inne strony). że celem tego komentarza nie jest „besztanie” ani „ostrzeganie”, to jest po prostu przyjazne powiadomienie.
Ryan Williams
Cześć Ryan, dziękuję za powiadomienie. Przepraszam, jeśli to pytanie jest blisko granicy. Szukałem w Internecie i nic nie znalazłem: tylko niektóre solvery SAT, ale żadnych solverów #SAT. Właśnie dlatego zapytałem tutaj. Oczywiście wiem, że potrafię napisać własny kod, który wykorzystuje solver SAT jako silnik do liczenia rozwiązań, ale szukałem czegoś, co już jest gotowe i gotowe do użycia.
Giorgio Camerani,
12
Chciałbym się nie zgodzić Myślę, że takie pytania są w zasięgu i powinny być!
Suresh Venkat
uzgodnić jego zakres. fyi / imho nie jest zbyt praktyczne budowanie solvera #SAT z solvera SAT, chyba że ma się kod źródłowy, a nawet w takim przypadku nie jest tak praktyczny, z wyjątkiem bardzo małych formuł, ze względu na bardzo zły wykładniczy wybuch. zwykle wymagane są specjalne techniki unikalne dla #SAT, a nie SAT ...
dniu

Odpowiedzi:

16

Możesz to zrobić za pomocą SAT4J , po prostu iterując wszystkie modele: http://www.sat4j.org/howto.php#models . Wyobrażam sobie, że większość solverów SAT ma tę zdolność.

Dave Clarke
źródło
Cześć supercooldave, dzięki za twój wskaźnik. Nie wiedziałem, że SAT4J ma tę zdolność.
Giorgio Camerani,
16

Możesz także wypróbować solver #SAT „sharpSAT” ( strona internetowa , github ) do zliczania liczby spełniających wymagania formuł CNF.

Holger
źródło
11

Jedną z opcji jest użycie biblioteki BDD, takiej jak JavaBDD . Wszystkie takie biblioteki mają albo funkcję, która szybko liczy rozwiązania, albo przynajmniej ułatwiają napisanie takiej funkcji. Wadą jest jednak to, że konstruowanie BDD będzie w wielu przypadkach powolne i może wymagać dużej ilości pamięci.

mnO(mn)∼m+n

Radu GRIGore
źródło
7

Temat pokrewny: Najlepszy SAT Solver .

MS Dousti
źródło
1
Dzięki Sadeq. Wskazany temat wydaje się teoretyczny. Wymienia kilka dokumentów na temat zmniejszania górnej granicy. To bardzo interesujące, ale szukałem gotowej do użycia implementacji.
Giorgio Camerani,
2
Proszę bardzo Wśród cytowanych tam linków był jeden, który był czysto praktyczny: satcompetition.org . Myślę, że można tam znaleźć bardzo dobre wdrożenia.
MS Dousti,
7

Najlepsze, co znalazłem, to „kompilator c2d”. http://reasoning.cs.ucla.edu/c2d/

Używa d-DNNF i potrzebujesz opcji -count .

Leon Leon
źródło
c2d rozwiązuje znacznie więcej CNF niż sharpsat. Dla zabawek celów „relsat” sat solver zrobi też.
Leon Leon
7

MBound Solver podany tutaj http://www.cs.cornell.edu/~sabhar/ może dawać liczby modeli z gwarancjami probabilistycznymi. Jest to znacznie szybsze niż wyliczenie wszystkich rozwiązań.

Optować
źródło
5

Napisałem mały model / główny wylicznik implikujący . Można to już wykorzystać do zliczania modeli z wyliczeniem modelu, ale nie jest to zbyt praktyczne. Jeśli ktoś jest zainteresowany, mogę go rozszerzyć, aby liczył modele z najlepszych implantów.

Mikolas
źródło
2

Witryna BeyondNP zawiera dobry spis istniejących narzędzi do rozwiązywania #SAT (i innych powiązanych trudnych problemów dotyczących formuł CNF). Możesz także znaleźć listę narzędzi do przybliżonego zliczania modeli i kompilacji wiedzy (zadanie przekształcenia CNF w miejmy nadzieję zwięzłą strukturę danych, która często obsługuje zliczanie wielomianowe modelu czasowego).

Możesz także znaleźć listę narzędzi do wstępnego przetwarzania formuł CNF, które mogą być przydatne do poprawy wydajności liczników modeli i różnych testów porównawczych .

holf
źródło