This is the original NP-complete problem (Karp's problem 1).

In this problem, the input is a boolean formula written in conjunctive normal form (CNF).  The output is either an assignment of boolean values that makes the boolean formula true of an elaborate proof that there is no satisfying assignment.

It turns out that it's possible to express any CNF formula in such a way that each clause contains only 3 literals.  In that case, it's a different variation of the problem: 3-sat (Karp's problem 13).

Here is a youtube video describing the problem: https://youtu.be/sCxmi9ZLmdc

There's a mountain of information available about boolean satisfiability.  There's no easy way to summarize it.

I personally would be more interested in a sat solver that took any propositional formula as an input and solved it without necessarily converting to CNF.  Converting disjunctive normal form (DNF) to CNF for satisfiability would be stupid, but I've been told that it's not as big of a deal as I think.  My instinct is that working on this particular version of satisfiability may be making the problem harder, but there isn't any solid evidence to back that up.