import inspect import itertools import random from pprint import pprint from grover import classical_func_search_multi_rv class X(object): """""" def __init__(self, i): self.i = i class SAT(object): def __init__(self, predicates=3): self.and_clauses = [] self.and_clauses_funcs = [] self.predicates = predicates def or_(self, or_clauses): def inner_or_(params): for or_clause in or_clauses: yes_no, var = or_clause[0], or_clause[1].i - 1 if yes_no(params[var]): return True return False return inner_or_ def and_(self, and_clauses): def inner_and_(params): for and_clause in and_clauses: if not and_clause(params): return False return True return inner_and_ def yes(self, x): return x def no(self, x): return not x def generate(self, ands=1): params = [X(i) for i in range(1, self.predicates + 1)] def or_clause(or_clauses): def inner_or_clause(params): return self.or_(or_clauses)(params) return inner_or_clause for _ in range(ands): or_clauses = list(zip(random.choices([self.yes, self.no], k=3), random.sample(params, k=3))) self.and_clauses.append(or_clauses) self.and_clauses_funcs.append(or_clause(or_clauses)) def inner_generate(args): return self.and_(self.and_clauses_funcs)(args) self.inner = inner_generate def __call__(self, args): return self.inner(args) def show(self): for j, _or_clause in enumerate(self.and_clauses): for i, predicate in enumerate(_or_clause): if i == 0: print("( ", end='') trueness, var = predicate if trueness == self.yes: print("x_{}".format(var.i), end='') else: print("¬x_{}".format(var.i), end='') if i + 1 != len(_or_clause): print(" ∨ ", end='') if j + 1 != len(self.and_clauses): print(" ) ∧ ") else: print(" )") def classical_3sat(func): # Generate all possible true/false tupples for the 3-sat problem input_range = list(itertools.product([True, False], repeat=func.predicates)) random.shuffle(input_range) return classical_func_search_multi_rv(func, input_range) def main(): rv = [] for _ in range(100): gen_3sat = SAT(predicates=4) gen_3sat.generate(ands=8) # gen_3sat.show() sols = classical_3sat(gen_3sat) rv.append(len(sols)) print(sorted(rv)) if __name__ == "__main__": main()