Woburn Challenge 2001 - Suicidal

Thursday - The Mole

So that was enough craziness. Three whole days of no studying was just too much and so orientation week was cut back to only 3 days (or was it?). Today is the first day of class – discrete math. The students are divided into groups of about 10 and are each given a 2-CNF formula (ie. a formula in conjunctive normal form with 2 variables per clause – e.g., (a OR b) AND (c OR a) AND (x OR NOT y) ) for which they have to find a solution. Being engineers not in the math stream, they set out to solve the formula using the only method they know: brute force (ie. trying all possible combinations for all the variables). There are however 2 twists on this sinister day.

1. Word has leaked out that this so-called “class” is really another test of their orientation week and that there is a mole within their group who is sabotaging their efforts to find a solution to the formula.
2. They have discovered that not all CNF formulas are satisfiable.

Therefore the following question arises: are they unable to find a solution because a) they are stupid, b) the mole is sabotaging their efforts or c) the formula is unsatisfiable.

Furthermore, being Waterloo keeners, they want to solve this problem in time O(n lg(n) ) or less, where n is the number of clauses in the formula and lg is the base 2 logarithm.

Input

Several 2-CNF formulas: variables will be characters, & is AND, | is OR and ! is NOT; blank line denotes end of input. There will be spaces between | and & and brackets around each clause. There will be at most 10,000 variables per formula.

Output

If a formula is satisfiable, print out ‘satisfiable’.
Otherwise, output 'unsatisfiable'.

Sample Input

(a | b) & (a | c)
(a | a) & (!a | !a)

Sample Output

satisfiable
unsatisfiable

All Submissions
Best Solutions

Point Value: 20 (partial)
Time Limit: 2.00s
Memory Limit: 16M
Added: Dec 05, 2008

Languages Allowed:
C++03, PAS, C, HASK, ASM, RUBY, PYTH2, JAVA, PHP, SCM, CAML, PERL, C#, C++11, PYTH3

Comments (Search)

Each variable can be any sequence of alphanumeric characters.

This is pretty strange, and I don't know why no one pointed it out before, but the second line of the Sample Output should read 'unsatisfiable'.

What does it mean if it satisfiable? Is the question basically "Is there a set of numbers that you can substitute into each variable to make this equation evaluate to true?"?

Yup

can we not just output satisfiable or unsatisfiable for partial points?

Which is why Hanson and the other admins can see your code =P

wow, how naive can you get.  and guess what, after they see your code seyon, they will ban you.

This judge is for learning, what do you learn by doing that?

does it rest well on your conscience that you cheated and earned partial points while others toiled for endless nights with the problem trying to earn points nobly and learn something at the same time?

Lol... "nobly"

hey, Comp Sci is a noble subject, don't you think?  It's the subject of the kings.