Boolean formulae satisfiable

[haroon]

Are the following Boolean formulae satisfiable? Why or why not?
a) Ф = (x1) ^ (not x3 v x7) ^ (x2 v x3 v x4) ^ (not x2 v x3 v notx5 v x6)
b) Ф = (x2 v x3 v x5) ^(x1 v x4 v x6) ^(notx2 v x3 v x6) ^(notx3 v x4 v x7)
c) Ф = (x1) ^ (notx3) ^ (notx5) ^ (x2 v x5) ^ (notx1 v x2 v x3 v notx4 v x5)

[mfb]

Just try and check yourself? They are easy enough to do this by hand (even without pen+paper), and computers can do it in milliseconds.

[jaap]

Just use De Morgan's laws to expand it until you get something of the form
a OR b OR c OR ...
where the a,b,c... are terms without ORs in them, only ANDs and NOTs. For example (x1 AND NOT x3).
It is then very easy to see if it is satisfiable.

This is more work than necessary for these relatively simple cases, but it is a good exercise.

[Ankit1010]

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.

[alice alice]

These are NP Completeness satisfiability problems.

[korona]

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.

Some trickses:
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.

[Ankit1010]

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.

By variable, I mean that "a" and "~a" both count as one variable (i.e a, or any unary operator combined with a is one variable). In that case, it's clear that the formula you mentioned is unsatisfiable.

[Yakk]

So, you mean, "All of them are satisfiable, because for each of them I found an assignment (which I won't mention) whereby they evaluate to true"?

I suspect the disagreement comes from reading your post as "All of them, because problems of that form are always satisfiable via this described method", which korona (quite rightly) objected to. Korona's assumption is somewhat reasonable, because your post is a pretty obtuse way of saying "these can be satisfied because I found an answer".

As noted, these are an example of problems in NP, so showing that they are satisfiable is easy once you have the answer -- just give the answer, and say "duh". The interesting part about problems in NP is finding that answer -- the verification step after you find it is easy.

Sat (aka, logical formula satisfiability) isn't in coNP (as far as I can remember), which makes proving that a given formula cannot be satisfied trickier than showing it can be satisfied.

[korona]

SAT is in NP so UNSAT (aka prove the formula is unsatisfiable) is in coNP and actually it is coNP hard.
If you have a unsatisfiable formula in CNF you can give a resolution proof (the wiki page about that topic is not very good) to show that the formula is unsatisfiable. But there are classes of formulas for which the resolution proof is exponentially larger than the formula. An example are encodings of the pigeon hole problem as CNF formulas.
There are stronger proof systems for which no classes of formulas with exponentially large proofs have been found yet, e.g. extended resolution or various Hilbert systems. If there are no such classes then NP = coNP which would be a very surprising result.

[Yakk]

Ya, that was an bad brainfart on my part. Of course it is NP-hard, and hence not (known to be) in coNP.

[MHD]

Given that you only have seven variables, you can just enumerate all 128 possible variable configurations.