How to find a nearly-optimal covering of a set using SAT?
This problem is known as circuit minimization.  It falls within the broad area of logic synthesis.

The problem is known to be $\Sigma_2^P$-complete.  As a result, it is unlikely to be in NP (contrary to what you wrote).  And that means that it is unlikely to be solvable in polynomial time with queries to a SAT solver.  (NP is basically the class of problems you can solve with a SAT solver in a single query; $P^{NP}$ is the class of problems you can solve with an unlimited number of queries to a SAT solver; and $\Sigma_2^P$ is conjectured to be larger still, so a $\Sigma_2^P$-complete problem is conjectured not to be in NP or $P^{NP}$.)  There may still be heuristics that use a SAT solver along the way, but these heuristics either might make mistakes, might fail for some inputs, or might take exponentially long in some cases.

Anyway, there is a lot of literature on circuit minimization.  As far as I know, one standard approach is to use techniques built on Quine-McClusky, Espresso, etc.

You might be interested in approaches based on interpolation.  I believe those approaches use a SAT solver as a building block.