可满足性问题（Satisfiability Problem，简称SAT）是计算机科学的中心问题之一，也是第一个被证明的NP-完全问题，并且是一大类NP-完全问题的核心。SAT问题是指可满足布尔表达式的集合，它在数理逻辑、人工智能、约束可满足性问题、VLSI集成电路设计与检测、计算机科学理论、计算机视觉、机器定理证明、机器人规划、机器学习等领域具有广阔的应用背景。一个CNF公式F称为线性的，如果F中任意两个不同的子句中至多包含一个相同的变元。一个CNF公式F称为严格线性的，如果F中任两个不同的子句恰好包含一个相同的变元。所有严格线性公式是可满足的（[33]S．Porschen etc．，2006）。对于线性公式类LCNF，判定问题LSAT是NP-完全的。对于LCNF的子类LCNF_≥k（其公式中每个子句的长度至少为k），如果在LCNF_≥k公式中存在一个不可满足公式，则判定问题LSAT_≥k是NP-完全的（[31，32]S．Porschen，E．Speckenmeyer，2006）。因此，对于LCNF_≥k（k≥3）公式，判定问题LSAT_≥k的NP-完全性取决于在LCNF_≥k公式中是否存在不可满足公式。在（[31，32]S．Porschen，E．Speckenmeyer，2006）中，通过构造超图和拉丁方阵，已经证明了LCNF_≥3和LCNF_≥4都包含不可满足公式，并提出了一个公开问题：当k≥5时，在LCNF_≥k公式中是否存在不可满足公式。本文基于线性公式的结构与特点，提出了线性化算法，使用该算法可以在|F|多项式时间内把任一公式F转化为线性公式F^lin，且两者有相同的可满足性。另外，本文通过研究极小不可满足公式在公式归约中的应用，给出了在k-LCNF（其公式中每个子句的长度都为k，k≥3）公式中构造不可满足公式的一般方法。证明了：对每个k≥3，k-LCNF公式中存在极小不可满足公式，并且证明了下面更强的结果：对每个k≥3，k-LSAT是NP-完全的。