Sprawdzenie wzorów dwa kwantyfikatorów (

Solwery SAT dają potężny sposób na sprawdzenie poprawności formuły logicznej za pomocą jednego kwantyfikatora.

Na przykład, aby sprawdzić poprawność , możemy użyć solwera SAT, aby ustalić, czy jest zadowalające. Aby sprawdzić ważność , możemy użyć solwera SAT do ustalenia, czy jest zadowalające. (Tutaj jest -ektorem zmiennych boolowskich i $\exists x . \varphi(x)$ $\varphi(x)$ $\forall x . \varphi(x)$ $\neg \varphi(x)$ $x=(x_1,\dots,x_n)$ $n$ $\varphi$ to formuła boolowska).

Solwery QBF są zaprojektowane do sprawdzania poprawności formuły boolowskiej z dowolną liczbą kwantyfikatorów.

Co jeśli mamy wzór z dwoma kwantyfikatorami? Czy są jakieś wydajne algorytmy do sprawdzania poprawności: takie, które są lepsze niż zwykłe algorytmy dla QBF? Mówiąc dokładniej, mam wzór w postaci (lub ) i chcesz sprawdzić jego ważność. Czy są na to jakieś dobre algorytmy? Edytuj 4/8: Nauczyłem się, że ta klasa formuł jest czasami znana jako 2QBF, dlatego szukam dobrych algorytmów dla 2QBF. $\forall x . \exists y . \psi(x,y)$ $\exists x . \forall y . \psi(x,y)$

Specjalizuję się dalej: w moim konkretnym przypadku mam wzór w postaci którego ważność chcę sprawdzić, gdzie są funkcjami, które wytwarzają wyjście bitowe. Czy istnieją jakieś algorytmy do sprawdzania poprawności tego rodzaju formuły, bardziej wydajnie niż ogólne algorytmy dla QBF? $\forall x . \exists y . f(x)=g(y)$ $f,g$ $k$

PS Nie pytam o najgorszą twardość w teorii złożoności. Pytam o praktycznie przydatne algorytmy (podobnie jak współczesne solwery SAT są praktycznie przydatne w wielu problemach, mimo że SAT jest NP-kompletny).

nie jest zasadniczo równoważne

\forall x \exists y ψ (x, y)

$\forall x \exists y \ \psi(x,y)$

\exists x \forall y ψ (x, y)

$\exists x \forall y \ \psi(x,y)$

Huck Bennett

Myślę, że OP oznacza to nieformalnie, ponieważ oba są trudne dla solverów SAT i że rozwiązanie któregokolwiek z nich byłoby interesujące

Suresh Venkat

@HuckBennett, myślę, że oba mają równoważną twardość. (Dowód:

jest poprawny iff

jest. Dlatego jeśli mamy sposób na sprawdzenie poprawności formuł formularza

, możemy również przetestować poprawność formuł

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

\neg \forall x . \exists y . \neg ψ (x, y)

$\neg \forall x . \exists y . \neg \psi(x,y)$

\forall x . \exists y . ψ (x, y)

$\forall x . \exists y . \psi(x,y)$

, pozwalając

i testując poprawność

.) Ale tak czy inaczej, byłbym zainteresowany algorytmami dla obu przypadków.

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

ψ^{'} (x, y) = \neg ψ (x, y)

$\psi'(x,y) = \neg \psi(x,y)$

\forall x . \exists y . ψ^{'} (x, y)

$\forall x . \exists y . \psi'(x,y)$

@DW niekoniecznie, np. SAT i TAUT, nie mają podobnej złożoności.

Kaveh

@chazisop: Myślę, że OP prosi o algorytmy / solwery

-SAT, a nie ogólne solvery QBF. Istnieje jednak wiele solverów QBF. Zobacz zakładkę „solvers” na qbflib.org

Π_{2} / Σ_{2}

$\Pi_2/\Sigma_2$

Huck Bennett

Odpowiedzi:

Jeśli mogę, bezczelnie, zareklamować się, napisaliśmy artykuł o tym w zeszłym roku Algorytm oparty na abstrakcji dla 2QBF . Mam implementację qdimacs, którą mogę dostarczyć, jeśli chcesz, ale z mojego doświadczenia wynika, że specjalizacja algorytmu dla konkretnego problemu może być bardzo korzystna. Istnieje również starszy artykuł Analiza porównawcza algorytmów 2QBF , który przedstawia również dość łatwe do wyobrażenia algorytmy.

Mikolas
źródło

Niesamowite! Dzięki, Mikolas, właśnie tego się spodziewałem.

DW 9'12

Cześć @DW Cieszę się, że mogłem pomóc. Mam nadzieję, że okaże się to przydatne. QBF to zupełnie inna bestia niż SAT, więc trzeba być ostrożnym, ponieważ rzeczy mogą wybuchnąć bardzo łatwo :-). Napisz do mnie e-mail, jeśli masz więcej szczegółowych pytań na temat naszej pracy.

Mikolas

Przeczytałem dwa związane z tym artykuły, jeden związany konkretnie z 2QBF. Dokumenty są następujące:

Oznaczanie przyrostowe , Markus N. Rabe i Sanjit Seshia, Teoria i zastosowania testów satysfakcji (SAT 2016).

Zaimplementowali swój algorytm w narzędziu o nazwie CADET . Podstawową ideą jest stopniowe dodawanie nowych wiązań do formuły, dopóki wiązania nie opisują unikalnej funkcji Skolem lub do momentu potwierdzenia braku.

Drugim jest Incremental QBF Solving , Florian Lonsing i Uwe Egly.

Zaimplementowane w narzędziu o nazwie DepQBF . Nie nakłada żadnych ograniczeń na liczbę naprzemienności kwantyfikatora. Zaczyna się od założenia, że mamy ściśle powiązane formuły qbf. Opiera się na rozwiązywaniu przyrostowym i nie wyrzuca klauzul wyuczonych podczas ostatniego rozwiązywania. Dodaje klauzule i kostki do bieżącej formuły i zatrzymuje się, jeśli klauzule lub kostki są puste, reprezentując polecenia nienasycone lub sat.

Edycja : Dla pewnej perspektywy, jak dobrze te podejścia działają w testach porównawczych 2QBF. Proszę spojrzeć na Wyniki QBFEVal-2018 dla wyników corocznych zawodów QBF QBFEVAL . W 2019 roku nie było utworu 2QBF.

W 2QBF Tor QBFEVAL-2018 DepQBF był zwycięzcą , CADET był drugi w wyścigu.

Te dwa podejścia faktycznie działają bardzo dobrze w praktyce (przynajmniej w testach porównawczych QBFEVAL).

Pushpa
źródło

$\exists x \forall y \phi$ $D$ $a \in D$ $\neg \phi[a/x]$ $b \in B$ $a$ $\phi [b/y]$ $\phi$

Samuel Schlesinger
źródło

ϕ

$\phi$

ϕ

$\phi$

Jest to całkiem miłe, istnieje analogia do przeciwnego uczenia maszynowego, jeśli mrużysz oczy i rzeczywiście działa ona dla każdej uzupełnionej sieci, w której masz swego rodzaju solver

Samuel Schlesinger