如何只得到z3满足性检查后使用的变量的相关值赋值？
比如说
我有多个断言作为约束条件给了Z3 Sat Solver, 而一个布尔表达式，我需要检查它是否满足。
Note: The assertion may contain variables which are not present/irrelevant in the Boolean Expression (Formula)
分配给模型的值也包含了对断言约束的赋值，这对布尔表达式的满足性没有影响。
我可以在模块中看到 smt.relevance: 2 作为z3配置中的默认值。如何只限制对表达式可满足性有影响的变量？
一般来说，你不能这样做。一个sat求解器会 "启发式 "地求解约束条件，以找到一个满足的赋值，一般来说，你无法控制这种搜索如何进行。它们不会找到任何形式的 "最小满足赋值"。
你可以限制输出只包含那些在公式中出现的变量，并在最后查询这些变量的值。如果你的公式中有一个变量的赋值与SAT无关，这种技术显然是行不通的，但它应该能让你走得更远。