Przegląd transformacji związanych z wykorzystaniem solverów SAT

13

Zaczynam badać możliwość polegania na rozwiązaniu SAT w celu rozwiązania problemu optymalizacji, który mnie interesuje, i obecnie szukam ankiety, która zawierałaby przykłady „sprytnych” przekształceń w warianty SAT (tj. Przekształcenia, które wynikają w problemie o rozsądnej wielkości, ponieważ nie jestem zainteresowany udowodnieniem wyników twardości, ale faktycznym rozwiązaniem problemu), w przybliżeniu w duchu tego, co można znaleźć w ankiecie na grafach sześciennych autorstwa Greenlaw i Petreschi , jeśli jakiekolwiek porównanie może być zrobione między nimi.

Czy takie badanie wymknęło mi się, ponieważ nie istnieje, lub dlatego, że właśnie go przegapiłem?

ds.algorithms reference-request sat optimization Anthony Labarre
źródło
Co dokładnie rozumiesz przez „warianty SAT”?
Giorgio Camerani,
@Walter: Przepraszam, jeśli to nie jest właściwe słowo, miałem na myśli takie rzeczy jak -SAT, Planar-SAT, NAE-SAT itd. ... ale prawdopodobnie powinienem zawrzeć te dwa słowa między nawiasami, ponieważ nie wiedzieć, czy to ma znaczenie przy korzystaniu z solverów SAT. k
Anthony Labarre,
4
Nie martw się, to właściwe słowo, powinienem to zrozumieć. Z czysto praktycznego punktu widzenia nie sądzę jednak, żeby to miało znaczenie (najważniejsze jest to, jak oszczędne jest twoje kodowanie). Czy możesz podać dalsze szczegóły dotyczące problemu optymalizacji, który próbujesz rozwiązać? Jestem bardzo zainteresowany praktycznymi zastosowaniami SAT i inżynierskimi aspektami rozwiązywania SAT.
Giorgio Camerani,
Brzmi trochę myląco, gdy mówisz o problemie z optymalizacją, ale jednocześnie o SAT. Zazwyczaj dla optymalności potrzebujesz czegoś mocniejszego, np. MAX-SAT. Może mógłbyś to wyjaśnić.
Mikolas
to pytanie może być nieco powiązane: cstheory.stackexchange.com/q/4314/4506
Mikolas

Odpowiedzi:

9

Nie jestem pewien, czy tego właśnie szukasz, ale oto jedno: JM Silva, Praktyczne zastosowania logicznej satysfakcji .

Mikolas
źródło
2
Nie mogłem uzyskać dostępu do tego przez twój link, oto kolejny . Na pierwszy rzut oka papier wydaje się dość interesujący, ale bardziej skoncentrowany na aplikacjach niż na tym, czego szukam.
Anthony Labarre,
@Anthony dobrze powiedziałeś, że jesteś zainteresowany aspektem praktycznym :-) W każdym razie, istniejące solwery głównego nurtu tak naprawdę nie rozróżniają różnych typów SAT. W przeszłości pracowano na przykład nad wykorzystaniem klauzul binarnych. Ale istniejące solwery wykorzystują po prostu uczenie się DPLL + jednostka prop + klauzula. Jednak niektóre z preprocesorów wykorzystują tę strukturę. Ale znowu, nie tak naprawdę z punktu widzenia złożoności. Klasyfikacja.
Mikolas,
8

Rozdział 2 Podręcznika satysfakcji analizuje aspekty, o których należy pamiętać przy projektowaniu tych transformacji, a także listę odniesień, które odpowiadają na moje pytanie. Pomogło mi to znaleźć kilka przykładów, na które można spojrzeć, aby zapoznać się z tymi transformacjami:

Anthony Labarre
źródło