我可以解释任何必要的深度，但长话短说，我的项目使用 Z3 的优化器来找到有效解决与布尔变量相关的权重的 SAT 问题的最大解决方案。除此之外，我项目的另一部分有效地实现了基于规则的饱和引擎，我最近一直在考虑使用定点求解器对其进行重写。我以为我可以分别考虑问题的两个部分，但事实证明存在先有鸡还是先有蛋的问题，规则引擎需要解决 SAT 实例才能使其输入和输出正确且有意义，并且 SAT 实例本身来自规则引擎的输出。因此，我想我可能会尝试结合Fixedpoint和Optimize. 这可能吗？它甚至有意义吗？
问问题
61 次