boolean-logic - 原生 XOR 支持：xor-DPLL(to_examine)

Question

这里有没有人理解代码并能够回答我的一些问题？

For info: to_examine是一个队列并保存最近分配的变量。 var显然是一个变量，将检查它是否会导致冲突、传播或什么都没有。

我不明白的是如何DPLL(var)在第 3 行返回一个子句，我认为 DPLL 只能返回 true 或 false。

以及 DPLL 算法如何/为什么只接受第 3 行中的单个变量？

这个伪代码的来源是 Mate Soos 2009 年的博士论文。