Teoretyczne wyjaśnienia praktycznego sukcesu solverów SAT?

Jakie są teoretyczne wyjaśnienia praktycznego sukcesu solverów SAT i czy ktoś może dać przegląd i wyjaśnienie w stylu „wikipedii” łącząc je wszystkie?

Analogicznie, wygładzona analiza ( wersja arXiv )) dla algorytmu simplex świetnie się tłumaczy, dlaczego działa tak dobrze w praktyce, mimo że w najgorszym przypadku zajmuje on czas wykładniczy i jest NP-potężna ( wersja arXiv ).

Słyszałem trochę o takich rzeczach, jak backdoory, struktura wykresu klauzulowego i przejścia fazowe, ale (1) nie widzę, jak wszystkie one pasują do siebie, aby dać większy obraz (jeśli tak) i (2) Nie wiem, czy to naprawdę wyjaśnia, dlaczego solwery SAT działają tak dobrze, na przykład w instancjach przemysłowych. Ponadto, jeśli chodzi o takie elementy, jak struktura grafu klauzulowego: dlaczego obecne solwery mogą korzystać z niektórych struktur grafu klauzulowego?

Uważam, że wyniki dotyczące przemian fazowych są częściowo satysfakcjonujące pod tym względem, przynajmniej w moim obecnie ograniczonym rozumieniu. Literatura dotycząca przemian fazowych dotyczy przypadków losowego k-SAT, ale czy to naprawdę tłumaczy coś na temat rzeczywistych przypadków? Nie oczekuję, że rzeczywiste instancje SAT będą wyglądać jak instancje losowe; Czy powinienem? Czy istnieje powód, aby sądzić, że przejścia fazowe mówią nam coś, nawet intuicyjnie, o instancjach w świecie rzeczywistym, nawet jeśli nie wyglądają one jak instancje losowe?

Powiązane pytania, które pomagają, ale nie odpowiadają w pełni na moje pytanie, w szczególności prośba o połączenie rzeczy w spójny obraz:

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

• Które problemy z SAT są łatwe?

• Jaka jest korelacja między wysokością a twardością instancji z losowego 3SAT?

Zakładam, że masz na myśli solwery CDCL SAT w zestawach danych testowych, takich jak te używane w konkursie SAT . Programy te oparte są na wielu heurystykach i wielu optymalizacjach. Było kilka bardzo dobrych wprowadzeń do ich pracy na warsztatach Theoretical Foundations of Applied SAT Solving w Banff w 2014 roku ( filmy ).

Algorytmy te opierają się na algorytmie śledzenia wstecznego DPLL, który próbuje znaleźć satysfakcjonujące przypisanie poprzez ustawienie wartości zmiennych i cofanie się, gdy znajdzie konflikt. Ludzie sprawdzili, jak duży wpływ mają te heurystyki. Np. Patrz

• Hadi Katebi, Karem A. Sakallah i Joao P. Marques-Silva, „ Empirical Study of Anatomy of Modern Sat Solvers ”, 2011

Wydaje się, że wydajność tych solverów SAT w testach porównawczych wynika głównie z dwóch dwóch heurystyk (i ich wariantów):

1. Jutowa jodła VSIDS wybiera, która zmienna ma rozgałęzić się na następnej.
2. CDCL: heurystyczna nauka klauzuli opartej na konflikcie, która uczy się nowej klauzuli z konfliktu.

Powszechnie wiadomo, że dowody DPLL odpowiadają dowodom w rozdzielczości. Bez CDCL jedynymi dowodami rozdzielczości, które możemy uzyskać, są dowody rozdzielczości drzewa, które są znacznie słabsze niż ogólne dowody rozdzielczości.

Istnieją wyniki, które pokazują, że dzięki CDCL możemy uzyskać dowolny dowód ogólnej rozdzielczości. Jednak istnieją pewne zastrzeżenia, wymagają one wielu sztucznych restartów, sztucznych rozgałęzień i / lub szczególnego przetwarzania wstępnego, więc nie jest jasne, jak blisko są one do tego, co te programy robią w praktyce. Aby uzyskać więcej informacji, patrz np. Następujący papier:

• Paul Beame i Ashish Sabharwal, „ Nie restartujące się solwery SAT z prostym przetwarzaniem wstępnym mogą skutecznie symulować rozdzielczość ”, 2014

