It means satisfiability problem. You can think of it as one "assembly language" of optimization, in the sense that many higher-order problem formulations can be "compiled" to SAT.