Как определить количество решений данного экземпляра с помощью Mathsat

Mathsat поддерживает команду check-allsat, а Z3 ее не поддерживает. Пожалуйста, рассмотрите следующий пример:

(declare-fun m () Bool)
(declare-fun p () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun r () Bool)
(declare-fun al () Bool)
(declare-fun all () Bool)
(declare-fun la () Bool)
(declare-fun lal () Bool)
(declare-fun g () Bool)
(declare-fun a () Bool)
(define-fun conjecture () Bool
(and (= (and (not r) c) m) (= p m) (= b m) (= c (not g)) (= (and (not al) (not all)) r)
(=(and la b) al) 
(= (and al la lal) all) (= (and (not g) p a) la) (= (and (not g) (or la a)) lal)))
(assert conjecture)
(check-allsat (m p b c r al all la lal g a))

При выполнении этого кода с помощью mathsat получаются все согласованные назначения. Вопрос в том, как определить количество таких последовательных заданий с помощью Mathsat?


z3 smt z3py mathsat
person Juan Ospina    schedule 05.11.2013    source источник
comment
Вопрос в том, как определить количество таких последовательных заданий с помощью Mathsat? Вы имеете в виду ... использование Z3 ?? Если да, пробовали ли вы API с генерацией модели, например: все удовлетворяющие модели">stackoverflow.com/questions/13395391/ или stackoverflow.com/questions/19578627/model-counting-in-z3py   -  person Taylor T. Johnson    schedule 05.11.2013
comment
Я имею в виду использование Mathsat: как считать решения с помощью Mathsat?   -  person Juan Ospina    schedule 05.11.2013

Ответы (1)


arrow_upward
3
arrow_downward

Я не знаю ни одной команды для подсчета количества решений. Но это можно легко сделать с помощью MathSAT API. Создайте счетчик и увеличивайте его каждый раз, когда MathSAT уведомляет.

static int counter = 0;
static int my_callback(msat_term *model, int size, void *user_data)
{
   counter++; return 1;
}
...
msat_all_sat(env, important, 4, my_callback, &data);
person qsp    schedule 18.11.2013