A very nice proof of existence
We prove that this formula is satisfiable.
First, we consider the following random experiment: We assign each occuring variable (in the whole formula) a value 1 or 0 generating a random assignment of values to variables. Then, the probability that one specific clause is satisfied, is . This is due to the fact that one single clause evaluates to false only for one single assignment of variables (the variables occuring in the clause).
So, we now introduce the following: For each clause , we introduce an indicator variable indicating whether the corresponding clause is satisfied or not (i.e. iff is satisfied by our randomly generated assignment). The above considerations yield , where denotes the expected value of and is the probability of event .
Moreover, we now define as the sum over all indication variables. This means, stands for the number of satisfied clauses. We compute the expected value (since the expected value is linear). This means, we can conclude .
This can be simplified to . This means, in average, we have clauses satisfied. Due to the principle of average, this means, that there must exist some assignment of variables such that the number of satisfied clauses .
But since must be a natural number, this can be restated so that we now know that there must exist an assignemt of variables such that , which is the next natural number. But since is exactly the number of clauses, we now know that all clauses are satisfied, and, thus, the whole formula is satisfied.
Thus, the formula is satisfiable.
I personally find this proof so nice because usually existence proofs involve some routine to construct an explicit solution which is then used as a proof of existence. However, this existence proof purely relies on the averaging principle, and proves the existence of a satisfying assignment without explicitly constructing it. Moreover, the proof uses the probabilistic method, which I consider a very elegant technique.