时间戳

首页 > 解决方案 > C# 中 z3 中的递归和多参数函数

recursion - C# 中 z3 中的递归和多参数函数

问题描述

我是 z3 的新手，并试图用它来解决逻辑难题。我正在研究的谜题类型 Skyscrapers 包括对在读取一系列整数时找到新最大值的次数的给定限制。

例如，如果给定的约束是 3，那么序列 [2,3,1,5,4] 将满足约束，因为我们将检测到最大值“2”、“3”、“5”。

我已经实现了一个递归解决方案，但该规则没有正确应用，并且得到的解决方案无效。

        for (int i = 0; i < clues.Length; ++i)
        {
            IntExpr clue = c.MkInt(clues[i].count);
            IntExpr[] orderedCells = GetCells(clues[i].x, clues[i].y, clues[i].direction, cells, size);
            IntExpr numCells = c.MkInt(orderedCells.Length);
            ArrayExpr localCells = c.MkArrayConst(string.Format("clue_{0}", i), c.MkIntSort(), c.MkIntSort());

            for (int j = 0; j < orderedCells.Length; ++j)
            {
                c.MkStore(localCells, c.MkInt(j), orderedCells[j]);
            }

            // numSeen counter_i(index, localMax)
            FuncDecl counter = c.MkFuncDecl(String.Format("counter_{0}", i), new Sort[] { c.MkIntSort(), c.MkIntSort()}, c.MkIntSort());
            
            IntExpr index = c.MkIntConst(String.Format("index_{0}", i));
            IntExpr localMax = c.MkIntConst(String.Format("localMax_{0}", i));

            s.Assert(c.MkForall(new Expr[] { index, localMax }, c.MkImplies(
                c.MkAnd(c.MkAnd(index >= 0, index < numCells), c.MkAnd(localMax >= 0, localMax <= numCells)), c.MkEq(c.MkApp(counter, index, localMax),
                c.MkITE(c.MkOr(c.MkGe(index, numCells), c.MkLt(index, c.MkInt(0))),
                        c.MkInt(0),
                        c.MkITE(c.MkOr(c.MkEq(localMax, c.MkInt(0)), (IntExpr)localCells[index] >= localMax),
                            1 + (IntExpr)c.MkApp(counter, index + 1, (IntExpr)localCells[index]),
                            c.MkApp(counter, index + 1, localMax)))))));

            s.Assert(c.MkEq(clue, c.MkApp(counter, c.MkInt(0), c.MkInt(0))));

或者作为如何存储第一个断言的示例：

(forall ((index_3 Int) (localMax_3 Int))
  (let ((a!1 (ite (or (= localMax_3 0) (>= (select clue_3 index_3) localMax_3))
                  (+ 1 (counter_3 (+ index_3 1) (select clue_3 index_3)))
                  (counter_3 (+ index_3 1) localMax_3))))
  (let ((a!2 (= (counter_3 index_3 localMax_3)
                (ite (or (>= index_3 5) (< index_3 0)) 0 a!1))))
    (=> (and (>= index_3 0) (< index_3 5) (>= localMax_3 0) (<= localMax_3 5))
        a!2))))

通过阅读这里的问题，我觉得通过 Assert 定义函数应该可以工作。但是，我没有看到函数有两个参数的任何示例。任何想法出了什么问题？我意识到我可以定义所有原始断言并避免递归，但我想要一个不依赖于拼图大小的通用求解器。

标签： recursionz3

解决方案

如果您发布可以独立运行以进行调试的整个代码段，则堆栈溢出效果最佳。不幸的是，发布选定的部分让人们很难理解可能是什么问题。

话虽如此，我想知道你为什么要在 C/C# 中编码？使用这些较低级别的接口对 z3 进行编程虽然肯定是可能的，但这是一个糟糕的主意，除非您有其他集成需求。对于个人项目和学习目的，最好使用更高级别的 API。您使用的 API 非常低级，您最终会处理以 API 为中心的问题，而不是您原来的问题。

在 Python 中

基于此，我强烈建议使用更高级别的 API，例如来自 Python 或 Haskell。（许多语言都有可用的绑定；但我认为 Python 和 Haskell 是最容易使用的。当然，这是我个人的偏见。）

“摩天大楼”约束可以很容易地在 Python API 中进行编码，如下所示：

from z3 import *

def skyscraper(clue, xs):
    # If list is empty, clue has to be 0
    if not xs:
        return clue == 0;

    # Otherwise count the visible ones:
    visible = 1  # First one is always visible!
    curMax  = xs[0]
    for i in xs[1:]:
        visible = visible + If(i > curMax, 1, 0)
        curMax  = If(i > curMax, i, curMax)

    # Clue must equal number of visibles
    return clue == visible

为了使用它，让我们创建一排摩天大楼。我们将根据您可以设置的常量来确定大小，我将其称为N：

s = Solver()
N = 5  # configure size
row = [Int("v%d" % i) for i in range(N)]

# Make sure row is distinct and each element is between 1-N
s.add(Distinct(row))
for i in row:
    s.add(And(1 <= i, i <= N))

# Add the clue, let's say we want 3 for this row:
s.add(skyscraper(3, row))

# solve
if s.check() == sat:
    m = s.model()
    print([m[i] for i in row])
else:
    print("Not satisfiable")

当我运行它时，我得到：

[3, 1, 2, 4, 5]

其中确实有 3 座摩天大楼可见。

要解决整个网格，您将创建 NxN 变量并skyscraper为所有行/列添加所有断言。这是一些编码，但您可以看到它比您尝试的 C 编码更高级且更易于使用。

在哈斯克尔

作为参考，这里是使用构建在 z3 之上的 Haskell SBV库编码的相同问题：

import Data.SBV

skyscraper :: SInteger -> [SInteger] -> SBool
skyscraper clue []     = clue .== 0
skyscraper clue (x:xs) = clue .== visible xs x 1
  where visible []     _      sofar = sofar
        visible (x:xs) curMax sofar = ite (x .> curMax)
                                          (visible xs x      (1+sofar))
                                          (visible xs curMax sofar)

row :: Integer -> Integer -> IO SatResult
row clue n = sat $ do xs <- mapM (const free_) [1..n]

                      constrain $ distinct xs
                      constrain $ sAll (`inRange` (1, literal n)) xs
                      constrain $ skyscraper (literal clue) xs

请注意，这甚至比 Python 编码还要短（大约 15 行代码，而不是 Python 的 30 行左右），如果您熟悉 Haskell，则可以很自然地描述问题，而不会迷失在低级细节中。当我运行它时，我得到：

*Main> row 3 5
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 4 :: Integer
  s2 = 5 :: Integer
  s3 = 3 :: Integer
  s4 = 2 :: Integer

这告诉我高度应该是1 4 5 3 23 座可见的摩天大楼。

概括

一旦您熟悉了 Python/Haskell API 并对如何解决您的问题有了一个好主意，您可以根据需要使用 C# 对其进行编码。不过，我建议您不要这样做，除非您有充分的理由这样做。坚持使用 Python 或 Haskell 是避免迷失 API 细节的最佳选择。

推荐阅读