Modal SAT: Introduction — LessWrong