Interesting logic problems
Rather than going to talk about algorithms and more about SAT, this answer tries to show that there is more than just one kind of logic and that there are also different kinds of approaches.

I won't go into detail much but rather provide a list with some topics and keywords that should form a good basis to do some research:



Higher order logic

There are many ways of extending the propositional logic as you know it, for example (first order logic) with the quantifiers $\forall$ and $\exists$ quantifiers.

Keywords: First/second order logic (with equality), free/bound variables, Skolem normal form



Type theory

This is basically just another higher order logic, but it's a very rich topic and in my opinion deserves its own category since it plays a special role in CS.

Keywords: $\Pi$-/$\Sigma$-types, subtypes, quotient types, Curry-Howard correspondence, (un)typed $\lambda$-calculus, System F, Martin-Löf type theory, $\lambda$-cube



Proof systems

These can vary from classical logic as you know, but can be more abstract working with other syntactical objects than Boolean values or predicates. Generally they define some set $\mathcal{X}$ of objects (formulas/syntax), a truth-assigning function $t: \mathcal{X} \to \{\texttt{false},\texttt{true}\}$ (defines semantics), some notion of proofs and a way to (efficiently) check whether a proof is valid.

Keywords: Completeness &amp; soundness, Gentzen/Hilbert style proofs, resolution calculus, Sequent calculus, Intuitionistic logic, Formal verification, temporal logic etc.



If this was not specific enough, here is one thing I found fascinating when I first learned about logic:

$$
\lnot \exists x . \forall y . \bigl ( F(x,y) \longleftrightarrow \lnot F(y,y) \bigr )
$$

The above formula is a tautology (ie. always true) for any domain $\mathcal{U}$ and predicate $F$. Now usually this is not very interesting, but


define $\mathcal{U}$ as the set of all sets, $F(x,y) = y \in x$ and we get Russell's paradox, or
define $\mathcal{U}$ some fixed enumeration of $\{0,1\}^\infty$, $F(x,y) = \text{$x$th bit of $y$}$ (now interpreting $\longleftrightarrow$ as equality on $\{0,1\}$) and we get Cantor's diagonalisation argument


which I find quite interesting.