1.将一个长度为 n 的二进制串 s 初始化为 00⋯0 ; 2.循环直到串 s 为 11⋯1 2.1 将二进制串 s 代入给定的合取范式中; 2.2 若合取范式取值为 TRUE ,则将串 s 作为结果输出,算法结束; 2.3 否则,将串 s 加 1; 3.输出 “无解” ;

这是一种基于暴力枚举的方法，称为“穷举法”。它的时间复杂度为$O(2^n)$，当$n$较大时，计算量非常大，不适合实际应用。以下是使用Python实现该算法的示例代码：

def brute_force_sat(clauses):
    n = len(clauses[0]) - 1  # 变量数
    s = [0] * n  # 初始化为 0
    while s != [1] * n:  # 循环直到 s 变为 1...1
        # 将二进制串 s 代入合取范式中
        satisfied = True
        for clause in clauses:
            clause_satisfied = False
            for i in range(n):
                if clause[i] == -1 and s[i] == 0:
                    clause_satisfied = True
                    break
                elif clause[i] == 1 and s[i] == 1:
                    clause_satisfied = True
                    break
            if not clause_satisfied:
                satisfied = False
                break
        if satisfied:
            return s
        # 将 s 加 1
        i = 0
        while i < n and s[i] == 1:
            s[i] = 0
            i += 1
        if i < n:
            s[i] = 1
    return None  # 无解

# 测试
clauses = [[1, -2, 3], [-1, 2, 3], [1, 2, -3], [-1, -2, 3]]
solution = brute_force_sat(clauses)
if solution:
    print('SAT solution:', solution)
else:
    print('No solution')

其中，`clauses`表示CNF范式中的所有子句，每个子句是一个长度为$n+1$的列表，其中第$i$个元素表示第$i$个变量在该子句中的取值（1表示选中，-1表示否定，0表示不考虑）。函数`brute_force_sat`返回一个列表，表示求解得到的可行解。如果没有找到可行解，则返回`None`。