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.
źródło