CDCL zasadniczo wycina gałęzie z przestrzeni wyszukiwania. Istnieją różne sposoby wyprowadzenia nowej wyuczonej klauzuli z konfliktu. Idealnie byłoby dodać zestaw minimalnych klauzul, które sugerowałyby konflikt, ale w praktyce mogą być duże i kosztowne do obliczenia. Najlepsze solwery SAT często usuwają wyuczone klauzule regularnie, co pomaga w praktyce.

Drugi heurystyczny VSIDS zasadniczo utrzymuje wynik dla każdej zmiennej. Za każdym razem, gdy występuje konflikt, wszystkie wyniki są korygowane poprzez pomnożenie ich przez wartość <1 i dodanie stałej do tych, które były „zaangażowane” w konflikt. Aby zobaczyć, co to znaczy, pomyśl o sekwencji która wynosi 1, jeśli zmienna v była „zaangażowana” w ty konflikt. Niech będzie stałą. Wynik zmiennej w czasie wynosi wtedy: F ( v , i $\alpha$$F(v,i)$0 < α < 1 v n ∑ i < n F ( v , i ) α ( n - i $i$$0<\alpha<1$$v$$n$

Intuicyjnie można powiedzieć, że stara się to podkreślić zmienne, które konsekwentnie były zaangażowane w ostatnie konflikty. Możesz również myśleć o tym jako o prostym, ale wyjątkowo tanim sposobie przewidywania, które zmienne będą zaangażowane w następnym konflikcie. Więc VSIDS rozgałęzia się najpierw na tych zmiennych. Można twierdzić, że algorytm jest zasadniczo algorytmem odpornym na awarie, szybko znajduje konflikty. Szybka jest związana z mniejszą liczbą zestawów zmiennych, co oznacza blokowanie dużych poddrzewa drzewa wyszukiwania. Ale jest to głównie intuicja, ponieważ nikt nie sformalizował tego bardzo ostrożnie, aby przetestować go na zestawach danych SAT. Uruchomienie solvera SAT na jednym z tych zestawów danych nie jest tanie, nie mówiąc już o porównaniu go z optymalnymi decyzjami (najmniejsze rozszerzenie bieżącego przypisania do zmiennych, które naruszałoby jedną z klauzul). VSIDS zależy również od tego, które zmienne napotykamy podczas każdego konfliktu, istnieją różne sposoby określania, kiedy zmienna jest zaangażowana w konflikt.

Istnieją wyniki, które pokazują, że konkretna implementacja tych pomysłów odpowiada ważonej czasowo centralności wierzchołków na wykresach dynamicznych.

Istnieją również sugestie, że wykluczając przypadki przeciwne, takie jak te oparte na problemach trudnych dla NP, krypto-prymitywy i przypadki losowe (w których solvery CDCL SAT nie są dobre), pozostałe przypadki pochodzą z bardzo dobrze ustrukturyzowanych rzeczy, takich jak weryfikacja oprogramowania i sprzętu, i w jakiś sposób te struktury są wykorzystywane przez solwery CDCL SAT (wspomniano wiele pomysłów, takich jak backdoory, zamrożone zmienne itp.), ale afaik są głównie pomysłami i nie mają mocnych dowodów teoretycznych ani eksperymentalnych na ich poparcie. Myślę, że należałoby dokładnie zdefiniować poprawnie i pokazać, że instancje, w których te algorytmy działają dobrze, mają właściwość, a następnie pokazać, że algorytmy te wykorzystują te właściwości.

Niektórzy twierdzą, że wskaźnik klauzul i progi są jedyną grą w mieście. Jest to zdecydowanie nieprawda, ponieważ wiedziałby każdy, kto jest nieco obeznany z działaniem przemysłowych solverów SAT lub ma wiedzę na temat złożoności dowodów. Istnieje wiele rzeczy, które sprawiają, że solver SAT działa dobrze lub nie w danej instancji w praktyce, a współczynnik klauzul jest tylko jedną z rzeczy, które mogą być zaangażowane. Myślę, że poniższe badanie jest dobrym punktem wyjścia do poznania związków między złożonością dowodu a rozwiązaniami SAT i perspektywą:

• Jakob Nordstrom, „ O wzajemnym oddziaływaniu złożoności dowodu i rozwiązywania problemów SAT ”, 2015

Co ciekawe, nawet zjawisko progowe jest bardziej skomplikowane, niż myśli większość ludzi, Moshe Vardi stwierdził w swoim przemówieniu „ Przejścia fazowe i złożoność obliczeniowa ”, że mediana czasu działania GRASP pozostaje wykładnicza dla losowych wzorów 3SAT po progu, ale wykładnik maleje (afaik, nie jest jasne, jak szybko maleje).

Dlaczego badamy solwery SAT (jako teoretycy złożoności)? Myślę, że odpowiedź jest taka sama jak w przypadku innych algorytmów: 1. porównaj je, 2. znajdź ich ograniczenia, 3. projektuj lepsze, 4. odpowiedz na podstawowe pytania teorii złożoności.

Podczas modelowania heurystyki często zastępujemy heurystykę niedeterminizmem. Powstaje zatem pytanie, czy jest to „sprawiedliwy” zamiennik? I tutaj przez uczciwość mam na myśli, jak bliski jest model, pomagając nam odpowiedzieć na powyższe pytanie.

Kiedy modelujemy solver SAT jako system sprawdzający, częściowo pokazujemy to ograniczenie, ponieważ algorytm będzie nieskuteczny dla instrukcji, które mają niższe granice w systemie sprawdzającym. Ale nadal istnieje luka między tym, co algorytm faktycznie znajduje, a optymalnym dowodem w systemie dowodu. Musimy więc pokazać, że również odwrotnie, tj. Algorytm może znaleźć dowody, które są tak dobre, jak te w systemie dowodów. Nie jesteśmy bliscy odpowiedzi na to pytanie, ale ilość heurystyki, którą zastępuje niedeterminizm, określa, jak blisko model jest do systemu dowodu. Nie oczekuję, że całkowicie porzucimy zastąpienie heurystyki niedeterminizmem, w przeciwnym razie uzyskalibyśmy wyniki automatyzacji, które miałyby konsekwencje dla otwartych problemów w kryptografii itp.

Pytanie, kiedy patrzy się na model, brzmi: w jaki sposób modele pomagają wyjaśnić, dlaczego solver SAT A jest lepszy od SAT solver B? Jak bardzo pomagają w tworzeniu lepszych rozwiązań SAT? Czy solver SAT znajduje w praktyce dowody zbliżone do optymalnych dowodów w modelu? ... Musimy również modelować praktyczne przykłady.

Jeśli chodzi o intuicję, że solwery CDCL SAT „wykorzystują strukturę praktycznych instancji” (cokolwiek to jest), ogólnie uważam, że intuicja jest akceptowana. Prawdziwym pytaniem jest przekonujące wyjaśnienie, co to oznacza, i wykazanie, że jest to prawda.

Zobacz także własną odpowiedź Jakoba Nordstroma, aby uzyskać najnowsze informacje.

Piszę to dość szybko z powodu poważnych ograniczeń czasowych (i nawet nie dostałem wcześniej odpowiedzi z tego samego powodu), ale pomyślałem, że spróbuję przynajmniej wpłacić moje dwa centy.

Myślę, że to naprawdę świetne pytanie i spędziłem niemiłe ilości czasu w ciągu ostatnich kilku lat, zastanawiając się nad tym. (Pełne ujawnienie: Otrzymałem dużą część mojego obecnego finansowania właśnie po to, aby spróbować znaleźć odpowiedzi na tego typu pytania, a następnie potencjalnie przekształcić głębsze wgląd w SAT w bardziej wydajne rozwiązania SAT.)

Myślę, że gdyby ktoś musiał udzielić odpowiedzi w jednym zdaniu

nikt tak naprawdę nie wie i jest to aktywny obszar badań

jest prawie tak dobry, jak to tylko możliwe. Tyle, że jest o wiele więcej miejsca na większą aktywność, szczególnie od strony teorii.

Niektóre proponowane wyjaśnienia (nie wykluczające się wzajemnie), które zostały już omówione w innych odpowiedziach i komentarzach, są

• a) tylne drzwi,
• (b) sparametryzowane względy złożoności,
• (c) struktura graficzna problemu CNF,
• (d) względy złożoności dowodu oraz
• (e) przejścia fazowe.

Począwszy od końca (e), wydaje się, że istnieje pewne zamieszanie dotyczące przejść fazowych. Krótka odpowiedź tutaj jest taka, że ​​nie ma żadnego powodu, aby sądzić, że stosunek klauzul do zmiennych jest istotny dla zastosowanych problemów lub teoretycznych problemów kombinatorycznych (czyli spreparowanych przypadków). Ale z jakiegoś powodu nie jest zbyt rzadkim nieporozumieniem w stosowanej części społeczności SAT, że stosunek klauzul do zmiennych powinien w jakiś sposób być ogólnie istotną miarą. Stosunek klauzuli do zmiennej jest bardzo istotny dla losowego k-SAT, ale nie dla innych modeli.

Mam wrażenie, że tylne drzwi (a) były popularnym wytłumaczeniem, ale osobiście tak naprawdę nie widziałem przekonujących dowodów, które wyjaśniają, co dzieje się w praktyce.

Sparametryzowana złożoność (b) zapewnia piękną teorię na temat niektórych aspektów SAT, a bardzo atrakcyjną hipotezą jest to, że instancje SAT są łatwe, ponieważ mają tendencję do „zbliżania się do jakiejś wyspy wykonalności”. Myślę, że ta hipoteza otwiera wiele ekscytujących kierunków badań. Jak zauważono w niektórych odpowiedziach, istnieje wiele powiązań między (a) i (b). Jednak do tej pory nie widzę żadnych dowodów na to, że sparametryzowana złożoność zbyt mocno koreluje z tym, co dzieje się w praktyce. W szczególności wydaje się, że możliwe do wykonania instancje mogą być bardzo trudne w praktyce, a instancje bez małych tylnych drzwi mogą być bardzo łatwe.

Wyjaśnienie, które wydaje mi się najbardziej wiarygodne dla instancji przemysłowych, to (c), a mianowicie, że struktura (graficzna) omawianych wzorów CNF powinna być skorelowana z praktyczną wydajnością SAT. Chodzi o to, że zmienne i klauzule instancji przemysłowych mogą być grupowane w dobrze połączone społeczności z kilkoma połączeniami między nimi, a solwery SAT w jakiś sposób wykorzystują tę strukturę. Niestety, bardziej rygorystycznie wydaje się to dość trudne i równie niestety w tym obszarze występuje spory szum. Proponowane wyjaśnienia, które do tej pory widziałem w dokumentach, są dość niezadowalające, a modele wydają się łatwe do zestrzelenia. Problemem wydaje się być to, że jeśli ktoś naprawdę chce to zrobić dokładnie, wtedy matematyka staje się naprawdę trudna (ponieważ jest to trudny problem), a także staje się wyjątkowo nieuporządkowana (ponieważ potrzebujesz modelu, który jest wystarczająco blisko rzeczywistości, aby uzyskać odpowiednie wyniki). W szczególności artykuły, które widziałem wyjaśniające, że wydajność heurystyk VSIDS (suma rozpadu niezależna od stanu zmiennego) dla zmiennych wyborów działa dobrze, ponieważ bada społeczności na graficznej reprezentacji instancji są dość nieprzekonujące, chociaż hipoteza jako taka jest nadal aktualna bardzo atrakcyjny.

Jedną z linii badań, które osobiście przeprowadziłem, jest to, czy praktyczna wydajność SAT w jakiś sposób koreluje z miarami złożoności dowodowej omawianych wzorów CNF. Niestety wydaje się, że krótka odpowiedź brzmi, że tak naprawdę nie ma wyraźnego i przekonującego związku. Być może nadal istnieją nietrywialne korelacje (jest to coś, co obecnie badamy na różne sposoby), ale wydaje się, że teoria jest zbyt ładna, czysta i ładna, a rzeczywistość jest zbyt niechlujna, aby można było naprawdę dobrze dopasować. (Odnosząc się do artykułu dotyczącego miar złożoności dowodu i twardości praktycznej SATJärvisalo, Matsliah, Nordström i Živný w CP '12 okazało się, że bardziej szczegółowe eksperymenty dostarczają o wiele bardziej złożony obraz z mniej jasnymi wnioskami --- mamy nadzieję uzyskać pełną wersję czasopisma informującą o tym w każdej dekadzie, ale jest to skomplikowane, choć mam nadzieję, że interesujące.)

Kolejną, pokrewną linią prac nad złożonością dowodu jest modelowanie supernowoczesnych solverów SAT jako systemów dowodu i dowodzenie twierdzeń w tych modelach w celu wywnioskowania właściwości odpowiednich solverów. Jest to jednak trochę pole minowe, ponieważ małe i pozornie nieszkodliwe wybory projektowe po stronie modelu teoretycznego mogą prowadzić do tego, że wyniki są praktycznie zupełnie nieistotne z praktycznego punktu widzenia. Z drugiej strony, jeśli ktoś chce modelu teoretycznego wystarczająco zbliżonego do rzeczywistości, aby uzyskać odpowiednie wyniki, wówczas model ten staje się wyjątkowo nieuporządkowany. (Wynika to z faktu, że wydajność solvera SAT zależy od globalnej historii wszystkiego, co do tej pory wydarzyło się w niebanalny sposób, a to oznacza, że ​​model nie może być modułowy w sposób, w jaki zwykle konfigurujemy nasze systemy dowodowe --- czy dany krok wyprowadzania jest "poprawny"

Dwa artykuły, które naprawdę należy wymienić jako wyjątki, to [Pipatsrisawat i Darwiche 2011] oraz [Atserias, Fichte i Thurley 2011], w których wykazano, że klauzula ucząca się o konfliktach, rozwiązująca modele SAT w naturalny sposób, ma: potencjał do wielomianowej symulacji pełnej, ogólnej rozdzielczości. Istnieje dość długa lista artykułów poprzedzających [PD11] i [AFT11], które zasadniczo twierdzą, że ten sam wynik, ale wszystkie mają poważne problemy z modelowaniem. (Prawdą jest, że [PD11] i [AFT11] również potrzebują pewnych założeń do działania, ale są to właściwie te minimalne, których można się spodziewać, chyba że poprosisz o dokumenty, które pokazałyby również, że sparametryzowana hierarchia złożoności ulega załamaniu.)

Ponownie piszę to wszystko bardzo szybko, ale jeśli istnieje jakiekolwiek zainteresowanie powyższym, mógłbym spróbować je rozwinąć (chociaż może to chwilę potrwać, aby wrócić do tego ponownie - nie wahaj się ze mną pingować, jeśli tam jest) to wszystko, co chciałbyś, żebym skomentował). Jako szybki sposób na dostarczenie referencji, pozwól mi zrobić kilka bezwstydnych wtyczek (chociaż wstyd nieco się zmniejsza, gdy widzę, że niektóre komentarze cytowały również niektóre z tych referencji):

Dyskusja Tutorial stylu Na interakcji pomiędzy Dowód złożoność i SAT Rozwiązywanie podano w Międzynarodowej Szkole Letniej na spełnialności teorie spełnialności Modulo i Automated rozumowanie w 2016 roku z dużą ilością pełnych odniesień na końcu zjeżdżalni: http://www.csc .kth.se / ~ jakobn / research / TalkInterplaySummerSchool2016.pdf

Nieco nowsza i krótsza dyskusja w ankiecie Zrozumienie rozwiązywania problemów opartych na konflikcie SAT dzięki obiektywowi złożoności dowodu od początku 2017 r. (Również z pełnymi referencjami na końcu): http://www.csc.kth.se/~jakobn/research /TalkProofComplexityLensCDCL1702.pdf

Badanie związków między złożonością dowodu a rozwiązywaniem SAT: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Odniesienia bibliograficzne: Jakob Nordström. O wzajemnym oddziaływaniu złożoności dowodu i rozwiązywania problemów SAT. ACM SIGLOG News, tom 2, numer 3, strony 19-44, lipiec 2015. (Wersja lekko edytowana z poprawionymi literówkami.)]

Artykuł SAT '16 z CDCL wiernie modelowanym jako system dowodowy: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [Odniesienia bibliograficzne: Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard , Jakob Nordström i Marc Vinyals. Kompromisy między czasem a pamięcią w ściślejszym modelu solverów CDCL SAT. W materiałach z 19. Międzynarodowej Konferencji Teorii i Zastosowań Testów Satysfakcji (SAT '16), Wykład Notatki z informatyki, tom 9710, strony 160-176, lipiec 2016 r.]

