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).

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.

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 2 k 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$

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$