1

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 を使用してそのような一貫した割り当ての数を決定する方法です。

4

1 に答える 1

3

解の数を数えるコマンドを知りません。しかし、これは 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);
于 2013-11-18T23:11:37.650 に答える