Let $F_1$ be a satisfiable CNF Formula with $n$ variables and $m$ clauses. Let $S_{F_1}$ be the solution space of $F_1$.
Consider the problem of determining, given $F_1$, another CNF Formula $F_2$ with the same set of variables as $F_1$, with $S_{F_2} = S_{F_1}$ (same solution space as $F_1$), but with as few clauses as possible (the only aim is to minimize the number of clauses, so how many literals each clause may have is not relevant).
Question
Did anyone already investigated this problem? Are there any results in the literature concerning it?
As an example, consider the following CNF Formula $F_1$ (each row is a clause):
$x_1 \lor x_2 \lor x_3$
$x_2 \lor x_3 \lor x_4$
$\lnot x_1 \lor x_2 \lor x_4$
$\lnot x_1 \lor x_2 \lor \lnot x_3$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2 \lor \lnot x_5$
and the following formula $F_2$:
$x_1 \lor x_2 \lor x_3$
$x_2 \lor x_3 \lor x_4$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2$
both have the same solution space, but while $F_1$ has $6$ clauses, $F_2$ only has $4$.
Finally, consider the following formula $F_3$:
$x_2 \lor x_3$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2$
The solution space is again the same, but with only $3$ clauses.