Shortest Equivalent CNF Formula 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.
The problem of determining whether there is an equivalent CNF formula with at most a given number of literals is $\Pi_2^p$-complete.  The version minimizing the number of clauses is within a factor of $n$ of the formula size, where $n$ is the number of variables.  See section 6 of:


Christopher Umans, The Minimum Equivalent DNF Problem and Shortest Implicants, JCSS 63(4), 597–611, 2001.  doi:10.1006/jcss.2001.1775 (preprint)


A recent result shows that computing a particular lower bound for the size of the shortest equivalent CNF formula (measured by number of clauses, as you specify) is NP-complete.  This paper also states that your problem of minimizing the number of clauses is $\Pi^p_2$-complete as well, citing the Umans paper above, although why this follows is not immediately obvious to me.


Ondřej Čepek, Petr Kučera and Petr Savický, Boolean functions with a simple certificate for CNF complexity, DAM 160(4–5), 365–382, 2012.  doi:10.1016/j.dam.2011.05.013