Skip to content

Instantly share code, notes, and snippets.

@kilimanjaro

kilimanjaro/3sat.py

Created Apr 22, 2019
Embed
What would you like to do?
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