用于合成社会法律的真实性多单元盈利最优机制

本文将社会法律合成（SLS）建模为战略多智能体环境中的新型多单元机制设计问题。我们基于交替时间逻辑（ATL）构建贝叶斯单参数采购拍卖模型，旨在设计一个真实性、 individually rational且盈利最优的机制。我们首先证明了一个表示引理，表明任何遵循交替双模态性的评估都可以简洁地表示为ATL公式的特征集合。随后我们将支付确定问题简化为分配确定问题，时间复杂度为多项式级，从而解决了多单元环境中固有的支付不规则问题。我们进一步表明，分配确定问题为 $FP^{NP}$-complete，并将ATL语义编码为整数线性规划（ILP）约束，以便使用标准求解器求解。基于这些结果，我们提出了 $\mathcal{PO\text{-}ASL}$ 机制，该机制具有激励相容性、individual rationality，并最大化预期利润。理论保证和示例确认，我们的方法为在战略智能体行为下合成最优社会法律提供了有效且计算可行的解决方案。