# 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
```

Source: codewars | Difficulty: EASY
Tags: Mathematics

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


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]