SAT Classifier: Predicting Satisfiability of 3-CNF Boolean Formulas

pip install python-sat

import random
import json
import argparse
from pysat.solvers import Glucose3

random.seed(42)

def generate_3cnf_formula(num_vars, num_clauses):
    formula = []
    for _ in range(num_clauses):
        clause = []
        vars_in_clause = random.sample(range(1, num_vars + 1), 3)
        for var in vars_in_clause:
            literal = f"x{var}" if random.random() < 0.5 else f"~x{var}"
            clause.append(literal)
        formula.append(f"({' v '.join(clause)})")
    return " ^ ".join(formula)


def formula_to_cnf_list(formula_str):
    clauses = []
    for part in formula_str.split("^"):
        part = part.strip()[1:-1]  # remove parentheses
        literals = part.split("v")
        clause = []
        for lit in literals:
            lit = lit.strip()
            if lit.startswith("~"):
                clause.append(-int(lit[2:]))  # ¬x5 -> -5
            else:
                clause.append(int(lit[1:]))  # x5 -> 5
        clauses.append(clause)
    return clauses


def check_satisfiability(clauses):
    solver = Glucose3()
    for clause in clauses:
        solver.add_clause(clause)
    is_sat = solver.solve()
    solver.delete()
    return int(is_sat)


def create_dataset(num_formulas=10_000):
    dataset = []
    for _ in range(num_formulas):
        num_vars = random.randint(5, 20)
        num_clauses = random.randint(40, 100)
        formula_str = generate_3cnf_formula(num_vars, num_clauses)
        clauses = formula_to_cnf_list(formula_str)
        label = check_satisfiability(clauses)
        dataset.append({"formula": formula_str, "label": label})
    random.shuffle(dataset)
    train = dataset[:int(num_formulas*0.9)]
    val = dataset[int(num_formulas*0.9):]

    with open("train.json", "w") as f:
        json.dump(train, f, indent=2)
    with open("val.json", "w") as f:
        json.dump(val, f, indent=2)

create_dataset()

ls

!head train.json

import json
import argparse
import pandas as pd
from sklearn.linear_model import LogisticRegression
from sklearn.model_selection import train_test_split
from sklearn.feature_extraction.text import TfidfVectorizer
from sklearn.metrics import classification_report, confusion_matrix, roc_auc_score

def load_data(json_path):
    with open(json_path, "r") as f:
        data = json.load(f)
    return pd.DataFrame(data)


def preprocess(text):
    # Optional: Remove parentheses, normalize spacing
    return text.replace("(", "").replace(")", "")


def train():
    train = load_data("train.json")
    val = load_data("val.json")

    train["formula"] = train["formula"].apply(preprocess)
    val["formula"] = val["formula"].apply(preprocess)

    # =============================================================================
    # COMPETITION ZONE: MODIFY CODE BELOW THIS LINE
    # =============================================================================
    # You can:
    # - Create new features or feature extractors
    # - Tune classifier hyperparameters
    # - Add different classifiers (RandomForest, SVM, etc.)
    # - Experiment with different vectorizers or tokenization strategies
    # - Combine multiple models or use ensemble methods
    # - Add preprocessing steps
    #
    # Goal: Improve the F1 score and ROC AUC for 3-SAT satisfiability prediction
    # =============================================================================

    # TF-IDF using custom token splitting on AND and OR
    vectorizer = TfidfVectorizer(
        token_pattern=r"~?x\d+",  # Extract literals
    )
    X = vectorizer.fit_transform(train["formula"])
    y = train["label"]

    clf = LogisticRegression()
    clf.fit(X, y)

    X_val = vectorizer.transform(val["formula"])
    y_val = val["label"]


    # =============================================================================
    # DO NOT CHANGE THE CODE BELOW THIS LINE!
    # =============================================================================

    y_pred = clf.predict(X_val)
    pred_proba = clf.predict_proba(X_val)[:, 1]

    roc_auc = roc_auc_score(val["label"], pred_proba)

    print("Classification Report:")
    print(classification_report(y_val, y_pred))

    print("Confusion Matrix:")
    print(confusion_matrix(y_val, y_pred))

    print(f"ROC AUC Score: {roc_auc:.4f}")

train()

train = load_data("train.json")
val = load_data("val.json")

train.label.value_counts()

val.label.value_counts()