Książka z przepisami dla kodowań SAT?

Solwery SAT stają się coraz bardziej wydajne w rozwiązywaniu dużych instancji i są używane jako zaplecze w różnych kontekstach. Za każdym razem, gdy chce się ich użyć do rozwiązania problemu w określonej domenie, musi wymyślić kodowanie ad-hoc, które nie tylko ma odpowiedni zestaw rozwiązań, ale także nakłada ograniczenia (nawet nadmiarowe) w formie który pomaga heurystykom solverów w szybszym znalezieniu rozwiązania.

Wydaje mi się, że wiele takich kodowań byłoby bardzo powszechnych, na przykład: twierdzenie, że skończony zestaw węzłów jest połączony jako drzewo lub jako DAG, lub lista jest sortowana ...

Czy istnieje repozytorium / książka kucharska z typowymi kodowaniami typowych problemów ze zoptymalizowanymi rozwiązaniami?

Kilka lat temu przeczytałem artykuł ankietowy, który wydaje się istotny, „ Udane techniki kodowania SAT ” Magnusa Björka.

Abstrakcyjny:

W tym artykule określono dobre praktyki kodowania SAT, analizując wywiady z wieloma znanymi ekspertami SAT. Celem jest zarówno określenie zaufania do różnych strategii kodowania poprzez analizę, czy eksperci są zgodni, czy też nie, a także dostarczenie ukrytej wiedzy użytkownikom SAT.

Panuje zgoda, że ​​techniki kodowania zwykle mają dramatyczny wpływ na wydajność solvera SAT, że znalezienie dobrego kodowania często wymaga dużo pracy, a rozmiar szyfrowania jest bardzo luźno związany z trudnością znalezienia rozwiązania . Tematy, w których rozmówcy się nie zgadzają, obejmują możliwość włączenia arytmetyki do problemów SAT i sformułowania problemów jako klauzul lub obwodów.

W artykule opisano szereg strategii, które sprawdzają się w różnych sytuacjach, takich jak różne sposoby przedstawiania liczb i sposób wykorzystania przyrostowości.

Zawsze dobrze jest najpierw zapoznać się z Podręcznikiem satysfakcji [1] (przepraszam, nie jest dostępny bezpłatnie). Tutaj rozdział 2 nosi tytuł „Kodowania CNF”. Przynajmniej książka zawiera odniesienia do literatury na temat aktualnego stanu wiedzy w momencie pisania, a dzięki nim możesz rozszerzyć swoje wyszukiwanie.

Ponadto tutaj i tutaj są dwa najnowsze slajdy na temat wstępnego przetwarzania SAT. Slajdy dają zwięzły przegląd technik wstępnego przetwarzania, a także dalsze odniesienia. Chodzi o to, że zamiast próbować „ręcznie” modelować problem w efektywny sposób, po prostu modelujesz go w najprostszy sposób, naciskasz go, a oprogramowanie zapewnia wydajne kodowanie.

[1] Biere, Armin, Marijn Heule i Hans van Maaren, red. Podręcznik satysfakcji. Vol. 185. IOS Press, 2009.

nie do końca bezpośrednia odpowiedź, ale inny, coraz bardziej zbliżony do siebie kąt: niektóre z nich są objęte stosunkowo nowym obszarem badań znanym jako SMT, Teorie Modulo Satisfiable . podstawową ideą jest połączenie kodowania problemów (np. arytmetyki liczb całkowitych, wykresów itp.) w solver SAT, ale także wykorzystanie / wykorzystanie dodatkowej wiedzy, która pochodzi z tego sprzężenia, aby zbudować bardziej zaawansowane algorytmy rozwiązania. Oto ankieta. jak wskazano, mogą być znacznie wydajniejsze niż łączenie mechanizmu kodowania ad-hoc ze standardowymi rozwiązaniami SAT.

• Teorie satysfakcji Modulo: Przekąska / Leonardo de Moura i Nikolaj Bjørner

  Teorie satysfakcji Modulo (SMT) polegają na sprawdzeniu, czy formuły logiczne spełniają jedną lub więcej teorii. Problem opiera się na połączeniu niektórych najbardziej podstawowych dziedzin informatyki. Łączy problem logicznej satysfakcji z domenami, takimi jak te badane w optymalizacji wypukłej i manipulowaniu symbolicznymi systemami symbolicznymi. Opiera się również na najbardziej płodnych problemach logiki symbolicznej w ostatnim stuleciu: problem decyzyjny, kompletność i niekompletność teorii logicznych, a na końcu teoria złożoności. Problem modułowego łączenia algorytmów specjalnego przeznaczenia dla każdej domeny jest tak głęboki i intrygujący, jak znalezienie nowych algorytmów, które działają szczególnie dobrze w kontekście kombinacji. SMT odgrywa również bardzo przydatną rolę w inżynierii oprogramowania. Nowoczesne oprogramowanie, analiza sprzętu i narzędzia oparte na modelach są coraz bardziej złożonymi i wielowymiarowymi systemami oprogramowania. Jednak ich rdzeniem jest niezmiennie komponent wykorzystujący logikę symboliczną do opisywania stanów i transformacji między nimi. Dobrze dostrojony solver SMT, który uwzględnia najnowocześniejsze przełomy, zwykle skaluje rzędy wielkości poza niestandardowymi rozwiązaniami ad-hoc.