主要观点：介绍了元变量耦合问题及解决方案 SMT，以 Marisa 躲避会议参会者和空中杂物为例，阐述了 SMT 在解决相关问题中的应用及算法。
关键信息：

• SMT 可确定数学公式是否可满足，在程序验证和模型检查等领域有应用。
• Marisa 躲避问题简化后，通过随机猜测和逻辑推导来确定其移动方向，避免碰撞。
• 介绍了 Temporal Version 中考虑时间因素的情况，通过随机猜测速度并检测碰撞来找到安全路径。
• 核心算法 Conflict-Driven Clause Learning (T) 基于 SAT 求解核心和理论求解器，MBQI 算法用于处理带量词的公式。
  重要细节：
• 定义“hitbox”避免与实体碰撞，Marisa 坐标需满足特定条件。
• 决策点的猜测可能导致冲突，需回溯，通过逻辑推导如传播、回溯等逐步确定条件。
• 在 Temporal Version 中，通过猜测速度和检测碰撞来确定安全速度范围，生成相关子句。
• CDCL 基于 SAT 求解核心和理论求解器，MBQI 算法通过候选模型和 Skolem 化处理带量词的公式。