UVa 11357 Ensuring truth solution description

We’re in the midst of preparing for the ICPC Southern Africa Regionals, to be held in October, and so I step up reading problems to find nice ones to train the interested students in a range of topics. The “Ensuring truth” problem was one of those, which I’ll discuss in the remainder of the post, since there’s no discussion of it online yet (only some code), and it is not as daunting as it may look like at first glance:


The task is to determine whether such a formula is satisfiable.

While it may ‘scare’ a 1st or 2nd-year student, when you actually break it down and play with an example or two, it turns out to be pretty easy. The ‘scary’ looking aspects are the basic propositional logic truth tables and the BNF grammar for (simplified!) Boolean formulas. Satisfiability of normal Boolean formulas is NP-compete, which you may have memorised, so that looks daunting as well, as if the contestant would have to come up with a nifty optimization to stay within the time limit. As it appears, not so.

Instead of being put off by it, let’s look at what is going on. The first line of the BNF grammar says that a formula can be a clause, or a formula followed by a clause that is separated by a disjunction (| ‘or’). The second line says that a clause is a conjunction of literals, which (in the third line) transpires to be just a series of ‘and’ (&) conjunctions between literals. The fourth lines states that a literal can be a variable or its negation, and the fifth line states that a variable is one of the letters in the alphabet.

Now try to generate a few inputs that adhere to this grammar. Swapping one variable at a time on the left of the “::=” sign for one of the elements on the right-hand side of the “::=” sign in the BNF grammar, with steps indicated with “=>”, then e.g.:

<formula> => <formula> | <clause> => <clause> | <clause> => (<conjunction-of-literals>) | <clause> => (<literal>) | <clause> => (<variable>) | <clause> => (a)| <clause> => (a)| (<conjunction-of-literals>) => (a)|(<conjunction-of-literals> & <literal>) => (a)|(<conjunction-of-literals> & <literal> & <literal>) => (a)|(<conjunction-of-literals> & <literal> & <literal> & <literal>) => (a)|(<literal> & <literal> & <literal> & <literal>) => (a)|(~<variable> & <literal> & <literal> & <literal>) => (a)|(~a & <literal> & <literal> & <literal>) => (a)|(~a & <variable> & <literal> & <literal>) => (a)|(~a&b& <literal> & <literal>) => (a)|(~a&b& <variable> & <literal>) => (a)|(~a&b&a& <literal>) => (a)|(~a&b&a& <variable>) => (a)|(~a&b&a&c)

That is, (a)|(~a&b&a&c) is in the language of the grammar, as are the two in the input given, being (a&b&c)|(a&b)|(a) and (x&~x). Do you see a pattern emerging of how the formulas look like with this grammar?

It’s a series of disjunctions of conjuncts, and only one of the conjuncts shouldn’t have a contradiction for the formula to be satisfiable. The only way we get a contradiction is if both a literal and its negation are in the same conjunct (analyse the truth tables if you didn’t know that). So, the only thing you have to do with the input is to check whether within the brackets there is, say, an x and a ~x, and with the first conjunct you encounter where there is no contradiction, then the formula is satisfiable and you print YES, else NO. That’s all. So, when given “(a)|(~a&b&a&c)”, you know upon processing the first conjunct “(a)”, that the answer is YES, because “(a)” is trivially not contradictory and thus we can ignore the “(~a&b&a&c)” that does have a contradiction (it doesn’t matter anymore, because we have found one already that doesn’t).

I’ll leave the implementation as an exercise to the reader  :).


ACM ICPC 2014 solution to problem A – baggage

Some of you already know I was on-site coach for the UCT team at the ACM Inter Collegiate Programming Contest World Finals in Ekaterinburg, held from 22 to 26 June, 2014. The problems were unusually hard this year, and solving 4 out of the 10 problems already got teams into the bronze medal range [results]. The technical coach of the UCT team, Bruce Merry, has written an analysis of 6 problems on his blog (D, K, C, E, B, and F–update: now also I and G, J, L, and H), and over at TopCoder, SnapDragon discusses 4 of the 10 problems (A, E, F, G), except that SnapDragon does not provide a solution to A (and I don’t like his hint of brute-force code-and-try) [update 3-7: there’s description of his solution here now]. Googling, I couldn’t find someone else discussing the solution to problem A, so here’s mine, which I solved on the plane from Moscow to Frankfurt (among other activities, and one among the four flights we had to take to arrive back in Cape Town).

