# -*- coding: utf-8 -*-
"""aitp_hw1.ipynb

Automatically generated by Colaboratory.

Original file is located at
    https://colab.research.google.com/drive/1BbD02FIRu5SaeLIGTfQbStnf4hPiKqms

# DP and DPLL with various heuristics comparision

author: <NAME> <<EMAIL>>

## Types
"""

from typing import MutableSet, FrozenSet, Iterable, List
# I represent the CNF formula as a frozenset of frozen sets
Literal = int
Clause = FrozenSet[Literal]
CNF = FrozenSet[Clause]

# Helper Functions
def to_list(cnf: CNF) -> List[List[Literal]]:
    return list(map(list, cnf))

def from_lists(cnf: Iterable[Iterable[Literal]]) -> CNF:
    return frozenset(map(frozenset, cnf))

"""## Base algorithm"""

from typing import Tuple, Callable
class BaseAlgorithm:
    @staticmethod
    def is_tautology(c: Clause) -> bool:
        return not c.isdisjoint(frozenset(map(lambda l: -l, c)))

    @staticmethod
    def get_singleton_literals(cnf: CNF) -> FrozenSet[Literal]:
        literals = set()
        for c in cnf:
            if len(c) == 1:
                literals |= c
        return frozenset(literals)
    
    @classmethod
    def tatuology_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        # We return False, because the tatutology rule is the first one, so
        # there is no point in trying it again if only it succeded
        return frozenset(filter(lambda c: not cls.is_tautology(c), cnf)), False

    @classmethod
    def unit_clause_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        singleton_literals = cls.get_singleton_literals(cnf)
        # I process all the singleton literals at once. I am awere that is is
        # different than the classical iteration and it can be easilly changed
        # if needed.
        # To process all the singleton literals at once we cannot process l 
        # and -l at the same time.
        singleton_literals = frozenset(filter(
            lambda l: -l not in singleton_literals or l > 0, singleton_literals))
        neg_singleton_literals = frozenset(map(lambda l: -l, singleton_literals))
        if singleton_literals:
            return frozenset(c - neg_singleton_literals for c in cnf if 
                             c.isdisjoint(singleton_literals)), True
        else:
            return cnf, False

    @classmethod
    def pure_literal_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        # union needs nonzero number of parameters
        if not cnf:
            return cnf, True
        # I process all one_sign_literals at once. I am awere that it is
        # different than the classical iteration and it can be easilly changed
        # if needed.
        all_literals = frozenset.union(*cnf)
        one_sign_literals = frozenset(
            filter(lambda l: -l not in all_literals, all_literals))
        if one_sign_literals:
            return frozenset(c for c in cnf if c.isdisjoint(one_sign_literals)), True
        else:
            return cnf, False

    @classmethod
    def simplify(cls, cnf: CNF) -> Tuple[CNF, bool]:
        simplified_acc = False
        for simplifier in [cls.tatuology_rule, 
                           cls.unit_clause_rule, 
                           cls.pure_literal_rule]:
            cnf, simplified = simplifier(cnf)
            simplified_acc |= simplified
        return cnf, simplified_acc

    def run(self, cnf: CNF) -> bool:
        # return satisfiability if there are no clauses
        if not cnf:
            return True            
        # return unsatisfiability if there is an empty clause
        for c in cnf:
            if not c:
                return False
        # try to simplify formula
        cnf, simplified, = self.simplify(cnf)
        if not simplified:
            return self.core_function(cnf)
        else:
            return self.run(cnf)

    @staticmethod
    def parse_preambule(preambule: str) -> Tuple[int, int]:
        preambule =  preambule.strip().split()
        line_start, format_name = preambule[0], preambule[1]
        if line_start != "p" or format_name != "cnf":
            raise NotImplementedError("File format not supported: " + format_name)
        no_variables, no_clauses = int(preambule[2]), int(preambule[3])
        return no_variables, no_clauses

    @classmethod
    def get_cnf_from_file(cls, fn: str) -> Tuple[int, int, CNF]:
        with open(fn) as f:
            lines = f.readlines()
        # filter comments
        lines = list(filter(lambda line: line[0] != 'c', lines))
        # Parse preambule
        no_variables, no_clauses = cls.parse_preambule(lines[0])
        # Split to clauses
        data = " ".join(lines[1:]).strip().split()
        clauses, clause, clauses_counter = set(), set(), 0
        for x in data:
            if x == "0":
                clauses.add(frozenset(clause))
                clause = set()
                clauses_counter += 1
                if clauses_counter == no_clauses:
                    break
            else:
                clause.add(int(x))
        return no_variables, no_clauses, frozenset(clauses)

    def __call__(self, fn: str) -> None:
        (_, _, cnf) = self.get_cnf_from_file(fn)
        if self.run(cnf):
            print("SAT")
        else:
            print("UNSAT")

    def core_function(self, cnf: CNF) -> bool:
        raise NotImplemented("This is an abstract class")

