## Boolean formulae satisfiable

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

### Boolean formulae satisfiable

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)
haroon

Posts: 2
Joined: Sun Nov 06, 2011 9:18 pm UTC

### Re: Boolean formulae satisfiable

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.
mfb

Posts: 824
Joined: Thu Jan 08, 2009 7:48 pm UTC

### Re: Boolean formulae satisfiable

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.

jaap

Posts: 1771
Joined: Fri Jul 06, 2007 7:06 am UTC

### Re: Boolean formulae satisfiable

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.
Ankit1010

Posts: 135
Joined: Fri Feb 11, 2011 11:32 am UTC

### Re: Boolean formulae satisfiable

These are NP Completeness satisfiability problems.
alice alice

Posts: 2
Joined: Thu Jan 12, 2012 10:19 pm UTC

### Re: Boolean formulae satisfiable

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.

Some tricks:
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.
korona

Posts: 243
Joined: Sun Jul 04, 2010 8:40 pm UTC

### Re: Boolean formulae satisfiable

korona wrote:
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.

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.
Ankit1010

Posts: 135
Joined: Fri Feb 11, 2011 11:32 am UTC

### Re: Boolean formulae satisfiable

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.
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision - BR

Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.

Yakk
Poster with most posts but no title.

Posts: 10213
Joined: Sat Jan 27, 2007 7:27 pm UTC
Location: E pur si muove

### Re: Boolean formulae satisfiable

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.
korona

Posts: 243
Joined: Sun Jul 04, 2010 8:40 pm UTC

### Re: Boolean formulae satisfiable

Ya, that was an bad brainfart on my part. Of course it is NP-hard, and hence not (known to be) in coNP.
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision - BR

Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.

Yakk
Poster with most posts but no title.

Posts: 10213
Joined: Sat Jan 27, 2007 7:27 pm UTC
Location: E pur si muove

### Re: Boolean formulae satisfiable

Given that you only have seven variables, you can just enumerate all 128 possible variable configurations.
EvanED wrote:be aware that when most people say "regular expression" they really mean "something that is almost, but not quite, entirely unlike a regular expression"

MHD

Posts: 631
Joined: Fri Mar 20, 2009 8:21 pm UTC
Location: Denmark

### Who is online

Users browsing this forum: No registered users and 2 guests