An LTL formula is satisfiable iff its tableau graph of maximal consistent atoms has a fulfilling path. Temporal expansion rules enforce local consistency, while recurrence conditions prevent infinite postponement of Until promises.