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.
ds.algorithms
reference-request
lo.logic
sat
Zirui Wang
źródło
źródło
Odpowiedzi:
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.
źródło
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.
źródło
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.
źródło
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.
źródło