We introduce a SAT enabled algorithm for checking language emptiness of alternating finite automata (AFA), with transition relation encoded symbolically in a form of (compactly represented) logical formulae. A SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors, and 2) store the antichain clauses in a special variant of trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art, and that the trie data structure may even be beneficial in general SAT solving.