所以我有一个 cnf，以及两个变量 K 和 C 的列表。在将 K 的变量发送到 sat-solver 之前，K 的变量作为单位子句（取反或不取决于布尔数组）添加到 cnf。当 sat-solver 返回一个模型时，我只关心 C 中也出现的变量，模型中的所有其他变量都被丢弃。
由于 cnf 将重复运行（将 K 中的不同变量设置为 true 或 false），因此值得花几个小时来简化 cnf 并删除不必要的变量（不必要的是任何不在 K 或 C 中的变量) 如果这意味着每次要解决它时都要减少几分钟。
我的问题是我是否可以使用此 pdf或此博客文章中描述的分辨率变量消除来消除一些变量，只要我不消除 K 或 C 中出现的任何变量。或者这是否会改变结果模型到 C 中的变量？