How to prove your solutions in Competitive Programming

Revision en5, by Everule, 2023-01-25 23:03:56

It seems many people struggle to understand what a proof even looks like, for greedy problems. The issue is the polarized forms of proof in CP and academic math, which may seem to be overly rigorous and difficult to during contest. However there is spectrum of what a proof even is. It is important to understand, that you cannot truly write and verify a proof within yourself, or within an entity (the entirety of codeforces for example). It is necessary to have judgement on what level of rigor is sufficient.

If you want to tell yourself that you just don't have math background and therefore can't prove and will perpetually use it as excuse this blog is not for you.

Academic proofs usually tend to be as rigorous as possible, and are carefully verified by other experts in the field, to be objectively certain of its correctness. Clearly that is not a level of rigor you need while solving a codeforces problem. You only need to prove it to yourself.

For this, there are certain heuristics you can use to solve these problems with proofs almost as fast as just solving as you do now, but with more certainty of correctness, which saves you time on implementing incorrect solutions or getting WAs and not knowing if your implementation or idea is bugged. Not only do these strategies help you prove your solutions, they also make it much faster to find approaches that could reasonably work, making you much faster at being able to solve, and you're not at the mercy of the tests while practicing.

On top of that, on problems with multistep solutions, finding the solution is exponential in number of steps, but by proving you can optimize it to linear. Most of my practice has been done without writing a single line of code, because I'm sufficiently experienced in knowing whether my solution is correct or not.

A lot of professional mathematicians believe there are 3 big segments of ability in any particular mathematical domain.

  • Level 1 : You either cannot make sensible claims, or cannot back your claims up to anyone else with anything more than heuristic arguments.
  • Level 2 : You're able to make claims and prove them, but you don't see the relation between your abstract writing and the intuition it works.
  • Level 3 : You don't need to even write down the proof anymore, and at this point you can tell if you can prove something or not.

IT IS NOT POSSIBLE TO REACH LEVEL 3 WITHOUT EXPERIENCE IN LEVEL 2

For example, you might see a proof like. You have a set $$$S$$$ of $$$n$$$ elements. Find the largest subset $$$T \subseteq S$$$ such that of size $$$k$$$, or $$$|T| = k$$$, and the sum of elements in $$$T$$$ is maximised, or $$$\sum_{t \in T} t$$$ is maximised.

It is quite obvious to simply pick the $$$k$$$ largest elements in $$$T$$$. You might think a formal proof would require you to do the following. Let $$$T$$$ be your solution, and let $$$T*$$$ be the optimal solution. If $$$T = T*$$$, our solution is optimal. Let $$$T \not= T*$$$. Then let us consider the symmetric difference of $$$T$$$ and $$$T*$$$. Notice that all elements in $$$T$$$ and not in $$$T*$$$ are larger than those in $$$T*$$$ and not in $$$T$$$. Therefore $$$sum(T) \ge sum(T*)$$$, and is optimal.

But this is not really a proof you need in Competitive programming. This is necessary for math, because everything relies on the basic axioms, and all arguments should derive from it. However, in most cases you don't need to prove a self-evident claim like this. It's useful, but not necessary to understand the formal reasoning of a proof of something really simple, so you can apply it to cases where you don't have as strong intuition as picking the $$$k$$$ largest. I can go on a tangent about how intuition is derived from the primal instincts of man, and is optimized for real life scenarios. For an interesting read on that, you can try this.

But effectively, what I'm trying to say that this claim is not obvious to you because its easy to prove. Its because the claim has applied for humans long enough that its "common sense" to our brain. Really the easiest way to improve in Competitive Programming is the art of developing intuition of something you can't quite intuit anything about. It's also why I enjoy easier problems that I struggle in. It usually means I had to develop intuition in something I didn't really have good intuition for. I personally believe that is something that helps in all areas of thinking, but you might disagree.

I hope that we're in agreement on what a proof should do.

An easy way to sanity check your proof is. Think of every step you took while proving. If you wanted to justify to an opponent you were correct, what would the opponent try to argue against. If you think you can't justify your reasoning over his to a jury without reasonable doubt, your proof needs to be more specific.

I will now show how to write effective proofs, and why they're still formal, despite not having the illusory abstract variables describing everything.

I've decided to make this part interactive. You can send me any problem that you might have guessed, or any constructive you did not understand how to derive, and I will reply to it (if I can solve it). If I think its sufficiently educational, I will add it to the blog.

Let's try this atcoder problem. You've binary string made with $$$AB$$$. You can change some pair of adjacent characters to "AB". Find if you can make the given string a palindrome.

Solution

This form of reasoning is applicable to solving problems, and not just proving your solutions.

Let's start with this unnecessarily hated problem for example click.

Create $$$n$$$ by $$$n$$$ matrix $$$M$$$, where every number from $$$1$$$ to $$$n^2$$$ appears once, such that the number of different values of $$$|x - y|$$$ for adjacent elements in $$$M$$$ is maximized.

Solution

History

 
 
 
 
Revisions
 
 
  Rev. Lang. By When Δ Comment
en5 English Everule 2023-01-25 23:03:56 3 Tiny change: ' you need Competiti' -> ' you need in Competiti'
en4 English Everule 2023-01-25 22:12:57 7 Tiny change: ' $T*$ and $T$. Ther' -> ' $T*$ and not in $T$. Ther'
en3 English Everule 2023-01-25 22:11:25 323
en2 English Everule 2023-01-25 21:58:10 9 Tiny change: 'heuristic claims.\n\n\n\n' -> 'heuristic arguments.\n\n\n\n'
en1 English Everule 2023-01-25 21:57:17 7623 Initial revision (published)