Ankit1010 wrote:All of them are, by the same logic: I can pick atleast 1 variable in each bracketed term without picking it in any other bracket. The bracketed terms all contain only ORs, so this is enough to let me force each of them to be true.
That is not true. Let -a be the inverse of a variable a and consider the formula (a OR b) AND (-a OR b) AND (a OR -b) AND (-a OR -b). It can easily be seen that this formula is unsatisfiable.
In this case however you can easily guess some variables that you have to set to true in order to satisfy the formula.
Terms of the form (a_1 OR ... OR a_k) with a_i either a variable or its inverse are usually called clauses
and a formula (C_1 AND ... AND C_m) with clauses C_i is said to be in "conjunctive normal form"
(CNF). One can easily show that for all boolean formulas over the unary/binary operations NOT, AND, OR, IMPLIES, XOR, IFF, etc. there exists a equisatisfiable formula in CNF of length O(n) where n is the length of the original formula; it follows that determining whether such a formula is satisfiable is actually coNP-hard.
Try to find variables that only occur in one polarity and set them to true (such a variable is called a "pure literal"). (Why can you do that without loss of generality?)
Then set all variables x to true if there is a clause consisting only of x (such a clause is called a "unit clause"). (Again: Why are we allowed to do that?)
Binary clauses (i.e. clause consisting of 2 variables) can be seen as implications of the form (a -> b) and may force additional variables to be set.
Then guess an assignment for the remaining variables.