class AlgorithmWithLiteralChoosingHeuristic(BaseAlgorithm):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        self.literal_heuristic = literal_heuristic

    def core_function(self, cnf: CNF) -> bool:
        l = self.literal_heuristic(cnf)
        return self.core_function_with_literal_heurstic(l, cnf)
    
    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        raise NotImplemented("This is an abstract class")

"""## The algoritms

### DP algorithm
"""

class DP(AlgorithmWithLiteralChoosingHeuristic):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        super().__init__(literal_heuristic)

    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        l_and_neg_l = frozenset({l, -l})
        c_with_l = frozenset(c - l_and_neg_l for c in cnf if l in c)
        c_with_neg_l = frozenset(c - l_and_neg_l for c in cnf if -l in c)
        resolvents = frozenset(c1.union(c2) for c1 in c_with_l for c2 in c_with_neg_l)
        cnf = resolvents.union(filter(l_and_neg_l.isdisjoint, cnf))
        return self.run(cnf)

"""### DPLL algorithm"""

class DPLL(AlgorithmWithLiteralChoosingHeuristic):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        super().__init__(literal_heuristic)

    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        if self.run(cnf | frozenset({frozenset({l})})):
            return True
        return self.run(cnf | frozenset({frozenset({-l})}))

"""### Selected algorithms"""

algorithms = {"DPLL": DPLL, "DP": DP}

"""## Heuristics for choosing a literal

### A helper function
"""

from typing import Dict
# Helper functions
def count_literals(cnf: CNF) -> Dict[Literal, int]:
    counts = {}
    for c in cnf:
        for l in c:
            counts[l] = counts.get(l, 0) + 1
    return counts

"""### The heuristics implementation"""

def first_of_first(cnf: CNF) -> Literal:
    for c in cnf:
        for l in c:
            return l

def most_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    return max(counts.items(), key=lambda x: x[1])[0]

def least_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    return min(counts.items(), key=lambda x: x[1])[0]

