  Recent years have witnessed a wide array of results in software testing,
exploring different approaches and methodologies ranging from fuzzers to
symbolic engines, with a full spectrum of instances in between such as concolic
execution and hybrid fuzzing. A key ingredient of many of these tools is
Satisfiability Modulo Theories (SMT) solvers, which are used to reason over
symbolic expressions collected during the analysis. In this paper, we
investigate whether techniques borrowed from the fuzzing domain can be applied
to check whether symbolic formulas are satisfiable in the context of concolic
and hybrid fuzzing engines, providing a viable alternative to classic SMT
solving techniques. We devise a new approximate solver, FUZZY-SAT, and show
that it is both competitive with and complementary to state-of-the-art solvers
such as Z3 with respect to handling queries generated by hybrid fuzzers.
