z3 最优化求解

这次的 Plaid 可以使用的就是 https://z3prover.github.io/papers/programmingz3.html#sec-optimization

这里需要反思一下了，并不是 Optimize 就一定慢。当约束的结果是一个可能的接近最大值的情况下，使用普通的约束求解可能因为少了这个信息（最大）而更加慢

如果可能，这类题目可以转化为 MaxSAT 求解（最小化违反软断言的数量），这就会好的多了

def tt(s, f): 
    return is_true(s.model().eval(f))
 
def get_mss(s, ps):
    if sat != s.check():
       return []
    mss = { q for q in ps if tt(s, q) }
    return get_mss(s, mss, ps)
 
def get_mss(s, mss, ps):
    ps = ps - mss
    backbones = set([])
    while len(ps) > 0:
       p = ps.pop()
       if sat == s.check(mss | backbones | { p }):
          mss = mss | { p } | { q for q in ps if tt(s, q) }
          ps  = ps - mss
       else:
          backbones = backbones | { Not(p) }
    return mss

计算最大满足子集的算法（好，可以出题了😋）

MaxSAT 问题求解：

a, b, c = Bools('a b c')
o = Optimize()
o.add(a == c)
o.add(Not(And(a, b)))
o.add_soft(Or(a, b), 2)
o.add_soft(b, 1)
o.add_soft(c, 1)
print(o.check())
print(o.model())

为了 debug 什么的，可以设置在最大值更新的时候输出当前最大的那个情况长啥样：

def on_model(m):
    print(m.eval(score), bytes(m[c].as_long() for c in flag))
solver = Optimize()
solver.set_on_model(on_model)

试着用 tactic 好像不怎么好使？没有 Optimize 这么好用的接口了