0

示例问题：

假设说谎者总是说假话，说真话的人总是说真话。进一步假设 Amy、Bob、Cal、Dan、Erny 和 Francis 都不是说谎者就是说真话的人。

Amy says, “Bob is a liar.”
Bob says, “Cal is a liar.” 
Cal says, “Dan is a liar”
Dan says, “Erny is a liar”
Erny says, “Francis is a liar”
Francis says, “Amy, Bob, Cal, Dan and Erny are liars ”

如果有的话，这些人中有哪些是讲真话的人？

解决方案：

解释：

A : Amy is a truth-teller (X[0])
B : Bob is a truth-teller (X[1])
C : Cal is a truth-teller (X[2])
D : Dan is a truth-teller (X[3])
E : Erny is a truth-teller (X[4])
F : Francis is truth-teller (X[5])

代码：

def add_constraints(s, model):
X = BoolVector('x', 6)
s.add(Implies(X[0], Not(X[1])),Implies(Not(X[1]),X[0]),
  Implies(X[1],Not(X[2])), Implies(Not(X[2]),X[1]),
  Implies(X[2],Not(X[3])), Implies(Not(X[3]),X[2]),
  Implies(X[3],Not(X[4])), Implies(Not(X[4]),X[3]),
  Implies(X[4],Not(X[5])), Implies(Not(X[5]),X[4]),
  Implies(X[5], And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4]))), 
  Implies(And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4])), X[5]))
  notAgain = []
  i = 0
  for val in model:
     notAgain.append(X[i] != model[X[i]])
  i = i + 1
  if len(notAgain) > 0:
    s.add(Or(notAgain))

  return s

 s = Solver()
 i = 0
 add_constraints(s, [])
 while s.check() == sat:
   print s.model()
  i = i + 1
  add_constraints(s, s.model())
  print i # solutions

输出：

[x1 = False,
 x5 = False,
 x0 = True,
 x3 = False,
 x4 = True,
 x2 = True]
 1

解释：

Amy is a truth-teller 
Bob is a liar
Cal is a truth-teller
Dan is a liar
Erny is a truth-teller
Francis is a liar

在此处在线运行此示例

请让我知道您的想法以及是否可以使用 Z3-SMT-LIB 解决此问题。非常感谢。

4

2 回答 2

2

SMT-LIB 没有“check-all-sat”模式。
格式描述如下：http ://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf 您可以使用文件管道与 SMT-LIB 交互以解析/打印以适合您问题的方式获得所有答案的方式。编程 API，例如 python API，更加灵活。

于 2013-06-22T18:02:50.763 回答
0

使用吸血鬼和证明者 9：

 fof(axio1,axiom,(  (truthteller(amy))
        <=> (~ truthteller(bob) )      )).



fof(axio2,axiom,
    ( ( truthteller(bob)
        <=> (~ truthteller(cal)) )  )).


fof(axio3,axiom,
    ( ( truthteller(cal)
        <=> (~ truthteller(dan)) )  )).

fof(axio4,axiom,
    ( ( truthteller(dan)
        <=> (~ truthteller(erny)) )  )).


fof(axio5,axiom,
    ( ( truthteller(erny)
        <=> (~ truthteller(francis)) )  )).

fof(axio6,axiom,
    ( ( truthteller(francis)
        <=> ( (~ truthteller(amy)) & (~ truthteller(bob)) &  (~ truthteller(cal)) 
   & (~ truthteller(dan)) & (~ truthteller(erny))   )     )  )).


fof(goal1,conjecture,
    (~ truthteller(francis) )).

我们获得：

% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Prover9---1109a says Theorem - CPU = 0.00 WC = 0.28  Given = 0 Generated = 18 Kept = 14
% OUTPUT: SOT_LlryEw - Prover9---1109a says Refutation - CPU = 0.00 WC = 0.28


% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Vampire---4.2 says Theorem - CPU = 0.00 WC = 0.01 
% OUTPUT: SOT_LlryEw - Vampire---4.2 says Refutation - CPU = 0.00 WC = 0.01

这样的输出表明“弗朗西斯是个骗子”。

于 2018-02-01T13:19:56.387 回答