Интерпретация статистики Z3

Я получил несколько статистических данных из прогонов Z3. Мне нужно понять, что это значит. Я довольно ржавый и не в курсе последних событий в области решения проблем с использованием спутниковой и SMT-технологии, по этой причине я сам пытался найти объяснения и мог быть совершенно неправ. Итак, мои вопросы в основном следующие:

1) Что означают названия мер?

2) Если нет, не могли бы вы дать мне указатели, чтобы лучше понять, к чему они относятся?

Другие наблюдения представлены ниже и концептуально относятся к двум вопросам, указанным выше. Заранее спасибо!

Моя интерпретация следует.

  • DPLL. Все приведенные ниже показатели относятся к жаргону алгоритма DPLL, который лежит в основе большинства решателей.

    • :decisions
      • Number of decisions
    • :propagations
      • Number of propagations (I guess unit propagations)
    • :binary-propagations, :ternary-propagations
      • Propagations of two and three literals at once
    • :conflicts
      • Number of conflicts

  • РЕШЕНИЕ. Грубо говоря, операции сделали интерпретирующие предложения как множества; методы, взятые из разрешения, что является еще одной парадигмой для решения SAT.

    • :subsumed
    • :subsumption-resolution
      • What is the difference between the above two?
    • :dyn-subsumption-resolution
      • Should be described here: Learning for Dynamic Subsumption, by Hamadi et al.

  • ДРУГИЕ МЕТОДЫ

    • :minimized-lits
      • No clear idea. Is it probably related with clause learning?
    • :probing-assigned
      • I guess it counts the number of assignment made when "probing", which I guess is some kind of lookahead technique.
    • :del-clause
      • Number of deleted clauses (for what reason? Redundant?)
    • :elim-literals :elim-clauses :elim-bool-vars :elim-blocked-clauses
      • Number of entities after the elim- eliminated. These metrics refer to particular SAT solving techniques (see for reference Blocked Clause Elimination, by M.Järvisalo et al.)
    • :restarts
      • Number of restarts.

  • ДРУГИЕ АСПЕКТЫ

    • :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
      • Number of boolean variables and binary,ternary and generic clauses created.
    • :memory
      • Maximum amount of memory used.
    • :gc-clause
      • Garbage-collected clauses ...?
      • This interpretation is plausible according to my experiments since it's always the case that
        • :gc-clause <= :del-clause ; in my case the disequality is strict.
      • It is not always the case that
        • :gc-clause<=:elim-clauses; it can also be :gc-clause > :elim-clauses

usage-statistics z3 smt sat-solvers dpll
person gapag    schedule 28.08.2013    source источник
comment
Это хороший вопрос (вместе с частичными ответами), который полностью не рассматривается в других вопросах по SO, но вот некоторые связанные вопросы, которые могут быть полезны: stackoverflow.com/questions/17856574/ stackoverflow.com/questions/10949633/ stackoverflow.com/questions/7340888/ stackoverflow.com/questions/6841193/   -  person Taylor T. Johnson    schedule 28.08.2013

Ответы (1)


arrow_upward
1
arrow_downward

Боюсь, это открытый вопрос. Z3 предоставляет множество счетчиков, которые собираются разными способами. Хотя многие из них отражают абстрактные концепции, их значения в конечном итоге основываются на поведении кода при реализации.

К счастью, исходный код доступен и предоставляет полный контекст для понимания поведения каждого счетчика. Таким образом, нет единого документа, отслеживающего значение счетчиков, но доступен исходный код, чтобы дать полный контекст.

person Nikolaj Bjorner    schedule 06.09.2013