The SAT-based Approach to Separation Logic