2

我有一个像(t>=0 or t>=1)and(t<=2 or t>=2)这样的约束，实际上约束可以简化为“ t>=0”，如何使用z3通过z3获得CNF形式的简化结果？

(declare-const t Int)                                                                                  
(assert (and 
            (or
               (>= t 0)
               (>= t 1)
            )
            (or
                (>= t 2)
                 (<= t 2)
            )
            (>= t 0)
            (<= t 1)
        )
)                                                                                         
(apply (par-then (! simplify :elim-and true) tseitin-cnf))

但是，脚本不起作用。

4

1 回答 1

3

该simplify策略仅执行“局部简化”。也就是说，在简化表达式时t，它会忽略 的上下文t。例如，它可以简化a + 1 - a为1，但不会简化a != 0 or b = a + 1为a != 0 or b = 1。上下文简化成本高昂，该simplify策略旨在高效且简单。可以使用其他策略来实现您想要的。

这种策略propagate-ineqs会传播不平等。但是，它不会处理嵌套在公式中的术语。该策略split-clause可用于打破案例\目标中的公式。该策略propagate-values将传播断言的值，例如：a = 0 and b >= a被简化为a = 0 and b >= 0.

该命令(help-tactic)将显示所有可用的策略。

这是将您的示例简化为t >= 0 and t <= 1.

(apply (then simplify propagate-values split-clause propagate-ineqs))

请注意，组合par-then器仅对组合产生许多子目标的策略有用。 (par-then t1 t2)适用t1于输入目标，并t2（并行）适用于由 . 生成的每个子目标t1。该split-clause策略产生了不止一个子目标。然后（对于更大的例子）它可能更有效地使用：

(apply (then simplify propagate-values (par-then split-clause propagate-ineqs)))
于 2012-07-15T16:54:36.683 回答