z3中的主要含义

我使用z3求解器查找QF_AUBV逻辑中用于查找公式（最小）主要含义的解决方案。是否有可能从z3求解器中获得这样的部分主要含义？z3中的主要含义

2016-12-16 Mary

是的，但没有功能可以完成这项工作。您可能不得不使用量词（来公开含义的概念）和/或重复的SAT查询（以最小化含义）。

2016-12-16 11:58:32

非常感谢您的回复。如果我是对的，你的意思是我必须有一个算法来找到最重要的暗示。我读到z3中的相关性传播，只是满足公式的基本真值分配，传播给理论解算器。我可以从这些作业中受益吗？我是对的，这些是部分分配，可能是公式的主要影响因素，也可能不是。如果是，我可以从公式中提取传播的分配给理论解算器吗？ – Mary

如果你正在实施一个理论求解器，这可能会有所帮助（在其他理论中开始寻找relevant_eh（...）），否则它可能不值得（相当大的）努力。请注意，相关性也会传播给非布尔型子项。如果您正在查找所有（主要或其他）含义，那么您将需要多个SAT查询，而不仅仅是一个查询，所以最好在外层而不是SMT解算器内部实现所有这些查询。 –

非常感谢。你是对的。我可以请你更多地解释如何使用量化来将蕴涵者的概念公理化。这对我来说很模糊。 – Mary

z3中的主要含义

回答

相关问题