Separation of limited nondeterminism classes? It is interesting to find the best lower bound on the  number of nondeterministic bits needed to solve satisfiability problem. Let $\beta_k P$ be the class of problems solvable by a  nondeterministic Turing machine in polynomial time and using $O(\log^k n)$ nondeterministic bits.

$P=\beta_1P$. Notice that $O(\log n)$-clique
 is in $\beta_2P$. 
It is an open problem whether $\beta_1 P = \beta_2 P$. It is known that
$\beta_1P \neq \beta_2P$ implies $P \neq NP$


  What is the most serious attempt at separating  $\beta_1P$ from $\beta_2P$?


Does $\beta_kP=NP(\log^k n)$ form an infinite hierarchy?

This reference contains a survey of limited nondeterminism:

A SURVEY OF LIMITED NONDETERMINISM
IN COMPUTATIONAL COMPLEXITY THEORY
For attempts to separate the bounded nondeterminism hierarchy, I think monotone dualization of prime formulas is the most salient topic.

Consider the decision problem


  MONOTONE DUAL
  Input: two monotone CNF formulas, from which no literals can be removed
  Question: is the one formula the dual of the other?


MONOTONE DUAL can be decided with $O((\log\ n)^2/\log\ \log\ n)$ nondeterministic steps.  There is also a quasi-polynomial $n^{o(\log\ n)}$ time upper bound for this problem which has stood since 1996.  

So MONOTONE DUAL is in co-$\beta_2$P and also doesn't seem to require the full power of this class.  On the other hand, MONOTONE DUAL may be a good candidate for a problem that is outside P = co-$\beta_1$P.

This is surveyed in:


Thomas Eiter, Kazuhisa Makino, and Georg Gottlob, Computational aspects of monotone dualization: A brief survey, DAM 156 2035– 2049, 2008.  doi: 10.1016/j.dam.2007.04.017 (preprint)


I am not sure there is more work along these lines.  As with many other areas with the potential to separate P from NP, after some promising early progress new ideas now appear to be necessary.