looking at 3-SAT phase transitions

3sat.py

from itertools import product
import random

def random_clause(vars):
    """Return a random 3-SAT clause."""
    clause_vars = random.choices(vars, k=3)
    modifiers = random.choices(["", "not "], k=3)
    exprs = [f"{v}{x}" for x,v in zip(clause_vars, modifiers)]
    clause = " or ".join(exprs)
    return clause

def random_3sat(num_vars, num_clauses):
    """Return a random 3-SAT instance.

    The resulting problem is represented as a Python function,
    with NUM_VARS arguments. When applied to NUM_VARS boolean values,
    the function returns true if they constitute a satisfying assignment.
    """
    vars = [f"x_{i}" for i in range(num_vars)]

    clauses = ["(" + random_clause(vars) + ")" for _ in range(num_clauses)]

    body = " \\\n and ".join(clauses)
    header = "lambda " + ",".join(vars) + ": \\\n"
    problem = eval(header + body)
    problem.num_vars = num_vars
    return problem


def satisfy(problem):
    """Find a satisfying assignment for a given 3-SAT problem,
    or return None if no such assignment exists."""
    for assignment in product([True, False], repeat=problem.num_vars):
        if problem(*assignment):
            return assignment
    return None


import pandas as pd
import matplotlib.pyplot as plt
import seaborn as sns
import numpy as np

width = 5
height = 5
sns.set(rc={'figure.figsize':(width, height)})
sns.set_style("white")

def sat_experiment(num_vars, clause_range, sample_size=20):
    """Generate a number of random 3-SAT instances and tries to satisfy them.

    Returns a Pandas dataframe with three columns: 'num_vars', 'num_clauses',
    'satisfiable'. Here 'satisfiable' is a proportion (between 0 and 1), as
    observed over a number of samples.
    """
    data = []
    for num_clauses in clause_range:
        for i in range(sample_size):
            prob = random_3sat(num_vars, num_clauses)
            satisfiable = 1.0 if satisfy(prob) is not None else 0.0
            data.append([num_vars, num_clauses, satisfiable])
    df = pd.DataFrame(data, columns=['num_vars',
                                     'num_clauses',
                                     'satisfiable'])
    df = df.groupby(['num_vars', 'num_clauses'], as_index=False).mean()
    return df

def sat_plot(num_vars, filename=None):
    df = sat_experiment(num_vars, range(num_vars, 10*num_vars))
    df = df.groupby(['num_vars', 'num_clauses'], as_index=False).mean()
    df['clauses_per_variable'] = df['num_clauses'] / df['num_vars']
    sns.lmplot(x="clauses_per_variable", y="satisfiable", logistic=True,
               data=df, markers='.')
    plt.ylabel("Probability")
    plt.xlabel("Number of Clauses per Variable")
    plt.title(f"Satisfiability Probability ({num_vars} variables)")
    if filename is not None:
        plt.savefig(filename)
    else:
        plt.show()

def ideal_plot(filename=None):
    threshold = 4.2667
    df = pd.DataFrame([[ratio, 1.0 if ratio < threshold else 0.0]
                       for ratio in np.linspace(1, 9, 100)],
                      columns=['clauses_per_variable', 'satisfiable'])
    sns.lineplot(x='clauses_per_variable', y='satisfiable', data=df)
    sns.despine()
    plt.title("Satisfiability Probability (ideal limit)")
    plt.ylabel("Probability")
    plt.xlabel("Number of Clauses per Variable")
    if filename is not None:
        plt.savefig(filename)
    else:
        plt.show()