Dlaczego istnieje ogromna różnica między rozwiązaniami SAT?

25

Rozwiązują SAT są bardzo ważne w algebraicznych ataków , na przykład walksat i minisat .

Jednak przy rozwiązywaniu problemów z testami porównawczymi dostępnymi tutaj istnieje ogromna różnica w wydajności między nimi - Walksat jest znacznie szybszy niż minisat dla tych problemów. Dlaczego to?

Ta implementacja walksata wydaje się mieć pewne ulepszenia wydajności - czy jest jakiś powód, dla którego nie została uwzględniona w międzynarodowych konkursach SAT ?

ir01
źródło
Twoje drugie pytanie, dlaczego dany algorytm został wykluczony z pewnej konkurencji, prawdopodobnie nie wchodzi w zakres tej witryny. Twoje pierwsze pytanie dotyczące tego, co sprawia, że ​​jeden algorytm jest często szybszy od drugiego, myślę, że to uczciwa gra, ale może potrzebować trochę przeredagowania, aby uczynić go bardziej przyjaznym dla teorii.
Lew Reyzin
Krótka uwaga: Minisat jest dość stary, nie wydaje się utrzymany i nie uczestniczył w konkursie. Co również rozumiesz przez „ogromny” i do którego utworu się odnosisz (losowo / crafted / application)?
Radu GRIGore
5
@Radu: MiniSAT 2.2.0 został wydany w lipcu 2010 roku. Nie powiedziałbym, że nie jest obsługiwany. Ponadto kod jest dość stabilny i czysty, więc rzadkie aktualizacje mogą nie stanowić problemu. Zgadzam się jednak, że nowsze solvery lepiej odzwierciedlają stan techniki.
Vijay D
1
Pytanie przeniesione z Crypto.SE crypto.stackexchange.com/questions/153/… .
M. Alaggan

Odpowiedzi:

33

Tak, istnieje zasadnicza różnica między MiniSAT a WalkSAT. Po pierwsze, wyjaśnijmy - MiniSAT jest specyficzną implementacją ogólnej klasy algorytmów DPLL / CDCL, które wykorzystują backtracking i uczenie się klauzul, podczas gdy WalkSAT to ogólna nazwa algorytmu na przemian między krokami chciwymi a krokami losowymi.

Zasadniczo DPLL / CDCL jest znacznie szybszy w przypadku ustrukturyzowanych instancji SAT, podczas gdy WalkSAT jest szybszy w przypadkowych k-SAT. Przemysłowe i stosowane instancje SAT mają zwykle dużą strukturę, więc DPLL / CDCL dominuje w większości współczesnych solverów SAT. Jednak instancja na instancję jedna technika może wygrać, co jest jednym z powodów, dla których solwery portfolio stały się popularne.

Mam duży problem z twoim twierdzeniem, że WalkSAT jest znacznie szybszy niż MiniSAT w instancjach na tej stronie. Po pierwsze, są tam gigabajty instancji SAT - na ilu próbujesz je porównać? WalkSAT wcale nie jest konkurencyjny w większości przypadków ustrukturyzowanych, dlatego nie jest często spotykany w zawodach.

Na marginesie - Vijay ma rację, że MiniSAT jest nadal aktualny. Faktycznie, ponieważ jest open source i dobrze napisany, MiniSAT jest solver pokonać w celu wykazania, że dana optymalizacja ma obietnicy. Wiele osób poprawia samą MiniSAT, aby zaprezentować swoje optymalizacje - spójrz na kategorię „MiniSAT hack” w ostatnich konkursach SAT.

Huck Bennett
źródło
17

AXYBYX

Dobrym artykułem do przeczytania na ten temat jest ten autorstwa Nudelman i in . Głównym celem artykułu jest określenie łatwych do obliczenia cech instancji SAT, które mogą powiedzieć, które algorytmy mogą działać dobrze, a które nie. Za pomocą tej techniki można zbudować algorytm oparty na portfolio, który szybko przeanalizuje wystąpienie problemu, a następnie rozwiąże wystąpienie za pomocą najbardziej odpowiedniego algorytmu. Następuje szereg dokumentów, które następują po tym; przeglądając SATzilla pojawi się wiele materiałów do czytania.

AB

James King
źródło