Minimum viable product TODO:

[X] SAT solver:

    [X] DPLL algo
    [] Proof for SAT
    [] (Optional) Proof for UNSAT
    [] (Optional) 2-SAT polynomial time algorithm
    [] (Optional) Conflict driven

[X] Tseiten transformation

[X] Expr parsing:

    [X] Operators: and, or, not, (core) xor, nor, nand, if, iff (built on core)

[X] Expr evaluation

[X] Truth table generation


Not quite part of MVP TODO:

[X] Free with SAT solver:
    
    [X] Tautology checker
    [X] Contradiction checker
    [X] Logical equivalence
    [X] Argument checking

[X] Explict expr building from other exprs
    - Engine.or, Engine.and, ...

Maybe in future TODO:

[] Term rewritting/expr simplification

engine.gen_truth_table(engine.parse("x or y"))


Implementation plan:

* Parser: recursive decent
* Evaluation of proposition: bytecode vm


Example brainstorming

* General API: 


``
import * from easypls

engine = Engine()

# Variable definition
x = engine.def("x", True)

# Expr parsing and evaulation
expr = Expr.parse("x or x")
print(engine.eval(expr))                            # Prints "True"

# Logical equivilace checking
engine.logically_eq(x, expr)                        # Returns True

# CNF conversion
cnf = Expr.parse("a -> b").into_cnf()

# SAT Solver
engine.is_sat(cnf)                                  # Returns True

args = [
    Expr.parse("a -> b"),
    Expr.parse("a"),
]

a = Expr.var("a")
b = Expr.var("b")

raw_cnf = engine.cnf_from_arr([[a, b], [a, b.negated()]])
new_cnf = engine.condition(a, Bool.T)

conclusion = engine.parse("b")

engine.is_valid_argument(args, conclusion)          # Returns True

`