def middle_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    # It is possible to do is in O(n) time, but here is O(n * log(n)) solution
    return sorted(counts.items(), key=lambda x: x[1])[len(counts) // 2][0]

"""### Selected heuristics"""

heuristics = {"first_of_first": first_of_first, 
              "most_common": most_common, 
              "least_common": least_common, 
              "middle_common": middle_common}
# -*- coding: utf-8 -*-
"""aitp_hw1.ipynb

Automatically generated by Colaboratory.

Original file is located at
    https://colab.research.google.com/drive/1BbD02FIRu5SaeLIGTfQbStnf4hPiKqms

# DP and DPLL with various heuristics comparision

author: <NAME> <<EMAIL>>

## Types
"""

from typing import MutableSet, FrozenSet, Iterable, List
# I represent the CNF formula as a frozenset of frozen sets
Literal = int
Clause = FrozenSet[Literal]
CNF = FrozenSet[Clause]

# Helper Functions
def to_list(cnf: CNF) -> List[List[Literal]]:
    return list(map(list, cnf))

def from_lists(cnf: Iterable[Iterable[Literal]]) -> CNF:
    return frozenset(map(frozenset, cnf))

"""## Base algorithm"""

from typing import Tuple, Callable
class BaseAlgorithm:
    @staticmethod
    def is_tautology(c: Clause) -> bool:
        return not c.isdisjoint(frozenset(map(lambda l: -l, c)))

    @staticmethod
    def get_singleton_literals(cnf: CNF) -> FrozenSet[Literal]:
        literals = set()
        for c in cnf:
            if len(c) == 1:
                literals |= c
        return frozenset(literals)
    
    @classmethod
    def tatuology_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        # We return False, because the tatutology rule is the first one, so
        # there is no point in trying it again if only it succeded
        return frozenset(filter(lambda c: not cls.is_tautology(c), cnf)), False

    @classmethod
    def unit_clause_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        singleton_literals = cls.get_singleton_literals(cnf)
        # I process all the singleton literals at once. I am awere that is is
        # different than the classical iteration and it can be easilly changed
        # if needed.
        # To process all the singleton literals at once we cannot process l 
        # and -l at the same time.
        singleton_literals = frozenset(filter(
            lambda l: -l not in singleton_literals or l > 0, singleton_literals))
        neg_singleton_literals = frozenset(map(lambda l: -l, singleton_literals))
        if singleton_literals:
            return frozenset(c - neg_singleton_literals for c in cnf if 
                             c.isdisjoint(singleton_literals)), True
        else:
            return cnf, False

    @classmethod
    def pure_literal_rule(cls, cnf: CNF) -> Tuple[CNF, bool]:
        # union needs nonzero number of parameters
        if not cnf:
            return cnf, True
        # I process all one_sign_literals at once. I am awere that it is
        # different than the classical iteration and it can be easilly changed
        # if needed.
        all_literals = frozenset.union(*cnf)
        one_sign_literals = frozenset(
            filter(lambda l: -l not in all_literals, all_literals))
        if one_sign_literals:
            return frozenset(c for c in cnf if c.isdisjoint(one_sign_literals)), True
        else:
            return cnf, False

    @classmethod
    def simplify(cls, cnf: CNF) -> Tuple[CNF, bool]:
        simplified_acc = False
        for simplifier in [cls.tatuology_rule, 
                           cls.unit_clause_rule, 
                           cls.pure_literal_rule]:
            cnf, simplified = simplifier(cnf)
            simplified_acc |= simplified
        return cnf, simplified_acc

    def run(self, cnf: CNF) -> bool:
        # return satisfiability if there are no clauses
        if not cnf:
            return True            
        # return unsatisfiability if there is an empty clause
        for c in cnf:
            if not c:
                return False
        # try to simplify formula
        cnf, simplified, = self.simplify(cnf)
        if not simplified:
            return self.core_function(cnf)
        else:
            return self.run(cnf)

    @staticmethod
    def parse_preambule(preambule: str) -> Tuple[int, int]:
        preambule =  preambule.strip().split()
        line_start, format_name = preambule[0], preambule[1]
        if line_start != "p" or format_name != "cnf":
            raise NotImplementedError("File format not supported: " + format_name)
        no_variables, no_clauses = int(preambule[2]), int(preambule[3])
        return no_variables, no_clauses

    @classmethod
    def get_cnf_from_file(cls, fn: str) -> Tuple[int, int, CNF]:
        with open(fn) as f:
            lines = f.readlines()
        # filter comments
        lines = list(filter(lambda line: line[0] != 'c', lines))
        # Parse preambule
        no_variables, no_clauses = cls.parse_preambule(lines[0])
        # Split to clauses
        data = " ".join(lines[1:]).strip().split()
        clauses, clause, clauses_counter = set(), set(), 0
        for x in data:
            if x == "0":
                clauses.add(frozenset(clause))
                clause = set()
                clauses_counter += 1
                if clauses_counter == no_clauses:
                    break
            else:
                clause.add(int(x))
        return no_variables, no_clauses, frozenset(clauses)

    def __call__(self, fn: str) -> None:
        (_, _, cnf) = self.get_cnf_from_file(fn)
        if self.run(cnf):
            print("SAT")
        else:
            print("UNSAT")

    def core_function(self, cnf: CNF) -> bool:
        raise NotImplemented("This is an abstract class")

class AlgorithmWithLiteralChoosingHeuristic(BaseAlgorithm):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        self.literal_heuristic = literal_heuristic

    def core_function(self, cnf: CNF) -> bool:
        l = self.literal_heuristic(cnf)
        return self.core_function_with_literal_heurstic(l, cnf)
    
    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        raise NotImplemented("This is an abstract class")

"""## The algoritms

### DP algorithm
"""

class DP(AlgorithmWithLiteralChoosingHeuristic):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        super().__init__(literal_heuristic)

    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        l_and_neg_l = frozenset({l, -l})
        c_with_l = frozenset(c - l_and_neg_l for c in cnf if l in c)
        c_with_neg_l = frozenset(c - l_and_neg_l for c in cnf if -l in c)
        resolvents = frozenset(c1.union(c2) for c1 in c_with_l for c2 in c_with_neg_l)
        cnf = resolvents.union(filter(l_and_neg_l.isdisjoint, cnf))
        return self.run(cnf)

"""### DPLL algorithm"""

class DPLL(AlgorithmWithLiteralChoosingHeuristic):
    def __init__(self, literal_heuristic: Callable[[CNF], Literal]) -> None:
        super().__init__(literal_heuristic)

    def core_function_with_literal_heurstic(self, l: Literal, cnf: CNF) -> bool:
        if self.run(cnf | frozenset({frozenset({l})})):
            return True
        return self.run(cnf | frozenset({frozenset({-l})}))

"""### Selected algorithms"""

algorithms = {"DPLL": DPLL, "DP": DP}

"""## Heuristics for choosing a literal

### A helper function
"""

from typing import Dict
# Helper functions
def count_literals(cnf: CNF) -> Dict[Literal, int]:
    counts = {}
    for c in cnf:
        for l in c:
            counts[l] = counts.get(l, 0) + 1
    return counts

"""### The heuristics implementation"""

def first_of_first(cnf: CNF) -> Literal:
    for c in cnf:
        for l in c:
            return l

def most_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    return max(counts.items(), key=lambda x: x[1])[0]

def least_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    return min(counts.items(), key=lambda x: x[1])[0]

def middle_common(cnf: CNF) -> Literal:
    counts = count_literals(cnf)
    # It is possible to do is in O(n) time, but here is O(n * log(n)) solution
    return sorted(counts.items(), key=lambda x: x[1])[len(counts) // 2][0]

"""### Selected heuristics"""

heuristics = {"first_of_first": first_of_first, 
              "most_common": most_common, 
              "least_common": least_common, 
              "middle_common": middle_common}
# -*- coding: utf-8 -*- aitp_hw1.ipynb  Automatically generated by Colaboratory.  Original file is located at     https://colab.research.google.com/drive/1BbD02FIRu5SaeLIGTfQbStnf4hPiKqms  # DP and DPLL with various heuristics comparision  author: <NAME> <<EMAIL>>  ## Types # I represent the CNF formula as a frozenset of frozen sets # Helper Functions ## Base algorithm # We return False, because the tatutology rule is the first one, so # there is no point in trying it again if only it succeded # I process all the singleton literals at once. I am awere that is is # different than the classical iteration and it can be easilly changed # if needed. # To process all the singleton literals at once we cannot process l # and -l at the same time. # union needs nonzero number of parameters # I process all one_sign_literals at once. I am awere that it is # different than the classical iteration and it can be easilly changed # if needed. # return satisfiability if there are no clauses # return unsatisfiability if there is an empty clause # try to simplify formula # filter comments # Parse preambule # Split to clauses ## The algoritms  ### DP algorithm ### DPLL algorithm ### Selected algorithms ## Heuristics for choosing a literal  ### A helper function # Helper functions ### The heuristics implementation # It is possible to do is in O(n) time, but here is O(n * log(n)) solution ### Selected heuristics