C# 中 z3 中的递归和多参数函数
Recursion and Multi-Argument Functions in z3 in C#
我是 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 定义函数应该可行。但是，我没有看到函数有两个参数的任何示例。任何想法出了什么问题？我意识到我可以定义所有原始断言并避免递归，但我想要一个不依赖于拼图大小的通用求解器。
如果您 post 可以独立 运行 调试的整个代码段，那么 Stack-overflow 的效果最好。不幸的是，post选择部分让人们很难理解可能是什么问题。
话虽如此，我想知道您为什么要在 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 变量并为所有 rows/columns 添加所有 skyscraper 断言。这是一些编码，但您可以看到它非常高级，并且比您尝试的 C 编码更容易使用。
在Haskell
作为参考，这里是使用 Haskell SBV 库编码的相同问题，该库建立在 z3 之上：
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 API 并且对如何解决您的问题有了很好的了解，您可以根据需要用 C# 编写代码。不过，我建议不要这样做，除非您有充分的理由这样做。坚持 Python 或 Haskell 是最好的选择，不要迷失在 API.
的细节中
我是 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 定义函数应该可行。但是，我没有看到函数有两个参数的任何示例。任何想法出了什么问题？我意识到我可以定义所有原始断言并避免递归，但我想要一个不依赖于拼图大小的通用求解器。
如果您 post 可以独立 运行 调试的整个代码段，那么 Stack-overflow 的效果最好。不幸的是，post选择部分让人们很难理解可能是什么问题。
话虽如此，我想知道您为什么要在 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 变量并为所有 rows/columns 添加所有 skyscraper 断言。这是一些编码，但您可以看到它非常高级，并且比您尝试的 C 编码更容易使用。
在Haskell
作为参考，这里是使用 Haskell SBV 库编码的相同问题，该库建立在 z3 之上：
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 API 并且对如何解决您的问题有了很好的了解，您可以根据需要用 C# 编写代码。不过，我建议不要这样做，除非您有充分的理由这样做。坚持 Python 或 Haskell 是最好的选择，不要迷失在 API.
的细节中