# An introduction to propositional logic

Logic and proof theory are fields that study the formalization of logical statements and the structure of valid proofs. One of the most common ways to represent logical reasonings is with **propositional logic**.

A propositional formula is no more than what you normally use in your *if statements*, but without functions or predicates. The basic unit for these formulas are **literals**. Let's see some examples:

```
f = p ∧ q
```

Here ```p``` and ```q``` would be the literals. This formula means that *f* evaluates to ```True``` only when both ```p``` **and** ```q``` are True too. The ```∧``` operator is formally called **conjunction** and is often called **and**.

```
f = p ∨ q
```

This formula means that *f* evaluates to ```True``` only when any of ```p``` **or** ```q``` are  True. This includes the case when both are True. The ```∨``` operator is formally called **disjunction** and is often called **or**.

```
f = ¬p
```

The ```¬``` operator is analogous to the **not** operation. it evaluates to True only when its argument evaluates to False.

Normally, there are also two other operators called **implication** and **biconditional**, but we will ignore them for this kata (they can be expressed in terms of the other three anyways).

Once we know this, can construct what is called an **interpretation** in order to evaluate a propositional formula. This is a fancy name for any structure that tells us which literals are False and which ones are True. Normally, interpretations are given as a set:

```python
p = Literal('p')
q = Literal('q')
r = Literal('r')

f = p ∨ q ∨ ¬r

i_1 = {p, q} # p and q are True, r is False
i_2 = {r}    # r is True, p and q are False
i_3 = {}     # p, q and r are False

# Note: the 'evaluate' function is not given
evaluate(f, i_1) == True
evaluate(f, i_2) == False
evaluate(f, i_3) == True
```

As you can see, if the literal is in the set, we say it evaluates to True, else it is False.

As a final note, an interpretation that makes a formula True is called a **model** when all the literals in the set appear in the formula.

# The SAT problem

This is a famous NP problem that is stated as follows:

> Given a propositional formula *F*, does it exist an interpretation such that it evaluates to True? (i.e. is *F* **satisfiable**?)

Numerous algorithms exist for this purpose, and your task is to program one of them. Right now, you are not supposed to program an efficient algorithm, but I may create a performance version if this kata gets good reception :)

# Specification

Program a ```sat(f: Formula)``` function that returns the following:
- ```False``` if ```f``` is not satisfiable.
- An interpretation that makes ```f``` evaluate to True in the case that it is satisfiable.

# Preloaded code

You are given a class ```Formula``` that has the following members:

