这个压缩文件包含一个非常简单的MATLAB实现,用经典的Davis-Putnam算法解决可满足性(SAT)问题。函数sat_solve.m接受布尔公式的合取范式(CNF)的稀疏矩阵表示A作为输入。每行表示一个子句,其中的符号代表文字的极性,例如[1 0 -1]表示(x1或不x3)。输出参数包括S:公式是否可满足,以及a:满足布尔公式的赋值。更多详细信息请参阅示例。