SAT 技术可以求解出一个布尔公式的成真赋值
线性时序逻辑 LTL 扩展了命题逻辑，引入了时态运算符来描述系统在时间上的行为
直接使用 SAT 求解器解决 LTL 公式的问题是困难的，因为 LTL 公式涉及到时间的维度
使用 SAT 技术求解 LTL 的一种可行办法是：先将 LTL 公式转换为等价的布尔公式，再用 SAT 求解器来处理
示例
假设我们有以下 LTL 公式：
\phi = G(p \rightarrow F(q \land Xr)) \land F(\neg s)
这个公式可以理解为：
- G(p \rightarrow F(q \land Xr))：全程都有：一旦 p 为真，那么在未来必有某一时刻 q 为真，且再下一时刻 r 为真
- F(\neg s)：将来必有某一时刻s 为假
时间展开
为了使用 SAT 求解器，我们首先需要将这个公式在一个有限的时间范围内展开。假设我们选择的时间界限为 k = 3，那么我们要展开公式中的所有时态运算符到第 3 步：
\begin{aligned}
\phi_0 &= (p_0 \rightarrow (q_0 \land r_1) \lor (q_1 \land r_2) \lor (q_2 \land r_3)) \\
\phi_1 &= (p_1 \rightarrow (q_1 \land r_2) \lor (q_2 \land r_3)) \\
\phi_2 &= (p_2 \rightarrow (q_2 \land r_3)) \\
\phi_3 &= (\neg s_0 \lor \neg s_1 \lor \neg s_2 \lor \neg s_3)
\end{aligned}
构造布尔逻辑公式
将所有时间点上的公式结合起来形成一个布尔逻辑公式：
\phi = \phi_0 \land \phi_1 \land \phi_2 \land \phi_3
这个公式是一个纯布尔逻辑公式，现在我们可以通过 SAT 求解器来判断其可满足性
求解
将上面的布尔公式输入求解器，通过求解器的算法（例如 DPLL 或 CDCL 算法），判断是否存在一个布尔变量的赋值使得公式 \phi 为真
例如，可满足的一组成真赋值：p_0 = \text{true}, q_1 = \text{true}, r_2 = \text{true}, s_3 = \text{false}