Otrzymałem kilka statystyk z serii Z3. Muszę zrozumieć, co to znaczy. Jestem raczej zardzewiały i nieaktualny w związku z najnowszymi osiągnięciami w rozwiązaniach sat i SMT, dlatego sam próbowałem znaleźć wyjaśnienia i mogłem być martwy. Moje pytania to głównie:

1) Co oznaczają nazwy środków?

2) Jeśli nie, czy możesz dać mi wskazówki, aby lepiej zrozumieć, do czego się odnoszą?

Poniżej przedstawiono inne obserwacje i koncepcyjnie należą do dwóch powyższych pytań. Z góry dziękuję!

Moja interpretacja następuje.

DPLL. Wszystkie poniższe dane odnoszą się do żargonu algorytmu DPLL, który jest podstawą większości solverów.

: decyzjeLiczba decyzji: propagacjeLiczba propagacji (domyślam się, że propagacje jednostek): propagacje binarne, :propagacje trójskładnikowePropagacje dwóch i trzech literałów naraz: konfliktyLiczba konfliktów

ROZKŁAD. Operacje wprowadzały klauzule interpretacyjne jako zestawy, w przybliżeniu; techniki zaczerpnięte z rozdzielczości, która jest kolejnym paradygmatem do rozwiązywania SAT.

: subsumed: rozdzielczość podmenuJaka jest różnica między powyższymi dwoma?: dyn-subumption-resolutionPowinien zostać opisany tutaj: Nauka dla dynamicznego sumowania, Hamadi i in.

INNE TECHNIKI

: zminimalizowane-litsBez wyraźnego pomysłu. Czy jest to prawdopodobnie związane z nauką klauzuli?: przypisane sondowanieDomyślam się, że liczy się liczba przydziałów dokonanych podczas „sondowania”, co, jak sądzę, jest pewnego rodzaju techniką patrzenia wstecz.: del-klauzulaLiczba usuniętych klauzul (z jakiego powodu? Zbędne?):elim-literały :klauzule elim :elim-bool-vars :klauzule elim-blokowaneLiczba podmiotów poelim- wyłączony. Metryki te odnoszą się do konkretnych technik rozwiązywania SAT (zob. Odnośnik Blocked Clause Elimination, M.Järvisalo i in.): restartujeLiczba ponownych uruchomień.

INNE ASPEKTY

: mk-bool-var :mk-binary-klauzula :mk-ternary-clause :mk-klauzulaUtworzono liczbę zmiennych boolowskich i klauzul binarnych, trójskładnikowych i ogólnych.:pamięćMaksymalna ilość używanej pamięci.: klauzula gcKlauzule gromadzące śmieci ...?Ta interpretacja jest wiarygodna zgodnie z moimi eksperymentami, ponieważ zawsze tak jest:klauzula gc <=:klauzula del ; w moim przypadku nierówność jest surowa.Nie zawsze tak jest:klauzula gc<=:klauzule elim; może to być również:klauzula gc >:klauzule elim