Questions tagged [correctness-proof]
Questions that ask for or about correctness proofs of algorithms.
385 questions
2
votes
1
answer
76
views
Proving NPhardness of linkedin queens
Consider the linkedin queens problem - our queens move like a rook + king on a nxn chessboard with coloured regions. The goal of the game is to place exactly queen in every row, column and coloured ...
- 21
2
votes
1
answer
75
views
You Will All Conform Programming Puzzle: The difference between the number of Fs and the number of Bs are at most 1?
Source of the puzzle: https://ocw.mit.edu/courses/6-s095-programming-for-the-puzzled-january-iap-2018/resources/mit6_s095iap18_puzzle_1/.
The puzzle is
input: a vector of F's and B's, in terms of ...
2
votes
1
answer
73
views
What is the loop invariant for stack-based algorithm for finding largest rectangle enclosed in a histogram?
I would like some help with proving the correctness of the following algorithm that solves LeetCode problem 84 of finding the largest rectangle enclosed by the bars of a histogram. For simplicity, we ...
- 45
0
votes
0
answers
74
views
Proof of correctness for a greedy algorithm finding the lexicographically smallest array
The following problem is from Codeforces.
We are given an array $a$, containing $n$ integers. In a single operation, we can take some index $i$, with $1\le i\le n$, increase $a_i$ by one, and move it ...
- 175
5
votes
3
answers
1k
views
Is partial correctness decidable?
Is partial correctness decidable? i.e., is there a general algorithm that for any pair of formal specification and encoded TM, returns true if and only if, when the TM halts, it meets the ...
1
vote
1
answer
87
views
FLP Impossibility Result: Uniqueness of schedule application
In the proof of Lemma 2 in the FLP impossibility paper, the authors use the fact that if a single process fails after inputting distinct messages into the message buffer and then failing, any schedule ...
- 203
2
votes
0
answers
71
views
Proving that for every semi-Thue system $\Gamma$, there exists a two-letter semi-Thue system $\Gamma'$ such that $S_\Gamma = S_{\Gamma'}$
I'm reading Martin Davis' Computabilty and Unsolvability. In Chapter 6, Section 1, Davis writes the following:
THEOREM 1.8. For every semi-Thue system $\Gamma$, we can construct a semi-Thue system $\...
- 21
-1
votes
1
answer
79
views
Loop invariant proof, nth fibonacci number
The code below calculates the nth Fibonacci number. Do you know the mathematical formula used in this algorithm? I couldn't prove the loop invariant here.
...
- 11
0
votes
1
answer
113
views
How to show $\mathsf{NP^{BQP} = QMA}$?
I was reading the document below, authored by @Lieuwe Vinkhuijzen.
In equation 2.1 (page 14 of this), the following equation is mentioned.
$$\mathsf{\Sigma_1^{BQP} =NP^{BQP}= QMA}$$
$\mathsf{NP}$, $\...
- 189
1
vote
0
answers
45
views
Is it possible to start a Dijkstra search from a source node s, bounded at r, with a non-empty distance map and priority queue?
TL:DR: I want to know whether correctness is affected if I start Dijkstra with a distances map that already contains shortest paths shorter than $r$ and a priority queue initialised with those ...
- 11
3
votes
3
answers
498
views
Proof of correctness for optimal solution for sorted two-sum
I have been solving the problem of two sum with a sorted array, which can described as follows:
Given a sorted array arr sorted in non-decreasing order and a ...
- 133
0
votes
1
answer
61
views
Formalizing Transformation Rules between Similar Loop Constructs
I'm trying to understand and formalize the relationship between two similar but slightly different loop structures in different programming languages:
Example 1 (PHP):
...
1
vote
1
answer
56
views
Why is it not possible to recognize a self-complementary graph just by searching for a self-complementary graph on $8$ vertices?
From the paper by Gibbs (1974) it is known that every self-complementary graph on $4n$ vertices has $n$ disjoint induced $P_4$ subgraphs. Let's call the collection of these subgraphs a $P_4$ cover.
...
- 2,131
2
votes
1
answer
119
views
Proof for Gas Refills on Circular Route Problem
The circular route gas station problem asks: If given a car with an unlimited gas tank, find the gas station on a circular road that if started from would allow you to travel station to station ...
- 23
0
votes
1
answer
90
views
Finding middle vertex of tree
"Given a graph G, the remoteness of a vertex v is the distance from v to the vertex u that is farthest from v in G. That is, the shortest path from v to u is as long as possible. A vertex of G ...
