Zrozumienie wydajności solverów QFBV SMT

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.

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.