Dodaję do tego moje dwa centy zrozumienia, mimo że nigdy tak naprawdę nie pracowałem w tej dziedzinie.

Zadajesz jedno z dwóch pytań: „jakie są wszystkie znane podejścia do udowodnienia teoretycznej wydajności jakiegoś solwera SAT dla niektórych rodzajów instancji” i „dlaczego solwery SAT są skuteczne w rzeczywistości”.

W przypadku pierwszego pytania skieruję cię do badań Stefana Szeidera. Wydaje mi się, że jest obecnie najbardziej aktywnym obszarem w temacie parametryzacji backdoorów i FPT SAT (który obejmuje zarówno podejścia strukturalne, takie jak miary typu treewidth i tak zwane zestawy backdoor, a także pewną ich kombinację).

Jeśli chodzi o to drugie pytanie, szczerze mówiąc, dokładnie to pytanie było dyskutowane na każdym warsztacie poświęconym rozwiązywaniu problemów SAT, w którym uczestniczyłem (w tym w ostatnich latach), więc nie jest to ustalone. Ale moje wrażenie jest następujące.

Przede wszystkim musisz określić ilościowo lub ograniczyć to, co rozumiesz przez „w rzeczywistości”. Nie jest prawdą, że solwery SAT są uniwersalnie dobrymi rozwiązaniami dla każdego problemu, na który je rzucasz (oczywiście), a między różnymi problemami ostatecznie potrzebujesz różnych strategii. Na przykład, istnieje kilka ostatnich sukcesów, w których domysły matematyczne zostały zweryfikowane lub zaostrzone przez ogromne wyszukiwanie komputerowe wspomagane przez solvery SAT. Najwyraźniej w tym przypadku sprytne ulepszenia i heurystyki w stylu CDCL, które zwykle stosują współczesne solwery SAT, nie kupują zbyt wiele mocy, a gra sprowadza się do sprytnego sposobu podzielenia problemu źródłowego na części, po których następuje (zasadniczo) algorytm rozgałęzienia siły brutalnej z małym stałym współczynnikiem czasu działania.

