没学过不会，希望用python代码解答一下，请详细一点，主要我不懂那个合理范式是啥

Question

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

Answer 1

def evaluate(expression, assignment):
    for clause in expression:
        satisfied = False
        for literal in clause:
            variable, negated = abs(literal), literal < 0
            if (variable in assignment and assignment[variable] == (not negated)):
                satisfied = True
                break
        if not satisfied:
            return False
    return True

def increment_binary_string(binary_string):
    carry = 1
    result = ""
    for i in range(len(binary_string) - 1, -1, -1):
        sum_val = int(binary_string[i]) + carry
        result = str(sum_val % 2) + result
        carry = sum_val // 2
    return result

def sat_solver(expression, n):
    assignment = {}
    current = "0" * n
    target = "1" * n

    while current != target:
        if evaluate(expression, [int(bit) for bit in current]):
            return current
        current = increment_binary_string(current)

    return "无解"

# 示例输入：expression为合取范式，n为变量个数
expression = [[1, 2, 3], [-1, 2, -3], [-1, -2, 3], [1, -2, -3]]
n = 3
result = sat_solver(expression, n)
print(result)