Я использую решатель Z3 с Python API для решения проблемы Circuit SAT. Он состоит из множества выражений Xor с 21 входом и выражений And с тремя входами. Z3 умеет решать мои маленькие примеры, но не справляется с большими.
Вместо создания объекта Solver с
s = Solver()
Я попытался оптимизировать тактику решателя, как в
t = Then('simplify', 'symmetry-reduce', 'aig', 'tseitin-cnf', 'sat' )
s = t.solver()
Я получил список тактик через describe_tactics()
К сожалению, мои попытки не увенчались успехом. Последовательность тактик по умолчанию, кажется, неплохо справляется со своей задачей. Учебник по тактике, ранее доступный в rise4fun, больше недоступен.
Другая попытка - без видимого эффекта - заключалась в установке параметра фазы, так как я ожидаю, что большинство моих переменных будут иметь ложные значения. (см. связанный пост)
set_option("sat.phase", "always-false")
Какая последовательность тактик рекомендуется для решения проблем Circuit SAT?