- ```args```: arguments of the operation if the formula is not a literal (children nodes of the formula's tree). They are given as a list of Formula objects that has one element in the case of the negation operator and two or more elements in the case of the conjunction and disjunction operators.
- ```is_literal()```: True if the formula is a literal (i.e. not an operation).
- ```is_and()```: True if the formula is a **conjunction**.
- ```is_or()```: True if the formula is a **disjunction**. 
- ```is_not()```: True if the formula is a **negation**. 

You are also given a class ```Literal``` that extends from ```Formula``` and has the following members:

- ```name```: string that represents the literal. Two literals with the same name **are the same literal**.
*Note: the rest of members are not guaranteed in the case of a literal*

The ```&``` operator is overloaded as the conjunction, ```|``` as the disjunction and ```~``` as the negation. Also, a ```__repr__``` function is given for debugging purposes.

# Extra examples

```
f = ¬(p ∨ q) # Satisfiable with {}
```
```
f = ¬(p ∧ q) # Satisfiable with {p}, {q} and {}
```
```
f = p ∧ (q ∨ r) # Satisfiable with {p, q}, {p, r} and {p, q, r}
```
```
f = ¬p ∨ ¬q # Satisfiable with {p}, {q} and {} (See De Morgan's Laws)
```
```
f = p ∧ ¬p # Not satisfiable
```

Difficulty: introductory

Starter code:

def sat(f:
	

Solutions:
from itertools import compress, product, chain
from functools import partial

def check(f, s):
    if f.is_literal(): return f in s
    elif f.is_and(): return all(check(e, s) for e in f.args)
    elif f.is_or(): return any(check(e, s) for e in f.args)
    elif f.is_not(): return not check(f.args[0], s)

def get_name(f):
    if f.is_literal(): yield f
    else: yield from chain.from_iterable(map(get_name, f.args))

def sat(f):
    s = set(get_name(f))
    return next(filter(partial(check, f), map(set, map(partial(compress, s), product((0,1), repeat=len(s))))), False)

from itertools import product

def sat(f: Formula):

    def getLiterals(f,s):
        if f.is_literal(): s.add(f)
        else:
            for n in f.args: getLiterals(n,s)
        return s
        
    def evaluate(f,bools):
        return ( bools[f] if f.is_literal() else 
                 any(evaluate(n,bools) for n in f.args) if f.is_or() else
                 all(evaluate(n,bools) for n in f.args) ^ f.is_not() )
                 
    lst = list(getLiterals(f,set()))
    for p in product([0,1],repeat=len(lst)):
        bools = dict(zip(lst,p))
        if evaluate(f,bools):
            return {n for n,v in bools.items() if v}
    return False

from itertools import combinations
from typing import Iterable, List

def literals(f: Formula) -> List[Literal]:
    if f.is_literal():
        return [f]
    return [x for g in f.args for x in literals(g)]
    
def evaluate(f: Formula, i: Iterable[Literal]) -> bool:
    if f.is_literal():
        return f in i
    if f.is_not():
        return not evaluate(f.args[0], i)
    args = (evaluate(g, i) for g in f.args)
    if f.is_and():
        return all(args)
    if f.is_or():
        return any(args)

def sat(f: Formula):
    lits = set(literals(f))
    n = len(lits)
    for r in range(0, n + 1):
        for i in combinations(lits, r):
            if evaluate(f, set(i)):
                return set(i)
    return False

def sat(f: Formula):
    literals = total_literals(f, {})
    length = len(literals)

    for b in range(2**length):
        table = {i:int(j) for i,j in zip(literals.keys(), bin(b)[2:].zfill(length))}
        if satisfiable(f, table):
            return {literals[i] for i in table if table[i]}
    return False
    
def total_literals(f, lit):
    for i in f.args:
        if i.is_literal() : lit[i.name] = i
        else : total_literals(i, lit)
    return lit

def satisfiable(f, table):
    if f.is_literal() : return table[f.name]
    if f.is_and() : return all(satisfiable(i,table) for i in f.args)
    if f.is_or()  : return any(satisfiable(i,table) for i in f.args)
    return not satisfiable(f.args[0], table)

from itertools import product
def sat(f: Formula):
    t=lambda f,s=set():s.add(f) or s if f.is_literal() else list(map(t,f.args)) and s
    e=lambda f,d:d[f] if f.is_literal() else any(e(n,d)for n in f.args) if f.is_or() else all(e(n,d)for n in f.args)^f.is_not()
    lst = list(t(f))
    return next(({n for n in d if d[n]} for p in product([0,1],repeat=len(lst)) for d in [dict(zip(lst,p))] if e(f,d)), False)

from itertools import product

def evaluate(self):
    return ( self.val if self.is_literal() else
             all(n.evaluate() for n in self.args) if self.is_and() else
             any(n.evaluate() for n in self.args) if self.is_or() else
             not self.args[0].evaluate() )

Formula.evaluate=evaluate


def sat(f: Formula):
    
    def travel(f):
        if f.is_literal(): s.add(f)
        else:              
            for n in f.args:
                travel(n)
    
    s=set()
    travel(f)
    lst = list(s)
    for p in product([0,1], repeat=len(lst)):
        s=set()
        for n,v in zip(lst,p):
            n.val=v
            if v: s.add(n)
        if f.evaluate(): return s
    return False

def sat(f: Formula):
    literals = total_literals(f, {})
    length = len(literals)

    for b in range(2**length):
        table = {i:int(j) for i,j in zip(list(literals.keys()), bin(b)[2:].zfill(length))}
        if satisfiable(f, table):
            return {literals[i] for i in table if table[i]}
    return False
    
def total_literals(f, lit):
    for i in f.args:
        if i.is_literal() : lit[i.name] = i
        else : total_literals(i, lit)
    return lit 

def satisfiable(f, table):
    if f.is_literal() : return table[f.name]
    x = [satisfiable(i,table) for i in f.args]    
    return all(x) if f.is_and() else any(x) if f.is_or() else not all(x)

#very INeffecient


from itertools import combinations

def sat(f: Formula) -> set or False:
    def eval_sat(f: Formula, true_vars: set) -> bool:
        if f.is_literal():
            return f in true_vars
        elif f.is_and():
            return all(eval_sat(ff, true_vars) for ff in f.args)
        elif f.is_or():
            return any(eval_sat(ff, true_vars) for ff in f.args)
        elif f.is_not():
            return not eval_sat(*f.args, true_vars)
    
    def get_vars(f: Formula) -> set:
        if f.is_literal():
            return {f}
        else:
            return set(var for ff in f.args for var in get_vars(ff))
    
    variables = get_vars(f)
    for i in range(len(variables) + 1):
        for true_vars in map(set, combinations(variables, i)):
            if eval_sat(f, true_vars):
                return true_vars
    return False

from itertools import combinations


def sat(f: Formula):
    
    literals = set()
    allLiterals(f, literals)
    all_lit = list(literals)
    for i in range (0, len(all_lit)+1):
        lit_comb = set(combinations(all_lit, i))
        for j in lit_comb:
            if evaluate(f, j): return set(j)
    return False
    

def evaluate(f: Formula, inter):

    if f.is_literal():
        if f in inter:
            return True
        else:
            return False
    elif f.is_and(): 
        flag = True
        for i in f.args:
            flag = flag and evaluate(i, inter)
        return flag
    elif f.is_or():
        flag = False
        for i in f.args:
            flag = flag or evaluate(i, inter)
        return flag
    else: return (not evaluate(f.args[0], inter))
    

def allLiterals(f: Formula, lit_set):

    for i in f.args:
        if i.is_literal(): lit_set.add(i)
        else: allLiterals(i, lit_set)

def _sat_and(models1, models2):
    models = []
    for model1 in models1:
        for model2 in models2:
            candidate = (model1[0] | model2[0], model1[1] | model2[1])
            if candidate[0] & candidate[1] == set():
                models.append(candidate)
    return models

def _sat_not(f: Formula):
    if f.is_literal():
        return [(set(), {f})]
    if f.is_not():
        return _sat(f.args[0])
    if f.is_and():
        return [option for arg in f.args for option in _sat_not(arg)]
    if f.is_or():
        models = [(set(), set())]
        for arg in f.args:
            models = _sat_and(models, _sat_not(arg))
        return models
    

def _sat(f: Formula):
    if f.is_literal():
        return [({f}, set())]
    if f.is_not():
        return _sat_not(f.args[0])
    if f.is_or():
        return [option for arg in f.args for option in _sat(arg)]
    if f.is_and():
        models = [(set(), set())]
        for arg in f.args:
            models = _sat_and(models, _sat(arg))
        return models
    
        

def sat(f: Formula):
    options = _sat(f)
    if len(options) == 0:
        return False
    return options[0][0]