Być może nieco przesadziłem z tym punktem, ale miałem na myśli to, że gdy solwery SAT zaatakowały na przykład hipotezę rozbieżności Erdosa, odniosły sukces z innego powodu niż w przypadku rozwiązywania instancji przemysłowych pochodzących z testowania obwodu.

Musimy więc zapytać, dlaczego solwery oparte na CDCL działają tak dobrze w instancjach przemysłowych, na przykład w przypadku weryfikacji obwodu (testowanie równoważności obwodu)? I pomyślećże najpotężniejszym poglądem (lub poglądem konsensusowym) jest tutaj strategia wyszukiwania solversów CDCL bardzo dobrze ze strukturą tych instancji. Oznacza to na przykład, że obwody składają się ze stosunkowo złożonych części (nazywają je klastrami), połączonych ze sobą przez relatywnie mniejszą liczbę prostszych połączeń, być może w sposób hierarchiczny; oraz że solwery CDCL z całą swoją heurystyką są bardzo dobre w (de facto) wykorzystywaniu tego i „rzutowaniu” tych klastrów na zmienne współdzielone, w dowolny sposób lub kolejność, które są najbardziej przydatne do weryfikacji dostępnego obwodu. Wydaje się jednak, że nadal jest to konsensus, że jest to niewystarczające wyjaśnienie (np. Prawdopodobnie nie jesteśmy w stanie teoretycznie wyjaśnić wydajności solverów CDCL SAT w tej dziedzinie wyłącznie poprzez odwołanie się do struktury graficznej instancji).

