looking at 3-SAT phase transitions
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() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment