Probabilistic method is a common technique to show the existence of interesting combinatorial objects by counting. Often, even in cases when we can compute that a majority of objects of certain type have a desirable property, it is still hard to explicitly construct one such object. This is the purpose of this paper, presented at FOCS'21. It uses methods of complexity, logic, randomness, etc. So, it will hopefully be interesting for everybody.