Multicore SAT Solver

Próbuję rozwiązać problem SAT z 25k klauzul 5k zmiennych. Ponieważ działa od godziny (precosat), a potem chciałbym rozwiązać większe, szukam wielordzeniowego SAT-Solvera.

Ponieważ wydaje się, że jest wiele rozwiązań SAT, jestem całkiem zagubiony.

Czy ktoś mógłby wskazać mi najlepszy dla mojej sprawy?

Byłbym również szczęśliwy, gdyby ktoś mógł podać mi przybliżony czas (jeśli to możliwe).

— multsatsolv
źródło

Szukasz gotowych programów? To nie jest najlepsza strona do zapytania. Chcesz się dowiedzieć na temat rozwiązywania problemów SAT? Witamy! Mówisz, że szukałeś; co znalazłeś? Co Cię myli?

— Raphael

Cóż, sprawdziłem liczbę wątków związanych z SAT na kilku forach StackExchange. Skończyło się na tym, że zbyt wybrałem teoretyczne CS i CS (i wybieram później). Gdzie powinienem poprosić o gotowy program? Dzięki.

— multsatsolv

Odpowiedzi:

Zobacz wyniki tegorocznego konkursu SAT 2013 . Na podstawie tych wyników zdecydowanie wypróbuj Lingeling . Plingeling jest jego równoległym wariantem.

Jeśli nie musisz udowodnić niezadowolenia (być może wiesz, że instancja jest satysfakcjonująca, a potrzebujesz tylko zadania przypisanego do SAT), możesz również spróbować lokalnych metod wyszukiwania.

— Juho
źródło

Dzięki. Rzucę okiem na (P) Lingeling. Poza tym nie mam pojęcia, czy jest zadowalający (chociaż lepiej, bo inaczej utknę).

— multsatsolv

+1. Opierając się na naszym doświadczeniu, plingeling jest z pewnością tym, co powinieneś najpierw wypróbować (przynajmniej jeśli masz jeden komputer z wieloma rdzeniami i dużą ilością pamięci). Aby uzyskać jeszcze większą wydajność, spróbuj znaleźć klaster obliczeniowy z jak największą liczbą węzłów i uruchom wiele instancji lingelinga (lub plingelinga) z różnymi losowymi nasionami.

— Jukka Suomela

Nie jestem pewien istnienia praktycznych wielordzeniowych satelitów, ale jest kilka projektów i dokumentów:

Krótki przegląd współczesnych równoległych solverów SAT
Asynchroniczne wielordzeniowe przyrostowe rozwiązywanie problemów SAT
cmcSAT - współpracujący solver MultiCore SAT
Poprawa wydajności SAT Solvera przy użyciu podejścia opartego na współpracy wielu rdzeni
ManySAT: Parallel SAT Solver (strona)
PMSat: równoległa wersja minisat (pobieranie, instrukcja)
Plingeling (strona)
SArTagnan - równoległy solver portfolio SAT z bezblokowanym współdzieleniem klauzul fizycznych (źródło)
ppfolio (strona)
antom
PMiniSat
MiraXT , PaMiraXT: Równoległe rozwiązywanie SAT z wątkami i przekazywaniem wiadomości (binarnie)

Znalazłem też ten interesujący punkt: możesz równolegle uruchomić zwykły sat-solver z różnymi nasionami dla tego samego problemu, aby uzyskać efekt wielordzeniowy.

Edytuj: Uwzględniając moje komentarze do pomysłu vzn tutaj:

Podobną alternatywną metodą jest po prostu wybranie jednej zmiennej, ustawienie jej wartości na true, wysłanie jej do jednej instancji solvera. Ustaw jego wartość na false i wyślij ją do innej instancji solvera. Możesz to zrobić dla zmiennych i uruchomić jednocześnie procesów. Wybór zmiennych do ustawienia może być trochę trudny, tj. jeśli są bezpośrednio od siebie zależne, nie ma sensu wybierać jednego, a potem drugiego. Konieczne może być uproszczenie, aby dokonać kolejnych / rekurencyjnych wyborów. $k$ $2^k$

(Byłbym również szczęśliwy, gdyby ktoś mógł podać mi przybliżony czas (jeśli to możliwe) na rozwiązanie problemu SAT dla zmiennych X, Y).

$m$ $n$ $m,n$

— Realz Slaw
źródło

Dzięki za linki. Przeczytam niektóre z nich. Mam nadzieję, że mój problem nie jest zbyt trudny do rozwiązania.

— multsatsolv

@multsatsolv zależy od problemu. To zależy również od kodowania. Solwery SAT mogą różnie obsługiwać różne kodowania tego samego problemu. A różne solwery SAT mogą być lepsze przy jednym kodowaniu niż innym; nie ma na to żadnej nauki (no cóż, ale warto spróbować zrozumieć, w szybkiej ewolucji solverów SAT): jedyne, co można zrobić, to wypróbować różne kombinacje kodowania i solverów.

— Realz Slaw

W rzeczywistości istnieje bardzo prosty sposób na przekształcenie dowolnego solwera SAT w wersję równoległą, ponieważ SAT jest kłopotliwie równoległy w następującym znaczeniu.

$2^n$ $n$ $2^n$

— vzn
źródło

n

$n$

k

$k$

To podejście wydaje się nie sprawdzać się w praktyce zbyt dobrze. W przypadku pozytywnych przypadków następujące podejście jest zwykle znacznie lepsze, jeśli masz wiele komputerów: po prostu uruchom np. Lingeling z tą samą instancją, ale z różnymi losowymi nasionami i poczekaj, aż jeden z solverów znajdzie rozwiązanie.

— Jukka Suomela,

n

$n$

@vzn: Podejście, które zasugerowałeś. Aby zobaczyć, dlaczego nie działa zbyt dobrze, wypróbuj to w rzeczywistych instancjach i porównaj z tym, co zasugerowałem. :) Twoje podejście miałoby sens, gdybyś miał do czynienia z naiwnym algorytmem wyszukiwania wstecznego, ale współczesne solwery SAT są czymś więcej niż naiwnym wyszukiwaniem wstecznym.

— Jukka Suomela

dobrze, ale czy możesz wyjaśnić słowami, na czym polega problem ? Twoje podejście może działać w zadowalających instancjach, ale czy nie zajmie to dokładnie tego samego czasu równolegle, aby odkryć niezadowalającą instancję, bez względu na to, ile osobnych instancji zostanie uruchomionych? jeśli nie, być może istnieje cytat, który można zacytować na

— subj