The problem

Stripping the “baggage problem” to its essentials: you have a sequence of alternating Bs and As, which has to be reordered to first all the As then all the Bs, and the reordering has to occur moving two letters at the same time, and remain adjacent. For instance, with an n = 4, we have 2n characters, BABABABA, and in the end after sorting, it then will be AAAABBBB, and this has to occur in the minimum amount of moves. N is randomly chosen, and is an integer between 3 and 100. The cells on your tape are numbered from 0 to -2n+1, so with our n = 4, from -7 to 8, and the first B is on position 1.

Update (3-7): This problem appears to be “Tait’s counter puzzle”, which Peter Guthrie Tait, a Scottish mathematical physicist, described in 1884 [see description] (thanks to Davi Duarte who mentioned it in the topcoder thread).


Informally, there are two parts to the algorithm: move around the As and Bs to pair them as AA and BB, which cost you n/2 moves if n is even and n/2-rounded up moves if n is odd, and then sort those pairs in the remainder to a total of n moves. The first part occurs alternating moving AB from the right to the left, starting at the last AB (position 2n-2) and then every other 4 to its left, and BA from left to right, starting from position 3 and every other 4 positions to the right (i.e., 7, 11, etc.), and then the BBs are ferried to the right from left to right, and the AAs from the right to the left, also alternating. N=3 is an exception.

One can do this with a neat mathematical proof, but I found out with pattern creation and recognition, visualizing the provided sample input and moves for n = 5 and n = 8, which can be done in 5 resp. 8 steps (given in the problem statement as sample output). Here’s a description of that approach.

First, devising one for 3 is trivial, using the following moves (the only option), using the position indicated with the position of the first letter, and highlighting the ones that will be moved next:

Start: . . . . . . BABABA
Move 2 to -1, which gives . . . . ABB . . ABA
Move 5 to 2, which gives . . . . ABBBAA . .
Move 3 to -3, which gives . . AAABBB . . . .

This already suggests that the minimum amount of moves will always be n, because it is n moves also for n = 5 and n = 8. Next, devising one for n = 4, and knowing the moves for n = 3 and n = 5, I tried to work it out for BABABABA, i.e., the first AB, like with n = 3, BABABABA, and BABABABA like with the n = 5 case. The last one is the only one that worked in 4 moves, starting with moving 6 to -1, again. Again, because for all ns so far, the first move is to -1.

Let’s put this to the test with n = 7, with the ones to be moved in bold and the empty cells indicated with dots:


i.e., move the last AB (thus, position 12) as this worked for n=4 and n=5, then


i.e., move the first BA after position 1 (thus, position 3)


i.e., move the last AB before a pair (thus, position 8)


i.e., move the first BA after position 1 (thus, position 5). Then sorting the BBs and AAs:


This was enough for me to have discovered the pattern of alternating for the matching and alternating for the sorting.

What is ‘nasty’ in the problem description, retrospectively and for the pattern-based approach vs. a neat maths-y proof at least, is that the pattern deviates for n = 3, and the provided sample output for n = 8, although in 8 steps, is an alternative solution, not one that one obtains with the algorithm. With the approach as mentioned above, we have for n = 8 the following (I did that one to double-check):


This confirmed it works. It may look a bit craft-y, but the patterns show beautifully with larger n, which are shown below for the even and odd case (made just for the blog post, not in solving it); squint your eyes if it’s not immediately clear.

N = 16


N = 17


Neat. Writing the code is left as an exercise to the reader.

I’m looking forward to the other problems (except the crane balancing problem C, whose description I did not like, at all), the upcoming regionals and next year’s ICPC World Finals in Morocco (if not winning, then to have at least a great time like we had this time)!