A logical formula is satisfiable if there exists a ["Model"].