quantum/3sat.py

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()