Rozpoczęcie pracy z rozwiązaniami SAT

24

Chcę zrobić pierwszy solver SAT. Znam konkurs SAT i konferencję SAT i jest tak wiele artykułów na ten temat. Jestem starterem, przytłoczonym starterem. Od czego powinienem zacząć W końcu chcę wprowadzić najnowocześniejsze rozwiązania. Chcę porady ekspertów, jak zacząć, żeby nie marnować czasu na rzeczy nieistotne zbyt wcześnie. Wielkie dzięki.

Zirui Wang
źródło
6
Czy już zaimplementowałeś algorytm DPLL? Czy dopracowałeś i dopracowałeś swoją implementację, aby działała wyjątkowo szybko?
Jukka Suomela,
5
Podręcznik satysfakcji - amazon.co.uk/… (być może sprawdź bibliotekę, koszt jest dość wysoki).
MGwynne
1
@Jukka: komentarz -> odpowiedź?
Suresh Venkat
4
Nie zgadzam się z Jukką. Po co wymyślać koło ponownie? Nie ma powodu, aby przerabiać to, co MiniSAT już zapewnia open source. Jeśli jesteś zainteresowany dodaniem do frameworka CDCL, twój dodatek pokaże zwiększoną wydajność MiniSAT. Również sam DPLL nie wystarczy; wprowadzono wiele ulepszeń. Zasadniczo podążaj za odpowiedzią Mikolasa!
Huck Bennett
1
Zobacz także powiązane pytanie cstheory.stackexchange.com/q/1988
András Salamon

Odpowiedzi:

18

Doskonały przegląd dla początkujących znajduje się w następującym artykule z 2009 roku.

Istnieje kilka sposobów na przejście do aspektów technicznych. Możesz nawet zacząć od oryginalnego papieru Davisa-Putnama. Jest to bardzo jasne i zawiera szczegółowe przykłady. Podczas omawiania optymalizacji SAT na kursie odkryliśmy, że niektórzy mogą sobie wyobrazić, że już tam są. Artykuł Davisa-Logemana-Lovelanda jest (wydaje mi się) mniej pouczający, ale jest tak krótki, że równie dobrze możesz go przeczytać.

Istnieją sposoby na nadrobienie zaległości w ciągu następnych 50 lat. Polecam slajdy z wykładów. Samo wyszukanie „DPLL” spowoduje wiele wielu samouczków. Jeśli je przejrzysz, jestem pewien, że mgła zniknie - do pewnego stopnia. Istnieje również wiele przydatnych ankiet. Artykuł Zhang-Malika to dobry początek. W Podręczniku satysfakcji znajduje się kilka artykułów, które mogą okazać się przydatne.

Popieram sugestię Mikolaos. Kod MiniSAT jest czysty i ma rozsądny rozmiar. Możesz z tym grać. Istnieje kilka innych rozwiązań, które możesz wypróbować. CryptoMiniSat jest również dość czysty. Powinieneś także skonsultować pracę Armina Biere'a , który pisze solvery SAT i pisze o pisaniu solverów SAT.

Vijay D.
źródło
17

Sugeruję najpierw zrozumieć, które techniki naprawdę rozwinęły solwery, dla których proponuję następujący przegląd i analizę .

Następnie polecam pobranie kodu źródłowego minisat i przeczytanie jego opisu .

Oczywiście może to być sprawa indywidualna, ale uważam, że przeglądanie kodu źródłowego jest najcenniejsze.

Mikolas
źródło
9

Jeśli jesteś przytłoczony całą pracą, dlaczego nie zaczniesz udawać, że nikt wcześniej nie pracował nad tym problemem? Jeśli Twoim celem jest zbudowanie konkurencyjnego rozwiązania SAT, będzie to dość długa podróż. Zaczynając od zabawy bez „sprawdzania rozwiązań”, że tak powiem, masz więcej do zyskania niż do stracenia.

nmnm

nm

James King
źródło
9

Zacznij od dobrej pracy ankietowej. Łatwo jest zaatakować przedmiot fragmentarycznie i pomylić różne nazwy w literaturze dla tych samych technik i tej samej nazwy używanej dla różnych technik. Łatwo jest również odtworzyć stare bitwy algorytmiczne (listy wystąpień vs. listy główek do głów vs. dwa oglądane literały dla implementacji DPLL), jeśli nie wiesz, jaki jest obecny stan techniki.

Solvers Satisfiable Gomes, i in. glin. da ci szorstkie ukształtowanie ziemi.

Ulepszanie solverów SAT przy użyciu najnowocześniejszych technik Manthey zbliży Cię do teraźniejszości.

Kyle Jones
źródło