混合互补问题求解策略及Z3求解器调优技术咨询

研究方向 #

本人正在开展以下研究：利用约束传播技术挖掘混合互补问题（MCP）的逻辑条件，将MCP转化为包含互补性条件命题公式的方程组，借助Z3求解器求解，以此引导可行解的搜索方向。

场景设定 #

测试场景为双矩阵博弈（双人同时博弈，双方均有有限行动集），收益由两个矩阵描述：

• 玩家1的收益矩阵：

A = \begin{bmatrix} 3 & 3 \\ 2 & 5 \\ 0 & 6 \end{bmatrix}

策略集为 M = {1, 2, 3}（即A的行）；

• 玩家2的收益矩阵：

B = \begin{bmatrix} 3 & 2 \\ 2 & 6 \\ 3 & 1 \end{bmatrix}

策略集为 N = {4, 5}（即B的列）。

将双矩阵博弈建模为可行性问题，寻找Nash均衡解（给定对方策略时，己方策略为收益最大化策略）。定义变量：

• 玩家1的混合策略变量：x₁, x₂, x₃ ∈ ℝ₊
• 玩家2的混合策略变量：y₄, y₅ ∈ ℝ₊
• 双方期望收益变量：u ∈ [0, max(A)]（玩家1）、v ∈ [0, max(B)]（玩家2）

问题建模 #

收益不等式 #

\begin{align*}
(Ay)_{i} \leq u \quad \forall i \in M \tag{1},\\
(B^{\top}x)_{j} \leq v \quad \forall j \in N \tag{2}.
\end{align*}

混合策略约束（概率分布） #

\begin{align*}
\sum_{i \in M} x_{i} = 1 \tag{3},\\
\sum_{j \in N} y_{j} = 1 \tag{4}.
\end{align*}

互补性条件（双线性项） #

玩家1：

x_{i} (u - (Ay)_{i}) = 0 \quad \forall i \in M \tag{5}

玩家2：

y_{j} (v - (B^{\top} x)_{j}) = 0 \quad \forall j \in N \tag{6}.

这些双线性项表示混合策略向量与期望收益向量正交：若某行动被以正概率选择，则其期望收益等于总期望收益。

假设推导 #

将互补性条件（5）（6）表示为逻辑析取：
玩家1：

(x_{i} = 0) \lor (u - (Ay)_{i} = 0) \quad \forall i \in M \tag{7}

玩家2：

(y_{j} = 0) \lor (v - (B^{\top} x)_{j} = 0) \quad \forall j \in N \tag{8}

再转换为蕴含式：

\begin{align*}
(x_{i} > 0) \Rightarrow (u - (Ay)_{i} = 0) \quad \forall i \in M \tag{9},\\
(y_{j} > 0) \Rightarrow (v - (B^{\top}x)_{j} = 0) \quad \forall j \in N \tag{10},
\end{align*}

也可将前件改为双重否定形式：

\begin{align*}
(x_{i} \neq 0) \Rightarrow (u - (Ay)_{i} = 0) \quad \forall i \in M \tag{11},\\
(y_{j} \neq 0) \Rightarrow (v - (B^{\top}x)_{j} = 0) \quad \forall j \in N \tag{12},
\end{align*}

核心思路是通过混合策略变量的二元分支回溯求解：行动要么以0概率选择，要么以正概率选择（此时对应行动的期望收益等于总期望收益），以此避免在连续混合策略空间中搜索非线性方程组（1）-（6）的解。

求解方案 #

双矩阵博弈必存在混合策略Nash均衡，可通过Lemke-Howson算法（基于A、B的最优响应多面体的转轴技术）求解，但选择SAT/CSP/SMT方法的原因是其建模框架更灵活，可添加额外约束或针对目标优化混合策略向量。

最初选用Z3和Choco+IBEX（多数CSP求解器聚焦离散域，而本问题需连续域），但Choco+IBEX在150×150规模问题上扩展性不如Z3，推测原因是前者寻找区间集，后者聚焦点集。

实验经验 #

默认设置下，Z3可求解规模达150×150、收益为[0,10]整数的随机问题（方程组（1）-（4）加互补性条件）。初步实验显示，互补性约束的实现形式影响求解时间：

• 析取式（7）（8）：求解耗时0.66-10秒；
• 蕴含式（9）（10）：求解耗时1.2-15秒；
• 蕴含式（11）（12）：求解耗时1.2-8秒。

受MIP求解器调优思路启发（如分支策略、变量选择、回调等），希望对Z3进行类似调优。Porter、Nudelman & Shoham（2006）提出通过手动实现基于弧一致性剪枝的回溯算法包裹可行性问题（1）-（4），求解n人双矩阵博弈，该约束传播技术相比Lemke-Howson算法大幅提升计算效率，希望将此逻辑内化为Z3的配置。

具体问题 #

• 能否让Z3优先选择小规模真赋值（即 \min |\{ x_{i} : x_{i} > 0, \forall i \in M \cup N \}|）？
• 能否让Z3优先选择均衡真赋值（即 \min (|\{ x_{i} : x_{i} > 0, \forall i \in M \}| - |\{ y_{j} : y_{j} > 0 \forall j \in N \}|)）？
• 通过Python API设置 set_option(precision=16) 调整任意精度是否有意义？
• 通过Python API指定 SolveFor('QF_LRA') 求解引擎是否有意义？
• 是否应选择其他SMT求解器（如cvc5或MathSAT5）？

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