C#中z3中的递归和多参数函数
我是z3的新手，正在尝试用它来解决逻辑难题。我正在处理的拼图类型，摩天大楼，包括在读取一系列整数时找到新的最大值的次数的给定约束。
例如，如果给定的约束是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定义函数应该是可行的。但是，我没有看到函数有两个参数的任何示例。你知道哪里出问题了吗？我意识到我可以定义所有的原语断言并避免递归，但我想要一个不依赖于拼图大小的通用求解器。
回答 1
Stack Overflow用户
发布于 2021-07-29 15:20:13
如果您发布可以独立运行以进行调试的整个代码段，则堆栈溢出的效果最好。不幸的是，发布选定的部分会让人们很难理解可能的问题所在。
话虽如此，我想知道为什么你一开始就用C/C#编写代码？使用这些较低级别的接口来编写z3，虽然肯定是可能的，但除非您有其他集成需求，否则这是一个糟糕的想法。对于个人项目和学习目的，最好使用更高级别的API。您正在使用的API是非常低级的，您最终要处理的是以API为中心的问题，而不是原来的问题。
在Python中
基于此，我强烈建议使用更高级的API，例如来自Python或Haskell的API。(有许多语言的绑定可用；但我认为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]确实有三座摩天大楼可见。
要求解整个网格，需要创建NxN变量并为所有行/列添加所有skyscraper断言。这是一段代码，但是您可以看到它是相当高级的，并且比您正在尝试的C编码更容易使用。
在Haskell
作为参考，下面是使用构建在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 2，再次给出了3个可见摩天大楼的一排。
摘要
一旦您熟悉了Python/Haskell并对如何解决您的问题有了一个很好的想法，如果您愿意，您可以用C#编写它。我建议你不要这么做，除非你有很好的理由这样做。坚持使用Python或Haskell是避免迷失在API细节中的最佳选择。
https://stackoverflow.com/questions/68569155
复制相似问题
腾讯云开发者
