check_assignment.py

from pysat.formula import CNF


def is_model_correct(cnf_file, model):
    cnf = CNF(from_file=cnf_file)

    for clause in cnf.clauses:
        clause_satisfied = False
        for literal in clause:
            if literal > 0 and model[abs(literal) - 1] > 0:
                clause_satisfied = True
                break
            elif literal < 0 and model[abs(literal) - 1] < 0:
                clause_satisfied = True
                break

        if not clause_satisfied:
            return False

    return True


cnf_file_path = "test_16.cnf"

model = [
    -1,
    2,
    -3,
    -4,
    5,
    -6,
    7,
    -8,
    -9,
    -10,
    11,
    12,
    13,
    -14,
    15,
    -16,
    -17,
    -18,
    19,
    -20,
    21,
    -22,
    23,
    24,
    25,
    -26,
    27,
    -28,
    29,
    30,
    -31,
    -32,
    33,
    34,
    35,
    36,
    -37,
    38,
    39,
    -40,
    41,
    42,
    -43,
    -44,
    -45,
    46,
    -47,
    -48,
    -49,
    -50,
    51,
    52,
    53,
    54,
    -55,
    -56,
    -57,
    58,
    59,
    60,
    -61,
    62,
    63,
    -64,
    -65,
    66,
    67,
    68,
    69,
    -70,
    71,
    -72,
    -73,
    -74,
    75,
    -76,
    -77,
    78,
    79,
    80,
    81,
    -82,
    83,
    -84,
    85,
    86,
    87,
    88,
    -89,
    90,
    91,
    -92,
    93,
    94,
    -95,
    -96,
    -97,
    98,
    -99,
    -100,
    -101,
    102,
    103,
    -104,
    105,
    -106,
    -107,
    108,
    109,
    110,
    -111,
    -112,
    113,
    -114,
    115,
    -116,
    -117,
    118,
    -119,
    120,
    -121,
    -122,
    -123,
    124,
    125,
    -126,
    127,
    128,
    129,
    130,
    -131,
    132,
    -133,
    -134,
    -135,
    -136,
    137,
    138,
    139,
    -140,
    -141,
    -142,
    -143,
    144,
    145,
    -146,
    147,
    148,
    149,
    150,
]

if is_model_correct(cnf_file_path, model):
    print("The model is correct!")
else:
    print("The model is incorrect!")