如何用Z3 .NET库实现塔楼谜题的可见塔楼数量约束？

针对塔楼谜题中“从某方向可见X座塔楼”的约束，核心是用Z3的逻辑表达式建模**“当前塔楼是否比之前所有塔楼更高”**，再通过求和得到可见总数，最终绑定目标值。以下是具体实现思路和代码示例：

核心逻辑 #

从某方向（比如左）看，可见塔楼的数量等于从该方向开始，每个“比之前所有塔楼都高”的位置的数量。我们需要用Z3的辅助变量记录两个关键信息：

1. 到当前位置为止的最大塔楼高度
2. 当前塔楼是否是新的“可见塔楼”（即比之前的最大值更高）

最后将所有“可见塔楼”的标记求和，约束其等于题目给定的目标数。

代码示例（以左方向可见约束为例） #

假设你已经初始化了Z3的Context，并创建了5x5的IntExpr数组cells（每个元素取值1-5，且行/列已满足排列约束）。

1. 处理单行左方向可见约束 #

// 假设targetLeft是长度为5的数组，存储每行左方向的目标可见数
int[] targetLeft = { 3, 1, 2, 4, 2 };
Context ctx = new Context();

for (int row = 0; row < 5; row++)
{
    // 辅助变量：记录到当前位置的最大高度
    IntExpr[] maxLeft = new IntExpr[5];
    // 辅助变量：标记当前位置是否为可见塔楼（Bool类型）
    BoolExpr[] isVisibleLeft = new BoolExpr[5];

    // 第一个塔楼必然可见，最大值就是自身
    maxLeft[0] = cells[row][0];
    isVisibleLeft[0] = ctx.MkTrue();

    // 从第二个位置开始递推
    for (int col = 1; col < 5; col++)
    {
        // 更新当前最大值：如果当前塔楼比之前的最大值高，就替换，否则保留原最大值
        maxLeft[col] = ctx.MkITE(
            ctx.MkGT(cells[row][col], maxLeft[col - 1]),
            cells[row][col],
            maxLeft[col - 1]
        );

        // 当前塔楼可见的条件：比之前的最大值高
        isVisibleLeft[col] = ctx.MkGT(cells[row][col], maxLeft[col - 1]);
    }

    // 计算可见总数：将每个可见标记转换为1/0后求和
    IntExpr countLeft = ctx.MkAdd(
        ctx.MkITE(isVisibleLeft[0], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleLeft[1], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleLeft[2], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleLeft[3], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleLeft[4], ctx.MkInt(1), ctx.MkInt(0))
    );

    // 添加约束：可见总数等于目标值
    ctx.Assert(ctx.MkEq(countLeft, ctx.MkInt(targetLeft[row])));
}

适配其他方向的约束 #

• 右方向：从每行最后一列开始向左递推，记录从右到左的最大值，判断当前塔楼是否比右侧的最大值更高，最后求和约束。
• 上方向：按列从上到下递推，记录每列从上到下的最大值，判断当前塔楼是否比上方的最大值更高。
• 下方向：按列从下到上递推，记录每列从下到上的最大值，判断当前塔楼是否比下方的最大值更高。

以右方向为例，核心代码片段：

for (int row = 0; row < 5; row++)
{
    IntExpr[] maxRight = new IntExpr[5];
    BoolExpr[] isVisibleRight = new BoolExpr[5];

    maxRight[4] = cells[row][4];
    isVisibleRight[4] = ctx.MkTrue();

    for (int col = 3; col >= 0; col--)
    {
        maxRight[col] = ctx.MkITE(
            ctx.MkGT(cells[row][col], maxRight[col + 1]),
            cells[row][col],
            maxRight[col + 1]
        );
        isVisibleRight[col] = ctx.MkGT(cells[row][col], maxRight[col + 1]);
    }

    IntExpr countRight = ctx.MkAdd(
        ctx.MkITE(isVisibleRight[0], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleRight[1], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleRight[2], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleRight[3], ctx.MkInt(1), ctx.MkInt(0)),
        ctx.MkITE(isVisibleRight[4], ctx.MkInt(1), ctx.MkInt(0))
    );

    ctx.Assert(ctx.MkEq(countRight, ctx.MkInt(targetRight[row])));
}

关键说明 #

• 所有逻辑都基于Z3原生的表达式类型（IntExpr、BoolExpr），避免了普通整数逻辑的直接使用，完全适配Z3的约束求解机制。
• 递推式的最大值计算比直接比较当前塔楼与所有前置塔楼更高效，减少了约束的复杂度。

内容的提问来源于stack exchange，提问作者darthbob88