布尔可满足性(Boolean Satisfiability,SAT)问题是指,给定一组布尔变元X及由X构成的CNF公式,问是否存在一组对X的赋值,使得公式为真。SAT问题是第一个被证明为NP完全的问题,在计算理论中具有重要地位。如果找到能够在多项式时间求解SAT问题的完备方法,则P=NP;反之,如果能够确定所有SAT算法的最坏时间复杂度下界为指数级别,则P≠NP。此外,SAT问题在电路验证、组合优化、自动推理等领域有重要的实践意义。当前,SAT问题的求解算法分为完备算法和不完备算法。完备算法总是能够找到一个满足公式的赋值,或者证明公式的不可满足性。基于DPLL的搜索算法是目前主流的一类完备算法,这类算法用回溯的方法,对赋值空间进行系统的搜索。在对DPLL算法的各种改进中,CDCL算法利用子句学习和非逐字回溯大大减少了回溯次数。目前已知的完备算法最坏时间复杂度为指数级别。而不完备算法针对实际的SAT问题,提高了求解效率。其中,局部搜索算法广泛应用了概率和贪心的策略,只对赋值空间的一部分进行搜索,提高了搜索效率。基于优化的方法将SAT问题转化为优化问题,然后用拉格朗日法、牛顿法等方法解决。此外,有研究者从统计物理学得到启发,提出基于消息传递的纵览传播算法。当不完备算法找不到满足公式的赋值时,无法判定公式是否可满足。为了进一步研究SAT问题,有的研究者将关注点转移到一些特殊的SAT问题,比如1-in-3-SAT。1-in-3-SAT与3-SAT可以在多项式时间内相互转化,因此1-in-3-SAT问题也是NP完全问题。近年来,有一种称为LAF的方法可以用于证明一部分1-in-3公式的不可满足性。但是当公式是1-in-3可满足的时候,LAF算法还有待改进。本文基于LAF算法,提出了一种不完备的剪枝搜索方法,在多项式时间搜索能够1-in-3满足公式的赋值。实验证明,当变元不多于160个时,这种搜索方法能够判定大多数公式的可满足性。当变元个数增多时,搜索方法的效率下降。这是因为1-in-3-SAT的计算复杂度取决于对应公式的变元以及子句的个数。如何约减1-in-3公式,即,归约至一个变元数或者子句数更少的1-in-3公式,是提高求解1-in-3-SAT问题效率的一个关键。针对这个问题,本文基于一个新的范式形式——XCNF,对1-in-3-SAT问题提出一种新的代数逻辑约化方法,在多项式时间约减一个1-in-3公式的变元数和子句数。在该约化下,约减公式与原公式的1-in-3可满足性等价。