A CNF formula is k-satisfiable if each k clauses of it can be satisfied
simultaneously. Let \pi_k be the largest real number such that for each
k-satisfiable formula with variables x_i, there are probabilities p_i
with the following property: If each variable x_i is chosen randomly and
independently to be true with the probability p_i, then each clause is
satisfied with the probability at least \pi_k.

We determine the numbers \pi_k and design a linear-time algorithm which
given a formula either outputs that it is not k-satisfiable or finds
probabilities p_i such that each clause is satisfied with
the probability at least \pi_k. Our approach yields a robust linear-time
deterministic algorithm which finds for a k-satisfiable formula a truth
assignment satisfying at least the fraction of \pi_k of the clauses.

A related parameter is r_k which is the largest ratio such that for each
k-satisfiable CNF formula with m clauses, there is a truth assignment
which satisfies at least r_k*m of its clauses. It was known that
\pi_k=r_k for k=1,2,3. We compute the ratio r_4 and show \pi_4<>r_4.
We also design a linear-time algorithm which finds a truth assignment
satisfying at least the fraction r_4 of the clauses for 4-satisfiable
formulas.