Rozpoczęcie pracy z rozwiązaniami SAT

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.

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

• Boolean Satisfability: od teoretycznej twardości do praktycznego sukcesu , Sharad Malik, Lintao Zhang, Communications of the ACM, 2009

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ć.

• Procedura obliczeniowa dla teorii kwantyfikacji , Martin Davis, Hilary Putnam, Journal of the ACM, 1960.
• Program maszynowy do dowodzenia twierdzeń , Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.

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.

• W poszukiwaniu wydajnych logicznych solverów satysfakcji , Lintao Zhang, Sharad Malik, Wspólny dokument z zaproszeniem dla CAV i CADE 2002.
• Handbook of Satisfiable , pod redakcją Armin Biere, Marijn Heule, Hansa van Maarena i Toby'ego Walsha, 2009
• Anatomia i ocena empiryczna współczesnych solverów SAT , Karem Sakallah, Joao Marques-Silva, Biuletyn EATCS, 2011.

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.

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.

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.

$n$$m$$n$$m$

$n$$m$

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.