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 NONDETERMINISMIN COMPUTATIONAL COMPLEXITY THEORY
Separation of limited nondeterminism classes?
cc.complexity theory;nondeterminism
For attempts to separate the bounded nondeterminism hierarchy, I think monotone dualization of prime formulas is the most salient topic.Consider the decision problemMONOTONE DUALInput: two monotone CNF formulas, from which no literals can be removedQuestion: 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.