Is there a typical amount of clauses (in a 3CNF SAT expression)? Do SAT solvers regularlary solve expressions (or attempt to) with many?

Question

I'm curious as to in what settings we would be interested in finding out whether a boolean expression in 3CNF with a large number of clauses is satisfiable (I''m not sure how "large number" is defined though, that's kind of my question)?

Would an expression with 5000 clauses and 2000/3000/4000 variables be considered large?

I realize it'll take, at worst, a great exponential amount of time. But are there specific fields/situations where solving such an expression would be useful, nonetheless?

Actually, wikipedia says there could be, in practice, 100,000 variables. In what areas is this needed?

Answer 1

For a practical example, consider this academic (but very real and useful) problem : You have

1. 50 teachers
2. 50 students groups
3. 50 Rooms
4. 20 possible times for course during week
5. Several teachings
6. Many constraints

Each constraints can be (for example) :

1. A teacher will only teach some courses (He can't or didn't want to do some teachings)
2. A teacher will not be always available each day of each week
3. A room can only have one class at a time
4. Each course need a teacher
5. And so on.....

And you need to make a time table with all courses provided to the appropriate students groups...

Each variable will correspond to : That class with that teacher in that room at that time. So you obtain a very large amount of variables and constraints with a fairly small structure (Here $50\times 50\times 20\times 50$ but most universities have thousands of students and teachers)...

Will you find a time table that matches all constraints ?