Can CNF with an input string be evaluated in logarithmic space? I have been trying to solve satisfiability of

{$&lt;c, w&gt;$ | $c$ is a CNF and $w$ is a binary string which satifies the $c$}. 

As first looks to me, it is satisiable in linear time ($O(n)$) since $w$ has lenght $n$. 

I tried thinking about whether the space complexity of this problem can be reduced to logarithmic order. But couldn’t end up with an acceptable reason so far. Well, my first thought is the following:

Considering that CNF $c$ is composed of conjuction of some clasuses, it’s possible to write every clauses’s result (0 or 1) to the working tape and after reading the entire string, evaluate those 0’s and 1’s (which correlates with the CNF’s clauses). But this won’t result in a logarithmic space complexity anyway and I think it would be of $O(n/k) = O(n)$ where $k$ is the number of clauses. 

Is there an optimize way of solving this in logarithmic space?
Yes, you can decide this language in logarithmic space, using the following algorithm:


for each clause in the CNF:


do a linear scan of $w$ to see if one of the literals in the clause is satisfied; if not, reject

if you got through all the clauses without rejecting, accept


What's the space complexity?  Well, there are at most $n$ clauses, so we need at most $\lg n$ bits to store the loop counter to keep track of which clause we're currently on.  We also need to store the current clause; there are at most $n$ variables in the formula, so we need at most $3 (1+\lg n)$ bits to store the clause.  Therefore, we need at most $O(\lg n)$ bits in total of space.

Of course, the running time is not optimal (it is $O(n^2)$ or so), but that doesn't matter, as we're only counting space complexity.