Czy więc możliwa do parametryzacji parametryzacja przyczynia się do wyjaśnienia tego ostatniego? Szczerze mówiąc, nie wiem. Myślę, że w grze jest prawdopodobnie potężny efekt, że rzeczywiste przypadki nie są najgorszymi przypadkami, ani też (prawdopodobnie) naprawdę przeciętnymi przypadkami, zgodnie z rozkładem instancji, którym jesteśmy w stanie poradzić. Ale prawdopodobnie nadal warto o to zapytać.

Istnieje artykuł „ Relating Proof Complexity Measures and Practical Hard of SAT ” Matti Järvisalo, Arie Matsliah, Jakob Nordström i Stanislav Živný w CP '12, który próbuje powiązać twardość lub łatwość rozwiązywania niektórych formuł przez solvery CDCL z dowodem rozdzielczości miary złożoności, w szczególności przestrzeń próbna rozdzielczości. Wyniki są nieco mieszane, ale myślę, że jest to krok we właściwym kierunku.

Nie jestem ekspertem w tej dziedzinie, ale myślę, że losowe przejścia z fazy SAT / fazy są mniej lub bardziej całkowicie niezwiązane z aplikacjami przemysłowymi / praktycznymi.

Np. Bardzo dobre solwery dla przypadkowych instancji (takie jak https://www.gableske.net/dimetheus ) oparte są na metodach fizyki statystycznej (propagacja przekonań itp.), Podczas gdy bardzo dobre „ogólne” solwery (takie jak ponieważ http://fmv.jku.at/lingeling/ ) używają niepowiązanych technik (bardziej jak to, o czym mówił Kaveh), wierzę.

Ale, jak powiedziałem, może nie wierz mi na słowo; pochodzi od określonego nie-eksperta.