Zrozumienie wydajności solverów QFBV SMT

9

Solwery SMT, takie jak Z3 lub Boolector, wykorzystują złożony zestaw heurystyk do rozwiązywania problemów. Jednak bardzo utrudnia to przewidywanie wydajności takiego rozwiązania. Moje pytanie brzmi zatem:

Pytanie

Czy istnieje sposób na zrozumienie lub uzyskanie wglądu w wydajność solvera SMT dla konkretnego w teorii bitwektorów bez kwantyfikatora (QFBV)?

Obejmuje to także wszelkie narzędzia do wizualizacji, które pomogłyby zrozumieć, gdzie solver „utknął” / nie robi postępów.

Aplikacje

  • Zrozumcie z wyprzedzeniem, jak różne kodowania tego samego problemu wpływają na wydajność solvera (aktualny stan wiedzy nie może być „po prostu wypróbuj kilka różnych kodowań i mam nadzieję, że jedno jest wystarczająco szybkie”, prawda?)

  • Jeśli dany problem nie może zostać rozwiązany przez solver SMT z powodu ograniczeń czasowych, znajdź sposób, aby wyrazić problem inaczej, aby można go było rozwiązać.

  • Unikaj marnowania czasu na uproszczenia specyficzne dla domeny, które nie wpłyną wcale na wydajność solvera, a nawet negatywnie wpłyną na wydajność solvera.

Istniejące badania

Próbowałem znaleźć badania na ten temat, ale nie znalazłem wiele. Nie mam jeszcze dużego doświadczenia w dziedzinie solverów SAT / SMT, więc przepraszam, jeśli coś przeoczyłem.

  • SATzilla : przewiduje najlepiej działający solver na podstawie funkcji wyodrębnionych z problemu za pomocą technik uczenia maszynowego.

    Dotyczy to tylko SAT zamiast SMT i nie wyjaśnia przyczyn wydajności solverów.

  • Profiler aksjomatyczny Z3 Wizualizacja wykresu instancji Z3 i analiza pasujących pętli

    Wygląda na to, że skupia się tylko na teorii ilościowej.

bennofs
źródło

Odpowiedzi:

3

Krótka odpowiedź brzmi: nie, nie rozumiemy tego. Długa odpowiedź brzmi: tak, mamy pewne granice, ale te granice nie są zbyt pomocne. Jest całkiem jasne, że najgorszy czas działania ma charakter wykładniczy. Nie jest to zbyt pomocne, ponieważ wiemy, że w niektórych / wielu praktycznych sytuacjach wydaje się działać dość szybko - i tak naprawdę nie wiemy, dlaczego.

Nie wiemy, dlaczego tak jest w przypadku solverów SAT, nie mówiąc już o QFBV. Zrozumienie, dlaczego solwery QFBV są często szybkie, wydaje się co najmniej tak samo trudne, jak zrozumienie, dlaczego solwery SAT są często szybkie, co jest już powyżej naszego obecnego poziomu zrozumienia. Jeśli szukasz więcej na tej stronie, możesz znaleźć podsumowanie bieżących prób zrozumienia tego ostatniego tematu.

DW
źródło
dzięki za odpowiedź! już tak myślałem. Czy wiesz, czy są jakieś badania, które nie próbują znaleźć ogólnych zasad, ale zamiast tego wizualizują powód niskiej wydajności solvera sat / smt (lub w inny sposób pomagają użytkownikowi zrozumieć, jaka część problemu daje i SMT solver touble)
bennofs