采用以下一组逻辑语句：
A： B为错误
B： C为错误
C： B或A是真正的
我被赋予了将其形式化的任务；DPLL"；可以确定是否存在不会导致矛盾的解决方案(哪些规则为真，哪些规则为假(。
问题是：我不知道该怎么做。在线解算器需要特定格式的表达式，如下图所示：http://www.inf.ufpr.br/dpasqualin/d3-dpll/
如何将我的语句转换为这些数字？
您可能会混淆这里的表示法：我假设这里有三个语句和三个变量。我将用小写字母表示变量，用大写字母表示语句，以明确这一点：
Statement A: not b
Statement B: not c
Statement C: a or b
现在用数字替换小写字母：
Statement A: not 2
Statement B: not 3
Statement C: 1 or 2
not应写为负号，or应替换为冒号。生成的三条线现在可以输入到您链接的SAT解算器中：
-2
-3
1, 2
它输出1, -2, -3作为解，因此变量a必须为真，而b和c必须为假。