  It is crucial to generate crafted SAT formulas with predefined solutions for
the testing and development of SAT solvers since many SAT formulas from
real-world applications have solutions. Although some generating algorithms
have been proposed to generate SAT formulas with predefined solutions,
community structures of SAT formulas are not considered. We propose a 3-SAT
formula generating algorithm that not only guarantees the existence of a
predefined solution, but also simultaneously considers community structures and
clause distributions. The proposed 3-SAT formula generating algorithm controls
the quality of community structures through controlling (1) the number of
clauses whose variables have a common community, which we call intra-community
clauses, and (2) the number of variables that only belong to one community,
which we call intra-community variables. To study the combined effect of
community structures and clause distributions on the hardness of SAT formulas,
we measure solving runtimes of two solvers, gluHack (a leading CDCL solver) and
CPSparrow (a leading SLS solver), on the generated SAT formulas under different
groups of parameter settings. Through extensive experiments, we obtain some
noteworthy observations on the SAT formulas generated by the proposed
algorithm: (1) The community structure has little or no effects on the hardness
of SAT formulas with regard to CPSparrow but a strong effect with regard to
gluHack. (2) Only when the proportion of true literals in a SAT formula in
terms of the predefined solution is 0.5, SAT formulas are hard-to-solve with
regard to gluHack; when this proportion is below 0.5, SAT formulas are
hard-to-solve with regard to CPSparrow. (3) When the ratio of the number of
clauses to that of variables is around 4.25, the SAT formulas are hard-to-solve
with regard to both gluHack and CPSparrow.
