有没有可能在Python中生成一种算法来解决带有二进制变量的线性方程组？

from picosat import picosat

def solve_linear_equations(coefficients, constants):
    num_variables = len(coefficients[0])
    num_equations = len(coefficients)

    # 创建一个SAT求解器实例
    solver = picosat()

    # 添加变量
    for i in range(num_variables):
        solver.add_variable()

    # 添加方程
    for i in range(num_equations):
        equation = coefficients[i]
        constant = constants[i]
        clause = []

        # 将线性方程转换为CNF（合取范式）
        for j in range(num_variables):
            if equation[j] == 1:
                clause.append(j + 1)
            elif equation[j] == -1:
                clause.append(-(j + 1))

        # 添加CNF子句
        solver.add_clause(clause + [constant])

    # 求解SAT问题
    result = solver.solve()

    if result == picosat.SAT:
        # 获取解
        solution = [solver.get_model()[i] > 0 for i in range(num_variables)]
        return solution
    else:
        return None

# 示例用法
coefficients = [[1, 0, 1], [-1, 1, 0]]
constants = [1, 0]

solution = solve_linear_equations(coefficients, constants)
if solution is not None:
    print("Solution:", solution)
else:
    print("No solution found.")