Dlaczego wszystkie najnowsze solwery SAT działają na CNF zamiast na obwodzie SAT?

Po wydaniu biblioteki AIGER do obsługi wykresów i inwerterów w pewnym momencie w 2006 r. (Tak mi się wydaje), niektóre solvery z obwodami SAT zostały wydane w latach 2006-2008, a na kilku wyścigach / konkursach SAT były ścieżki AIG. Jednak od tego czasu wydaje się, że skupiono się całkowicie na SMT lub ulepszaniu klauzulowych solverów SAT.

Intuicyjnie dla mnie koncentrowanie się na obwodzie SAT wydaje się mieć sens: wiele, jeśli nie większość problemów, jest wyrażonych bardziej naturalnie jako obwód SAT niż CNF; obwody dostarczają informacji strukturalnych, których nie można poddać inżynierii odwrotnej z CNF, ale obwody można zawsze przekształcić w CNF; a przynajmniej znacząca przemysłowo dziedzina syntezy logicznej wydaje się szczególnie dobrze dopasowana do AIG.

Więc co się stało? Czy okazało się, że dodatkowe informacje strukturalne nie pomagają rozwiązującym? Czy system SAT oparty na AIG rozwiązał nieudany eksperyment?

twoje pytanie ma wiele różnych kątów. ogólnie zgodził się z twoim założeniem, że spojrzenie na „informacje strukturalne” w sformułowaniu SAT powinno być doskonałym obszarem badawczym.

• Kodowanie SAT w CNF jest standardem od dziesięcioleci. został zestalony na początku do połowy lat 90. XX wieku dzięki formatowi / konkursom DIMACS .

• czym technicznie są „informacje strukturalne”? formalne utrwalenie tej koncepcji i uniknięcie kręgów prawie tautologicznych może być trudne. tak naprawdę nie ma żadnej różnicy między kodowaniem SAT CNF a innymi kodowaniami, które zachowują strukturę sieci. jest to zawarte w pojęciach „klauzula / wykres zmienny”, z których korzysta wiele solverów SAT. innymi słowy, w pewnym sensie, każdy znaczący solver SAT używa „informacji strukturalnych” .

• tak, nowsze kierunki badań skupiły się na rozwiązywaniu ASP i SMT, które prawie w rzeczywistości zawierają „informacje strukturalne”, o które pytasz.

• Transformacja tseytiny z łatwością przekształca obwód w SAT w czasie / przestrzeni P w celu wprowadzenia do standardowego solvera SAT. jest przypuszczalnie szeroko stosowany w wielu kontekstach, zwłaszcza w kontekstach obwodów EE.

• istnieje kilka raczej odizolowanych badań, które są podobne do tych, o których wspomniałeś, ale niestety (ponownie wraz z twoją przesłanką) nigdy nie wydawały się zbytnio rozwijać w trend badawczy. nie sądzę, że wynika to z braku potencjału, ale z większej liczby czynników ludzkich. dwa ulubione artykuły [1] [2], innym jest przyjrzenie się poszczególnym instancjom z dziedzin takich jak „instancje przemysłowe” lub „elektrotechnika”, o których prowadzone są specjalistyczne badania.

• Puryści z CS czasami starają się unikać rozważań psychologicznych / socjologicznych we wszystkich abstrakcjach matematycznych, ale rozsądnie jest to nadal czynnik w informatyce . pytasz o trendy badawcze oparte na ludzkich czynnikach psychologicznych. możliwe, że dzieje się tutaj efekt oświetlenia ulicznego , czyli „nisko wiszący owoc”. można powiedzieć / wziąć pod uwagę, że nawet kilka lat temu, badania algorytmiczne SAT są w powijakach, tak że duże pytania, takie jak P vs NP, wydają się nigdzie niewidoczne, a być może istniejące badania, choć wciąż znaczące, wciąż „drapią powierzchnię” .

[1] Rozkładanie problemów związanych z satysfakcją lub Korzystanie z wykresów w celu uzyskania lepszego wglądu w problemy dotyczące satysfakcji , Herwig 2006 (83pp)

[2] Ostrze ograniczające Walsh 1998