Wymień wszystkie rozwiązania problemu SAT

11

Wszystkie znane mi solwery #SAT, np. RelSat, C2D, zwracają tylko liczbę zadowalających wystąpień. Ale chcę poznać każdy z tych przypadków?

Czy istnieje taki solver #SAT lub jak powinienem zmodyfikować dostępny solver #SAT, aby to zrobić?

Dziękuję Ci.

lo.logic sat software qsp
źródło
7
Jest to często nazywane „rozwiązaniem SAT dla wszystkich rozwiązań”, ale wydaje się, że nie jest dostępne z półki. Odnośniki, które mogę znaleźć, mówią o modyfikacjach MiniSAT i innych solverów, zwykle przez dodanie klauzul blokujących, aby wykluczyć rozwiązanie, gdy zostanie znalezione. Z drugiej strony większość rozwiązujących ograniczenia obsługuje generowanie wszystkich rozwiązań w standardzie.
András Salamon
jednym z podejść jest konwersja CNF → DNF, dla której jest dużo literatury
2013

Odpowiedzi:

13

Szukasz solvera ALL-SAT lub wszystkich rozwiązań SAT. Jest to inny problem niż #SAT. Nie musisz wyliczać wszystkich rozwiązań, aby je policzyć.

Nie znam narzędzia, które rozwiązałoby twój problem, ponieważ ludzie dodają te algorytmy do istniejących solverów SAT, ale rzadko wydają się wydawać te rozszerzenia. Poniżej znajdują się dwa artykuły, które powinny pomóc w modyfikacji solwera CDCL w celu wdrożenia ALL-SAT.

Rozwiązania SAT Efficient All-Solutions SAT i ich zastosowanie do osiągalności , O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Oto najnowszy artykuł opublikowany na arXiv.

Rozszerzanie nowoczesnych solverów SAT do wyliczania wszystkich modeli , Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

Możesz spróbować skontaktować się z tymi autorami w celu ich wdrożenia.

Vijay D.
źródło
W przypadku drugiego artykułu wystarczy kliknąć pierwszą wersję v1, aby go zobaczyć.
Tayfun Zapłać
Wydaje się, że ten ostatni artykuł jest powiązany: homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh
1
@Kaveh, wierzę, że OP prosi o solver ALLSAT lub sposób na przekształcenie solvera #SAT w solver ALLSAT. To jest artykuł o dolnych granicach dla #SAT. Nie jestem pewien, czy to pomaga OP.
Vijay D
2

Na konferencji VLSI znalazłem nowszy (2014) artykuł na temat All-SAT, więc zdecydowanie jest on ukierunkowany na stronę praktyczną (która wydaje się być zgodna z pytaniem OP tutaj, choć w mniejszym stopniu z cstheory.SE ogólnie):

  • „All-SAT przy użyciu minimalnych klauzul blokujących” Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. doi: 10.1109 / VLSID.2014.22 .

Dla osób bez subskrypcji IEEE dostępna jest bezpłatna kopia na stronie internetowej Subramanyan w Princeton . (Używa usługi udostępniania plików do przechowywania / dystrybucji kopii swoich dokumentów i nie jestem pewien, jak stabilne są te adresy URL, stąd ten link do ronda).

Istotą tego artykułu wydaje się być:

Nasz wkład, algorytm Non-Disjoint-Dec, generuje niezwykle krótkie klauzule blokujące, które nie zawierają żadnej z domyślnych zmiennych w solwerze. Zauważ, że zazwyczaj implikowana jest większość zmiennych w satysfakcjonującym okresie. Krótkie klauzule blokujące są bardzo korzystne dla wydajności solvera, co wykazano w ocenie.

Ich implementacja opiera się na MiniSat. Wydaje się, że kod źródłowy ich rozszerzenia nie jest publicznie dostępny. Niestety wydaje się, że jest to nawyk w dziedzinie All-SAT, więc artykuły w tym obszarze, które zawierają wyniki eksperymentalne, po prostu konfigurują mniej lub bardziej prosty algorytm, który można pokonać i rzadko można go bezpośrednio porównać (pod względem eksperymentalnym wyników) z dowolnym innym opublikowanym algorytmem dla All-SAT. Artykuł Jabbour et al. wspomniane przez Vijay D jest również tego rodzaju.

Ponieważ nie widzę tego w innej odpowiedzi (ale tylko w komentarzu Andrása Salamona), [raczej popularna] technika klauzul blokujących została wprowadzona w:

Syczeć
źródło