We consider the satisfiability problem for CNF instances that contain a (hidden) Horn or a generalized (hidden) Horn part and a $k$-CNF part, called {\em mixed} formulas. We show that SAT remains NP-complete for such instances and also that any SAT instance can be endcoded in terms of a mixed formula in polynomial time. We prove non-trivial worst case bounds by providing exact deterministic algorithms exploiting graph structures inherent in the mixed instances. Particularly, we provide an exact deterministic algorithm showing that SAT for instances composed of a Horn part and a 2-CNF part is solvable in time $O(2^{0.5284n})$. Motivating for these investigations are level graph formulas which are mixed Horn formulas.