發送短信 : Bridging Constraint Satisfaction and Boolean Satisfiability