A nice idea to learn a formula of symbols which can be evaluated logically for truth. But do they mention more general approaches such as using SAT solvers for this task? See Vijay Ganesh work.

This is just one specific type of the classes of satisfiability problems (a.k.a. search problems).

Other related problems include: Linear equation satisfiability, Linear inequality satisfiability, 0-1 integer linear equation satisfiability.

Given the current context (of search problems), all the above are known as NP problems in general (with the observation, that the classic definition of NP limited the scope to only YES-NO problems).

One can think of search problems as "one of many ways of characterizing the set of problems that form the basis of the study of intractability". Other ways include viewing such problems through the lenses of decision problems or optimization problems. In other words, problems in any of the aforementioned types can be translated between (or more formally, reduced to) each other with relative ease.

Source(s): http://algs4.cs.princeton.edu/66intractability/