How to find a nearly-optimal covering of a set using SAT? I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem.

I think one of the interesting problems where SAT solvers can be used is finding a minimal representation for a logic expression. However, I have trouble encoding the problem into a SAT problem.

In very old representations of an n-input logic circuit, three sets F, R, and D are defined. F represents the ON-set, which corresponds to permutations of input that cause a one in the output. R is the OFF-set, which corresponds to permutations of input that cause a zero in the output. Finally, D is the DON'T CARE-set which corresponds to permutations of input where output is not specified (could be set to either one or zero during optimization).

The objective is to find a minimal conjunctive normal form (CNF) that has the minimum number of clauses and each clause has the minimum number of literals. This CNF should cover all elements of F and may potentially cover some elements of D, but should not cover any elements of R.

For example, assume that a 3-input function is defined in the following way:

A B C | Y
---------
0 0 0 | 0
0 0 1 | 0
0 1 0 | 1
0 1 1 | 1
1 0 0 | -
1 0 1 | -
1 1 0 | -
1 1 1 | -


where A, B, and C are inputs, Y is the output, and a - determines a don't care output.

In this problem, a minimal CNF that meets the objective is O = B, because whenever B is true, the output is either true or don't care, but never false. Without having the DON'T CARE-set, a minimal representation would be O = ~A B, but DON'T CARE-set has allowed a more compact representation.

Is there a method to encode this problem as a SAT problem where inputs are F and R?
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.