Boolean Satisfiability (SAT) problems are expressed as mathematical formulas. This paper presents an alternative matrix representation for any type of these SAT problems. It shows how to use this matrix representation to get the full set of valid assignments. It proves that this is the full set of answers for the given problem, and it shows that this is exponential in size, relative to the matrix. It then presents an algorithm that utilizes the inverses of the clauses in this matrix for faster searching through this set of answers. It shows that this algorithm is both correct and polynomial.
翻译:布尔可满足性(SAT)问题通常表述为数学公式。本文针对各类SAT问题提出了一种替代性的矩阵表示方法。该表示法可用于获取全部有效赋值集合,并证明此集合构成给定问题的完整解集,同时揭示其规模相对于矩阵呈指数级增长。进一步地,本文提出一种利用该矩阵中子句逆元进行快速解空间搜索的算法,并证明该算法具有正确性且时间复杂度为多项式级别。