根据维基百科，最大满足性问题(MAX-SAT(是确定合取范式给定布尔公式的最大子句数的问题，可以通过将真值赋值分配给公式的变量来使子句为真。它是布尔满足性问题的推广，它询问是否存在使所有子句为真的真赋值。
我不明白关于MAX-SAT如何概括SAT的第二句话。根据维基百科，SAT询问给定布尔公式的变量是否可以一致地替换为值TRUE或FALSE，以使公式的计算结果为TRUE。
我之所以问这个问题，是因为论文"满足性和最大满足性问题的半定优化方法"，我想尝试半定优化技术来解决我手头的一些SAT问题。
想象一下，通过添加p -> q将每个子句变成含义，其中p是原始问题中每个子q的新变量。然后，当您选择求解器将true分配给相应p的那些子句时，此修改后问题的令人满意的实例是原始问题的解决方案MAXSAT。这为您提供了一个maxsat求解器，尽管是一个蹩脚的求解器。
现在想象一下，你有一个系统，确保它尽可能多地使这些p真实。这种组合现在为您提供了一个maxsat求解器，即可以优化真p数的求解器。通过这种方式，您可以为原始问题获得一个不错的maxsat求解器，即，您可以将maxsat问题简化为sat，前提是您有一些东西可以最大程度地增加通过翻译引入的那些p的真正赋值数量。
@PatrickTrentin大概可以解释得更好！vZ 论文(与 z3 相关的 maxsat 引擎(也是关于这个主题的非常好的和简单的阅读： https://backend.orbit.dtu.dk/ws/portalfiles/portal/110977246/Bj_rner_Phan_Fleckenstein_Unknown_Z_An_Optimizing_SMT_Solver_1.pdf