Created
April 22, 2019 02:41
-
-
Save braised-babbage/5f022f09a479446d9fa420838f2d6308 to your computer and use it in GitHub Desktop.
looking at 3-SAT phase transitions
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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