根据维基百科，最大可满足性问题 (MAX-SAT) 是确定给定布尔公式的最大子句数的问题，该问题可以通过将真值分配给公式。它是布尔可满足性问题的推广，它询问是否存在使所有子句为真的真值赋值。
我不明白关于 MAX-SAT 如何是 SAT 的概括的第二句话。根据维基百科，SAT 询问给定布尔公式的变量是否可以一致地被值 TRUE 或 FALSE 替换，从而使公式计算为 TRUE。
我之所以问这个问题是因为论文“可满足性和最大可满足性问题的半定优化方法”，我想尝试半定优化技术来解决我手头的一些 SAT 问题。
想象一下，通过为原始问题中的每个子句添加p -> qwhere pis a fresh 变量，将每个子句转换为含义。q然后，MAXSAT当您选择求解器分配true给相应p. 这为您提供了一个 maxsat 求解器，尽管它很糟糕。
现在想象一下，您有一个系统，可以确保它尽可能多地实现这些p。该组合现在为您提供了一个 maxsat 求解器，即可以优化p为真的 s 数量的求解器。这样你就可以为你的原始问题得到一个很好的 maxsat 求解器，也就是说，你可以将 maxsat 问题减少到 sat，只要你有一些东西可以最大化p你通过翻译引入的那些 's 的真实分配的数量。
@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