The input is a Boolean formula in $2-$CNF$,$ given as a string of symbols. A literal is a variable name $($at least any small Latin letter should be a legal variable name$)$ or its negation, denoted by ~$.$ A clause is either a literal, or $($L$1\backslash /$ L$2),$ or $($L$1->$ L$2),$ where L$1$ and L$2$ are literals. Finally, the $2-$CNF is either one clause or a conjunction of two or more clauses, where conjunction is denoted by $/\backslash .$

Example: p $/\backslash ($p $->$ q$)/\backslash ($p $->$ ~r$)/\backslash ($~r $\backslash /$ ~s$)/\backslash ($s $\backslash /$ ~q$)$

The first task is to check whether the given $2-$CNF is satisfiable. The second task is$,$ given a $2-$CNF$,$ report that it is not satisfiable or return one of its satisfying assignments. Solving only the first task gives you a half grade $(2$ points out of $4).$ Solving both gives $4$ points.

Technical Details

In order for the automated test to work fine, please carefully adhere the following technical instructions. Your solution should be implemented in Python$3,$ in a file named boolean.py$.$ For the first task, you should implement a function called is$\_$satisfiable, which takes the string with the $2-$CNF as an argument and returns either True $($satisfiable$)$ or False $($not satisfiable$).$ The second task should be implemented as a function called sat$\_$assignment. This function also takes one argument $($string$)$ and returns an associative array $($dictionary$)$ with the satifying assignment $($e$.$g$.,\{\text{'}$p$\text{'}$: True, $\text{'}$q$\text{'}$: False, $\text{'}$r$\text{'}$: True $\})$ or None, if the $2-$CNF is not satisfiable.

Warning: the automatic tests run several iterations of your functions, with different CNFs$.$ If you use global variables, please make sure that their values from previous iterations do not make the next one work incorrectly.