Programs become more error-prone with inappropriate management of memory because of pointer aliasing, e.g., dereferencing null or dangling pointers, and memory leaks.PPTLSL is a two-dimensional(spatial and temporal) logic which integrates separation logic with PPTL(propositional projection temporal logic).It is useful to describe and verify temporal properties of list manipulating programs.This paper first gives an overview of PPTLSL, and then introduces the foundation of the tool SAT-PPTLSL in detail.SAT-PPTLSL can be used to check the satisfiability of PPTLSL formulas according to the "isomorphic" relationship between PPTLSL and PPTL.In addition, the paper presents examples to show the checking process of SAT-PPTLSL and analyze the effect of some key parameters on the performance of SAT-PPTLSL.