我正在尝试寻找解决问题的实用方法（例如，在工程方面），其中我有一堆未知值：
val a: Int32 = ???
val c: Int32 = ???
val d: Bool = ???
和一个表达式二叉树（在内存中），最终返回一个布尔值，例如
((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e
我拥有的布尔运算符and or xor not和 32 位整数有比较之类的东西，以及加法、乘法、除法（注意：这些必须尊重 32 位溢出！）以及一些按位的东西（移位、按位 &、| ^)。但是，我不一定需要支持所有这些操作 [参见：LOL_NO_IDEA]
我想得到三个答案之一：
- ES_POSSIBLE [我不需要知道如何，只是被告知存在一种可能]
- 不可能 [无论我的变量持有什么值，这个等式永远不会是真的]
- LOL_NO_IDEA [这是可以接受的，如果问题太复杂或耗时]
我要解决的问题都不是太大或太复杂，术语太多（最多是数百个）。并且拥有大量的 LOL_NO_IDEA 很好。然而，我正在解决数以百万计的此类问题，因此持续的成本会让人感到痛苦（例如，转换为文本格式，并调用外部求解器）
由于我是从 scala 执行此操作的，因此使用 SAT4J 看起来非常吸引人。虽然，文档很糟糕（特别是像我这样的人，他只研究了这个 SAT 世界几天）
但我目前的想法是首先将所有 Int32 转换为 32 个布尔值。这样，我可以通过将其作为嵌套布尔表达式来表达（a < b）之类的关系（比较 msb，如果它们是 eq，则为下一个，等等）
然后当我有一个布尔变量和布尔表达式的大表达式树时——然后遍历它，同时逐步建立一个： http ://en.wikipedia.org/wiki/Conjunctive_normal_form
然后将其输入SAT4J。
然而，所有这些看起来都非常具有挑战性——甚至构建 CNF 似乎也非常低效（以天真的方式进行，我会实现它）并且容易出错。更不用说尝试将所有整数数学编码为布尔表达式。而且我还没有找到为像我这样的人设计的好资源
我会很感激任何反馈，即使它就像“大声笑，你是个白痴——看看 X”或“是的，你的想法是正确的。享受吧！”