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
źródło
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.
źródło
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.
źródło