Giải thích số liệu thống kê Z3

Question

Tôi thu được một số thống kê từ các lần chạy của Z3. Tôi cần phải hiểu những gì có ý nghĩa. Tôi khá là gỉ và không cập nhật cho những phát triển gần đây của sat và SMT giải quyết, vì lý do này tôi đã cố gắng để tìm giải thích bản thân mình và tôi có thể đã chết sai. Vì vậy, câu hỏi của tôi chủ yếu là:

1) Tên của các biện pháp có ý nghĩa gì?

2) Nếu sai, bạn có thể cho tôi biết con trỏ để hiểu rõ hơn về những gì họ đề cập không?

Các quan sát khác được thực hiện bên dưới và khái niệm thuộc về hai câu hỏi trên. Cảm ơn bạn trước!

Giải thích của tôi sau.

• DPLL. Tất cả các số liệu dưới đây đề cập đến thuật ngữ của thuật toán DPLL là nền tảng của hầu hết các giải pháp.

  • : quyết định
    • Số quyết định
  • : propagations
    • Số propagations (tôi đoán propagations đơn vị)
  • : nhị phân-propagations,: ternary-propagations
    • Propagations hai và ba chữ cùng một lúc
  • : mâu thuẫn
    • Số xung đột

• GIẢI PHÁP. Các thao tác đã thực hiện các mệnh đề diễn giải như các bộ, nói gần như; kỹ thuật lấy từ độ phân giải là một mô hình khác để giải quyết SAT.

  • : gộp
  • : subsumption độ phân giải
    • sự khác biệt giữa hai bên trên là gì?
  • : dyn-subsumption độ phân giải
    • nên được mô tả ở đây: Học cho động Subsumption, bởi Hamadi et al.

• kỹ thuật khác

  • : giảm thiểu-Lits
    • Không có ý tưởng rõ ràng. Có lẽ nó liên quan đến việc học mệnh đề?
  • : việc khảo sát giao
    • Tôi đoán nó đếm số nhiệm vụ thực hiện khi "thăm dò", mà tôi đoán là một số loại kỹ thuật lookahead.
  • : del-khoản
    • Số khoản bị xóa (lý do gì dư thừa?)
  • : Elim-literals: Elim-khoản: elim- bool-vars: loại trừ bị chặn
    • Số lượng đối tượng sau khi loại bỏ loại bỏ. Những số liệu tham khảo đặc biệt SAT kỹ thuật giải quyết (xem để tham khảo Blocked khoản loại trừ, bởi M.Järvisalo et al.)
  • : khởi động lại
    • Số lần khởi động lại.

• khía cạnh khác

  • : mk-bool-var: mk-nhị phân khoản: mk-ternary-khoản: mk-khoản
    • Số biến boolean và nhị phân , các mệnh đề ternary và generic được tạo ra.
  • : bộ nhớ
    • lượng tối đa bộ nhớ sử dụng.
  • : gc-khoản
    • khoản rác-thu ...?
    • giải thích này là chính đáng theo thí nghiệm của tôi vì nó luôn luôn như vậy mà
      • : gc-khoản < =: del-khoản; trong trường hợp của tôi, sự bất bình đẳng là nghiêm ngặt.
    • Nó không phải là luôn luôn như vậy mà
      • : gc-khoản < =: Elim-khoản; nó cũng có thể là: gc-khoản>: Elim-khoản

Answer 1

Tôi sợ đây là một câu hỏi mở. Z3 cho thấy nhiều quầy được thu thập theo nhiều cách khác nhau. Trong khi nhiều khái niệm trừu tượng chụp, ý nghĩa của chúng cuối cùng là dựa trên hành vi thực hiện của mã.

May mắn thay mã nguồn có sẵn và cung cấp ngữ cảnh đầy đủ để hiểu hành vi của từng bộ đếm. Vì vậy, không có tài liệu nào theo dõi ý nghĩa của các bộ đếm, nhưng mã nguồn được tạo sẵn để cung cấp ngữ cảnh đầy đủ.