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

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 ?

ds.algorithms 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

@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

Pytanie przeniesione z Crypto.SE crypto.stackexchange.com/questions/153/… .

— M. Alaggan

Odpowiedzi:

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

$A$ $X$ $Y$ $B$ $Y$ $X$

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.

$A$ $B$

— James King
źródło