Заставить Z3 сначала исследовать пространство-кандидат? - PullRequest
Новая
       20

Заставить Z3 сначала исследовать пространство-кандидат?

0 голосов
/ 22 декабря 2018

У меня был вопрос о smt-решателях (например, Z3), и мне было интересно, знаете ли вы какую-нибудь тактику Z3, которая может помочь мне достичь моей цели.

Я хочу знать, возможно ли форсировать Z3изучить некоторые переменные, прежде чем исследовать другие.

Например, у меня есть сценарий, в котором моя проблема MaxSMT имеет следующие жесткие ограничения 

X1 + X4 >=3
X2 + 7  >=3
X3 + 8  >=3

И мягкое ограничение равно 

X4 == 0

Здесь я хочу заставить smt-solver сначала исследовать пространство кандидатов с различными значениями для переменной X1.(Я полагаю, что по умолчанию Z3 случайным образом исследует различные значения X1, X2, X3, X4)

Так что мой вопрос - есть ли какая-либо тактика в Z3, которая позволяет мне сказать решателю Z3, какое пространство кандидата (набор переменных) стоит попробовать сначала?

1 Ответ

0 голосов
/ 22 декабря 2018

Движок max-smt допускает параметризацию пользователя в z3, но, к сожалению, неясно, позволит ли какой-либо из этих твиков сделать то, что вы хотите.Но вы можете, по крайней мере, спросить, что такое «твики», используя команду z3 -p и просматривая список.Я нашел следующие параметры: 

[module] opt, description: optimization parameters
    maxres.add_upper_bound_block (bool) (default: false)
    maxres.hill_climb (bool) (default: true)
    maxres.max_core_size (unsigned int) (default: 3)
    maxres.max_correction_set_size (unsigned int) (default: 3)
    maxres.max_num_cores (unsigned int) (default: 4294967295)
    maxres.maximize_assignment (bool) (default: false)
    maxres.pivot_on_correction_set (bool) (default: true)
    maxres.wmax (bool) (default: false)
    maxsat_engine (symbol) (default: maxres)

(Есть и другие, но они кажутся наиболее актуальными.)

Чтобы увидеть, как они влияют на поиск, вам лучше всего прочитать черезисходный код: https://github.com/Z3Prover/z3/blob/master/src/opt/maxres.cpp

В качестве альтернативы, вы можете попробовать задать вопрос на сайте z3 github (https://github.com/Z3Prover/z3/issues),, и авторы могут указать вам лучшее направление.

...