# Question
Title: Proof of correctness of some optimization of Heap's algorithm for producing permutations
Good day. Some time ago I found a page on (en.) wikipedia about Heap's algorithm for permutations. Here it is.

Original algorithm can be written as next (copy from (en.) wikipedia):

```
procedure generate(k : integer, A : array of any):
    if k = 1 then
        output(A)
    else
        for i := 0; i < k; i += 1 do
            generate(k - 1, A)
            if k is even then
                swap(A[i], A[k-1])
            else
                swap(A[0], A[k-1])
            end if

        end for
    end if

```

So we have two different ways of how algorithm works with odd and even value of k.

When we use "even way" - the set, which we permute, is been shifted to the right with a cycle. So \[1, 2, 3, 4\] -\> will become \[4, 1, 2, 3\]

When we use "odd way" (for some k = a \> 1) - we reduce previous cyclic shifts to the right, that were caused by recursive calls of original algorithm in a "for" cycle. So \[1, 2, 3, 4, 5\] -\> will stay \[1, 2, 3, 4, 5\]

That how original algorithm works, "even way" creates shifts, "odd way" reduce it, so upper "even way" may change set, in way that upper "odd way" may also reduce it.

---

Now about optimization (also from (en.) wikipedia):

```
procedure generate(k : integer, A : array of any):
    if k = 1 then
        output(A)
    else

        // Recursively call once for each k
        for i := 0; i < k; i += 1 do
            generate(k - 1, A)
            // avoid swap when i==k-1
            if (i < k - 1)
                // swap choice dependent on parity of k
                if k is even then
                    swap(A[i], A[k-1])
                else
                    swap(A[0], A[k-1])
                end if
            end if
        end for
    end if

```

The optimization consists in removing "extra" permutations. When algorithm uses "even way" the optimization doesn't change logic and result. But in "odd way" algorithm reduce last swap so we have next situation

Instead of \[1, 2, 3\] -\> \[1, 2, 3\] We will have \[1, 2, 3\] -\> \[3, 2, 1\]

And it will also effect on upper levels and so on.

My problem is that I don't understand how can algorithm continue produce correct amount of unique permutations? How can upper calls (it is about recursion) of algorithm correctly choose new unique number?

About last question, when we use algorithm, we use interesting logic that can be found in this publication Here

---

Please accept my apologies for possible grammatical errors in the text, I am still not very good at communicating in English. If you need any more detailed information, I will be happy to add it to my question.

---

Here the example from (en.)wikipedia 1,2,3,4,5 ... Original Array

4,1,2,3,5 ... 1st iteration (Permute subset/Rotate subset)

5,1,2,3,4 ... 1st iteration (Swap)

3,5,1,2,4 ... 2nd iteration (Permute subset/Rotate subset)

4,5,1,2,3 ... 2nd iteration (Swap)

2,4,5,1,3 ... 3rd iteration (Permute subset/Rotate subset)

3,4,5,1,2 ... 3rd iteration (Swap)

1,3,4,5,2 ... 4th iteration (Permute subset/Rotate subset)

2,3,4,5,1 ... 4th iteration (Swap)

5,2,3,4,1 ... 5th iteration (Permute subset/Rotate subset)

1,2,3,4,5 ... 5th iteration (Swap) The final state of the array is in the same order as the original

And according to optimization we don't make swap of last 5th iteration, so set doesn't return original state

# Answer
Your this claim: "*When algorithm uses "even way" the optimization doesn't change logic and result*" is incorrect.

Since the "even way" is dependent on the "odd way" (due to recursive dependency), the optimization does change the result.

For example, consider the following example when optimized algorithm is used for even sized array:

$\[1 \\, 2 \\, 3 \\, 4\]$: Original Array

$\[3 \\, 2 \\, 1 \\, 4\]$: First iteration (Permute subset/Rotate subset)

$\[4 \\, 2 \\, 1 \\, 3\]$: First iteration (Swap)

$\[1 \\, 2 \\, 4 \\, 3\]$: Second iteration (Permute subset/Rotate subset)

$\[1 \\, 3 \\, 4 \\, 2\]$: Second iteration (Swap)

$\[4 \\, 3 \\, 1 \\, 2\]$: Third iteration (Permute subset/Rotate subset)

$\[4 \\, 3 \\, 2 \\, 1\]$: Third iteration (Swap)

$\[2 \\, 3 \\, 4 \\, 1\]$: Fourth iteration (Permute subset/Rotate subset)

Note that you did not obtain $\[1 \\, 2 \\, 3 \\, 4\]$ (unaltered array) but you obtained an altered array, i.e., $\[2 \\, 3 \\, 4 \\, 1\]$.
> 0 votes

---
Tags: algorithms, correctness-proof, permutations
---


# Question
Title: Is the set of all duals same as the set of all planar graphs?
Let $P$ be the space of all possible planar graphs.

Fact: A planar graph may have multiple duals based on its embedding.

Let $D\_p$ be the set of all possible duals of a planar graph $p\in P$

Let $S$ be the space given by union of $D\_p$ for all $p \in P$

Is $S = P ?$

# Answer
If the dual of the dual of a planar graph is isomorphic to the original graph, then yes, it must be. Let $G$ be a planar graph and $G^\*$ its dual. Then, since $G^\*$ is a planar graph, then $G^{\**}$ is its dual. Therefore, any graph $G$ that is planar or the dual of a planar belongs in both $S$ and $P$:

If $G \in P$, then $G^\* \in S$. But clearly $S \subseteq P$, so $G^\* \in P$. Then also $G^{\**} \in S$, but since $G \simeq G^{\**}$, $G \in S$ as well, hence $P \subseteq S$.
> 0 votes

---
Tags: graphs, planar-graphs
---


# Question
Title: Ways to speed up a Recursive Backtracking Algorithm
When dealing with a Recursive Backtracking Algorithm what are the ways to speed it up and what computational hardware is involved?

I'm assuming from ignorance that everything is done by the CPU so the only thing that comes to mind to make it faster would be early exits, multithreading or quantum computing.

Is that it? Can a GPU be used or do these only work for mathematical operations?

TLDR: How can you speed up Recursive Backtracking Algorithm via Hardware or via Software.

# Edit:

Assume something simple, like having a goal amount and multiple coins, then having to find which combination of coins add up to that goal amount.

# Answer
I think you pretty much got it there. There really aren't many ways to improve it, our best method is a slow one! (though our human brains instinctively would love to find something better for such a simple problem)

Though I'm imagining, when I think of recursive back-tracking, I think of an algorithm to solve a rubiks cube, or a sudoku puzzle. Which is just brute-forcing the problem, and it'll be slow no matter what. There are millions or billions or pathways to check, to see if we get a solution, and even then we might not get the best one.

However, if you're willing to step away from recursive back-tracking, there are some algorithms that will "smartly" try to find you a good answer really efficiently. Imagine when a human tries to solve a rubiks cube, they don't try every combination possible.

Computerphile has a good video on it: https://www.youtube.com/watch?v=ySN5Wnu88nE

The general idea of it, is you model all of your possible options/choices/moves as a massive decision tree, or graph. You're attempting to find the shortest path from the start, to the solution, but because we don't know how far away from the solution we are, we have a heuristic function, which gives us a guess of how far away we are.

This is the A\* algorithm, almost like a Dijkstra, but it involves our heuristic function.

We selectively explore the paths which we guess will find us the solution the quickest. I applied this to a bubble sorting game once, my brute-force would explore 100000 different pathways and give you the BEST solution which takes only 9 steps to solve the game. But my A\* algorithm with a good heuristic would explore 100 pathways, and give you a really good solution (but not the best), which took 10 steps. 1000x faster, but not guaranteed to be the best solution.
> 1 votes

---
Tags: algorithm-analysis, backtracking
---


# Question
Title: Do all the numbers belong to same slot in the Hashtable?
I was reading the CLRS. In the Hashing Chapter on page 262 a statement says: "For example, if we know that the keys are random real numbers $k$ independently and uniformly distributed in the range $0 \leq k \< 1$, then the hash function $h(k)= \lfloor km \rfloor$."

Question: Does Uniformly distributed meant all numbers have equal probability. if so then all numbers have the same $k$ values and belong to the same slot.

# Answer
> 1 votes
Keys are uniformly distributed means that they are drawn from a space with equal probability.

So if we set the hash function to be $h(k)=\lfloor{km}\rfloor$, then each given element is equally likely to hash into any of the $m$ slots. (Refer to the definition of simple uniform hashing in page 259 CLRS)

Yes, it is true that each element with key $k$ will be hashed to the same slot. But the point is the elements are chosen uniformly independently, so they have the same probability to hash to any of the $m$ slots.

# Answer
> 1 votes
Your conclusion "then all numbers have the same $k$ values" is not justified. The samples are anywhere in $\[0,1)$ and can fall in any slot.

Uniformly means that in the long run, all slots will be filled in a balanced way. (The $\text{pdf}$ of $k$ is continuous and constant. The expectation of the filling of any bin is $\dfrac nb$ for $n$ drawings and $b$ bins. In other words, the probability to fall in a given bin is $\dfrac1b$.)

---
Tags: algorithms, discrete-mathematics, mathematical-programming
---


title: is Reduction from RE to coRE possible?

text:
# Question
Title: is Reduction from RE to coRE possible?
I'm trying to figure out if it something that I can say for every 2 languages:

is Reduction from RE\R to coRE\R always not possible, and why?

(some thoughts about it: this reduction might be possible when for given language L it's both in RE and both in coRE (meaning it's in R, but when it's RE\R and coRE\R, it is not possible)

another thought, can I use reduction from RE\R to prove that some language that in coRE is not in R?

# Answer
> 1 votes
This depends greatly on what "reducible" means.

* If we mean *Turing reducible*, then every set (trivially) Turing-reduces to its complement, so in particular each r.e. set reduces to a co-r.e. set.
* If we mean *many-one reducible*, on the other hand, then **no** properly r.e. (= r.e. and not recursive) set reduces to any co-r.e. set. For suppose $A$ is properly r.e. and $B$ is co-r.e. If $f:\mathbb{N}\rightarrow \mathbb{N}$ were an $m$-reduction of $A$ to $B$, then we could recursively enumerate the complement of $A$ (put $x$ into $\mathbb{N}\setminus A$ iff we see $f(x)$ leave $B$). This would make $A$ recursive.

In my experience, "reducible" in computer science almost always means "\[resource-bounded\] many-one reducible."

---
Tags: computability
---


# Question
Title: What does it mean if we disable K-rule in Agda?
TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ \mathit{refl} $"?

In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced as an implicit rule and it's defaultly enabled. If I understand it correctly, it means parameter of type $ \forall a.a \equiv a $ can be matched with $ \mathit{refl} $. If we disable K-rule, what will happen? What kind of codes is it going to prevent me writing? Because we can always construct $ \forall a . a \equiv a $, even without K, we can always get an instance of $ T $ by passing $ \mathit{refl} $ to any functions with type $ \forall a.a \equiv a \rightarrow T $.

Agda's doc has given me an example which indeed shows a circumstance that can only work with K:

```
K : {A : Set} {x : A} (P : x ≡ x → Set) →
    P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p

```

In this code, if we can pattern match `x≡x` with `refl`, `P refl` can be trivially equivalent to `P x≡x` (but without K, we can't).

So does that mean: "K enables people to match $ \forall a.a \equiv a $ with $ \mathit{refl} $"? I didn't find the answer on the Agda doc.

If we disable K, will the semantic of Agda's equality type (CH-ISO) change?

# Answer
Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching.

Axiom K is inconsistent with homotopy type theory, where the univalence axiom provides ways of constructing equalities other than `refl`. For example, if there are two functions that are pointwise equal, univalence asserts that there is an equality term equating them, but it cannot be `refl` if the functions have different implementations.

All removing K from Agda does is add restrictions to pattern matching, making fewer matches typecheck. The runtime semantics are unchanged, and no new programs typecheck.

For some excellent introductions on the subject, I recommend:

Pattern Matching without K

Unifiers as Equivalences

Both of these have more detailed versions in JFP if you have access to a subscription.
> 3 votes

# Answer
I'm studying this myself and I think the only essential distinction between K and J is that:

* The user of K is expected to provide a type `P : x ≡ x → Set` depending on some loop about `x` (a closed path).
* The user of J is expected to provide a type `Q : (y : A) → x ≡ y → Set` depending on a general path that could be either open or closed. Since `Q` isn't allowed to assume that it is closed, J is more restrictive on the user. You can define `P = Q x` but the reverse is not in general possible.

From a homotopic point of view, K is not possible because the structure of `P` is too rigid; the lack of an adjustable endpoint `y : A` prevents `P` from being continuously transported along arbitrary paths.

This is evidenced by the code below:

```
K : {A : Set} {x : A} (P : x ≡ x → Set)
  → P refl → (p : x ≡ x) → P p
K P d p = {- impossible in HoTT/CuTT -}

J' : {A : Set} {x : A} (Q : (y : A) → x ≡ y → Set)
   → Q x refl → (p : x ≡ x) → Q x p
J' Q d p = Cubical.Foundations.Prelude.J Q d p

```
> 1 votes

---
Tags: proof-assistants, agda
---


# Question
Title: Harder variation of light bulb problem (solvable in O(n log n)?)
Problem originally from: https://train.nzoi.org.nz/problems/1311

Every light-bulb is initially off, and O(N^2) solutions are too slow.

Emma is a massive nuisance at school by always meddling around with the light switches. Each day, she goes to toggle a selection of the school's N light switches, numbered from 1 to N. If the selected switch is originally on, she turns it off, and if it is originally off, she turns it on.

Emma chooses her light switches in a very particular way. For each day i, she starts at the ki-th light switch and moves towards higher-numbered switches, toggling every pi-th switch until she runs out of switches.

After D days, Emma is caught and is expelled from her school. You need to find the final states of all of the school's light switches.

All switches are initially off, and you can assume that no one else touches the switches.

I'm just wondering what would be a good way to go about this problem? It's a harder variation of the classic light bulb problem which can be seen here: https://math.stackexchange.com/questions/11223/the-final-state-of-1000-light-bulbs-switched-on-off-by-1000-people-passing-by

https://www.youtube.com/watch?v=-UBDRX6bk-A

The original problem being, you have 100 light bulbs, and you flip every 2nd light bulb, go back to the start, and flip every 3rth light bulb, ... all the way till you start doing every 100th. But instead, in this new problem, instead of doing 100 runs, you might only do something like 8 runs. And instead of doing every 5th light bulb starting from 0, which would be a simple 5\*N linear equation.

You might do every 5th light-bulb starting from the 2nd.

I'm not really sure how to solve this problem but, a time-complexity of O(N^2) is too slow. i.e., you can't just simulate doing or have a for-loop for every run given.

**Input**

The first line includes two space-separated integers: N, the number of light switches, and D, the number of days before Emma is expelled.

The following D lines each contain two space-separated integers representing ki and pi for each day.

D \<= N \<= 50000

**Explanations**

In the sample case, on day 1, Emma turns on the 1st switch, and then every 2nd switch after that until she runs out of switches:

```
ON
OFF
ON
OFF
ON

```

Then, on day 2, Emma starts by turning on the 2nd switch and continues by turning off the 5th switch:

```
ON
ON
ON
OFF
OFF

```

Sample Input 1

```
5 2
1 2
2 3

```

# Answer
Thanks to Vladislav Bezhentsev, and another article I read online, I now have a solution which is O(N * max(p\_i)).

The way this works, is, there might be 50k different combinations of K, and P given. But P is at most 50. So, previously we were doing 50k for loops simulating turning on/off light bulbs.

But now, we just have an array saved that gives us all possible K, and P combinations. Lets call it Query\_array, with all values 0 initially.

Query\_array is a 2D list which has dimensions \[0..50\] by \[0 .. N\] (both inclusive)

You also have a light\_bulb array that's size N, keeping track which light-bulb is on/off (which we loop over at the end to print ON OFF ON or whatever). And all values are 0 initially.

if K, and P come up, save Query\_array\[P\]\[K\] += 1

You loop through all P values, and then through all K mod P values.

For some specific P, and K mod P. You start off with amount\_of\_equations\_so\_far = 0

And then you loop through all values between K mod P, and N,

Going... K, K + P, K + 2P, K + 3P... \<= N

You go:

amount\_of\_equations\_so\_far += Query\_array\[P\]\[K\]

light\_bulb\[K\] += amount\_of\_equations\_so\_far

amount\_of\_equations\_so\_far += Query\_array\[P\]\[K + P\]

light\_bulb\[K + P\] += amount\_of\_equations\_so\_far

amount\_of\_equations\_so\_far += Query\_array\[P\]\[K + 2P\]

light\_bulb\[K + 2P\] += amount\_of\_equations\_so\_far

...

All the way till you pass N.

So this is basically just, 1 for loop, for all values of K which have the same value mod P. Rather than, doing an individual loop for K, and then another for K + P. And recalculating over-and-over again.

My solution below, but it could be more efficient.

# https://train.nzoi.org.nz/problems/1311

N, D = [int(x) for x in input().split()]

switches = [0 for _ in range(N)]

something_started = []

for p in range(51):
    something_started.append([])
    for k in range(N):
        # Shows nothing started at value k, using p step_length
        something_started[p].append(0)

for i in range(D):
    k, p = [int(x) for x in input().split()]
    # with jump value p, something started at k
    something_started[p][k-1] += 1

for p in range(1, 51):
    for k in range(p):
        how_many_are_mod_k = 0

        # Checks all values starting at value k, ending at N, checking all values that are mod K
        # Just like a smartly done for loop

        # Why is this faster?
        # You're not doing a for loop for every D value
        # There can be 50k p, and k combos given.
        # Instead of looping for each of them, if a lot of them are the same P value, all K mod P values are grouped together
        for light_bulb_i in range(k, N, p):
            # print(p, light_bulb_i)
            how_many_are_mod_k += something_started[p][light_bulb_i]
            switches[light_bulb_i] += how_many_are_mod_k

for light_bulb in switches:
    if light_bulb % 2 == 0:
        print("OFF")
    else:
        print("ON")
```

> 0 votes

---
Tags: algorithms, discrete-mathematics
---


# Question
Title: What is the time complexity of this Java program?
Below is the code.

```
public static boolean twoPositive(int[] num) {
    int i = 0;

    while ( i < num.length ) {
        int j = i + 1
        while (j < num.length) {
            if (Math.min(num[i], num[j]) > 0)
                return true;
            j++;
        }
        i++;
    }
    return false;
}

```

From my own understanding, as there is a nested loop, this is of O(n^2), which is the upper bound. It also seems to me that the lower bound is of O(n^2), as regardless of the array, it still has to go through both loops. Is this reasoning correct?

Also, would this mean that every array has exactly the same performance? I know that if an array has two positive integers, it would return true and go through less operations that an array with no positive integers. However, both go through the inner loop, and as both have O(n^2), they have the same runtime.

What do you guys think?

# Answer
> 0 votes
The upper bound (worst - case senario) is when there are 1 or 0 positive numbers in the array because the algorithm will terminate only when i is equal to the number of elements of the array. In this case the time complexity is O(n^2) because there is a nested loop. So for i = 0 ther will be n-1 comparisons for i = 1 n-2 comparisons ... so the total comparisons will be $$\sum\_{i=1}^{n-1} i = \frac{(n-1)(n)}{2} = \frac{n^2}{2} - \frac{-n}{2}$$ which is O(n^2).

The lower bound (best - case senario) is when the first 2 elements in the array are positive numbers so the algorithm will terminate instantly because of the return statement. Since in that senario the algorithm will make only a constant amount of comparisons - no matter the length n of the array - the time complexity will be O(1).

---
Tags: time-complexity, java
---


# Question
Title: How to start with verifying a formal proof programmatically?
I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (don't know which aforementioned camps they belong to), but are completely clueless where I should begin to verify a formal proof programmatically that I just came up with.

For context, I started out with Shawn Hedman's "*A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computatibility, and Complexity*" to learn the very basics. When I got to "Proof by Contradiction" derivation rule, I tried to derive the conclusion from the premises as an exercise, but I got there via a different path, and want to make sure that the steps are sound.

**So what language / tool should I dive into first to verify the formal proofs below? Or am I totally misguided and there's something fundamental that I'm missing?**

For example, this is from the book:

> Premises: ∪ {F } ⊢ G
> ∪ {F } ⊢ ¬G
> Conclusion: ⊢ ¬F
>
> | Line | Statement | Justification |
> | --- | --- | --- |
> | 1 | ∪ {F} ⊢ G | Premise |
> | 2 | ∪ {¬G} ⊢ ¬F | Contrapositive applied to 1 |
> | 3 | ∪ {F} ⊢ ¬G | Premise |
> | 4 | ∪ {¬¬G} ⊢ ¬F | Contrapositive applied to 3 |
> | 5 | ⊢ ¬F | Proof by cases applied to 2 and 4 |

and this is the route I took (which I'm pretty sure is wrong):

| Line | Statement | Justification |
| --- | --- | --- |
| 1 | ∪ {F} ⊢ ¬G | Premise |
| 2 | ∪ {F} ⊢ (¬G v ¬F) | V-introduction applied to 1 |
| 3 | ∪ {F} ⊢ (G → ¬F) | →-definition applied to 2 |
| 4 | ∪ {F} ⊢ G | Premise |
| 5 | ∪ {F} ⊢ ¬F | →-elimination applied to 3 and 4 |
| 6 | ∪ {¬F} ⊢ ¬F | assumption |
| 7 | ⊢ ¬F | Proof by cases applied to 5 and 6 |

Again, I'm not asking to you to tell me if my solution is good or bad, but a learning path on how I can check my work going forward. Thank you!

---

**update (7/19/2023)**: I guess this CS stack exchange thread, Introduction into first order logic verification, answers my question, but I'm not far enough into my studies to decide.

# Answer
In my opinion, it is quite difficult to answer your question because it is very broad. However, I'll try point out several facts that might help you choose a course of action. I will cite the proof assistants (PAs) I know or have been working with.

You correctly stated that mechanical theorem provers (MTPs) are proof assistants (PAs), and probably suspected that they are suitable to their own specific fields. In fact, this is the core of the argumentation: there are many proof assistants, and, depending on their purpose, they can turn out to be suitable for proving a theorem (or not; sometimes they can get very awkward at that).

You mentioned Coq and Agda, and, to the best of my knowledge, these are suitable in the context of mathematical theorem proving. That is, theorem proving oriented towards pure math or logic. On the other hand, Prototype Verification System (PVS) is suitable to verify theorems that represent software safety conditions.<sup>**1**</sup>

There are three parameters that help understand the affinity of a PA w.r.t. theorem proving:

1. the logic employed,
2. its mathematical library, and
3. degree of automation.

#### 1. The logic employed

You should choose a tool that supports an appropriate logic. That is, one that allows you to construct the kind of proofs you want. For instance, Coq uses intuitionistic higher-order logic, and such power allows to prove theorems that are out of grasp of PAs simply employing **higher-order logic**. If you are willing to prove simple properties using **first-order logic** only, this is not a parameter you should worry about.

#### 2. The mathematical library

It is easy to see that proving everything from scratch would require years of work, so consequently, the PA providing a heterogeneous library will make it easier to prove facts of interest. This is especially true when you are proving abstract facts, requiring sophisticated theories. Coq is an example of PA having a rather slim standard library; I recall having problems proving simple facts involving bits and sets of objects. The same problem did not arise when I used PVS.

#### 3. Degree of automation

In general, a proof's purpose is to show that a fact holds and explain why it is the case. In this sense, PAs like Twelf and Coq are very useful, because the proof is carried out by the human prover with the help of the computer, and the result is very informative. In contrast, software safety conditions (correctness proofs) are mathematically shallow, and don't tend to shed light on the problem at hand; in general, they are more interested in knowing whether the program is correct, rather than unfolding several tens of repetitive steps. In most cases, such proofs unfold for hundreds of steps, and very few cases are interesting...

---

Depending on the type of proof you want to get, you need to **choose the proper tool**. For example, PVS would prove your example automatically using automated decision strategies, but the proof itself would be of no value. On the other hand, Coq would force you to carry out every single step, providing a complete yet meticulous proof.

Last but not least, comes the **proof system** used by the PA. Coq and many other PAs employ **natural deduction**, a proof system that I do not enjoy much myself. PVS on the other hand employs **sequent calculus**, a much simpler and clearer proof system, if you ask me.

I my opinion, you should first figure out, **what** you want to prove and, most importantly, **why**. Answering this question will allow you to avoid using PAs that are totally out of scope or that will make you dislike mechanical TP.
> 1 votes

---
Tags: formal-methods, proof-assistants, automated-theorem-proving, interactive-proof-systems
---


# Question
Title: Why is the Turing machine model relevant?
I am learning about computational models, I wonder why Turing chose his model of Turing machines (the strip with the head and Read / Move left or right / Change state). I am suspecting his physical machine Enigma was having a stripe and behaved similarly. Is this correct?

The circuit gates model seems close to what an electronic circuit can do (and seems more natural?), why aren't we using it?

If the two models are equivalent (are they?), then we can just use the simplest ? Why then is the Turing machine model more simple than the other models?

# Answer
It's important to understand that the field of "computability", together with its vocabulary and formalisms, wasn't a thing in Turing's time.

Also, when introducing his machines, he was not trying to come up with a "computer architecture" in the sense understood today, planning a machine that you can build for problem-solving purposes.

Turing was intersted in a meta-mathematical problem that can be roughly stated as: what can a mathematician "solve" in a way that doesn't involve any insight or leap of creativity?$^1$

In his original 1936 paper describing these machines, he dedicates a third of section 9. ("The extent of the computable numbers - (a)") to justifying his "design choices":

He imagines a human trying to solve some mathematical problem, on a typical "child's arithmetic book", with the page divided into squares:$^2$

* the "pages" are irrelevant, simply glue them all side by side to have just one long page
* the "lines" are irrelevant, cut the page and glue the lines side by side to have a really long line
* if you reach the end, buy another notebook, glue it to the end of your current one then keep going; similarly for if you reach the beginning$^3$
* the symbols that can be written in a square must be distinguishable, so their difference can't be arbitrarily small; hence, a finite number of symbols
* the number of observable symbols must be bounded - you can't notice everything at once; you can then straightforwardly argue that if there's a finite bound $B$, you could just as well reduce it to 1; thus a RW head placed over one symbol
* when you're working on the problem, you operate in steps; at any step you can make a decision based on only two factors: what you're observing and what you're thinking, some "mental state";
    + you can choose to write something new; you can choose whether to read on, but you can't just jump with your eyes to some arbitrary point, you wouldn't know where to land; you can only go in a near place to the left or to the right (again, you can straightforwardly argue that you can reduce this to just 1 position L/R); finally you can choose to change your mental state. Hence, you get the transition function of a Turing Machine
* like the symbols used, he argues that mental states must be finite.

From these principles, the Turing Machines follows naturally. Other computational models (e.g. Gödel's recursive functions, Church's lambda calculus) also aimed at answering this question, of what can be resolved "algorithmically"; they were trying to synthesize a vague, intuitive and imprecise philosophical concept as a rigorous mathematical formalism.

Turing's machines were the most compelling; it was the most successful at convincing people that the set of things computable by a Turing machine is indeed the sought-for set of "effectively calculable" things. The fact that other models with the same aim could be formally proven to "compute" exactly the Turing-computable things, served to further cement this idea; that "effectively calculable" is "Turing computable".

---

$^1$ The term used for such tasks was "effectively-calculable"; I recommend reading the first section of the SEP entry on the Church-Turing thesis for more background.

$^2$ You also need to adopt the convention that you write one symbol per square; so no large "m" taking two squares.

$^3$ It's very important, IMO, to understand that a Turing Machine doesn't require "infinite" amounts of tape; in fact, at any point $i$ of computation, at most $i$ squares can be non-blank, always a finite number; you just need "an arbitrarily large number"
> 2 votes

# Answer
The Turing machine is a very simple concept, based on two components: the program (a finite state machine) and an infinite memory (the strip). The FMSs were well-known at the time of Turing, as were the pushdown automata (a refinement of the former). Replacing the stack (of the SA) by a strip increases the power of the machine to an extent considered as sufficient to represent any imaginable computation. (Technically, a Turing machine can handle non-context-free grammars.)

Enigma does not have the power of a Turing Machine and AFAIK, has little in common. It is quite ad-hoc to break the encryption method used by the Germans.

The Turing Machine is a theoretical tool with a sound mathematical representation, which is much more compact and convenient to handle than logical circuits can be. In particular, it is not tied to the binary basis and does not need any diagrammatic routing.
> 1 votes

---
Tags: turing-machines, computation-models
---


# Question
Title: Solving shortest path with negative weights with linear program. What is the underlying problem we want to solve?
Let us consider a shortest path problem with weights $w\_e$ for each edge $e$. It can be formulated as a (integer) linear program (ILP). \begin{align} \min \quad &\sum\_{e \in E} w\_e x\_e \\ s.t. \quad & A\_f x\_e = b\_f \\ & x\_e \in \\{0,1\\} \end{align} Here, $A\_f, b\_f$ are the flow conservation constraints. It is known that $A\_f$ is a totally unimodular matrix so solving the relaxed version above ILP (by letting $x\_e \in \[0,1\]$) gives us an integral solution. When the weights $w\_e$ are all non-negative, the above LP is indeed a shortest path problem.

However, when $w\_e$ can be negative and we allow the negative cycles in the graph, **what this ILP is actually trying to solve here?** I list some of my conjectures and thoughts below for your reference.

1. Longest path problem: I know that a shortest path problem with a negative cycle can be seen as the longest path problem which is NP-hard. The above ILP is certainly not NP-hard. Actually, the thing is that the above ILP allows a trail (each edge appears only once) instead of a walk (or simple path). But I am still not sure if this ILP tries to solve the shortest trail problem...
2. Min-cost flow problem: The relaxed ILP seems a special case of the min-cost flow problem with unit capacity and unit demand at the source and sink. If it is correct, is there a special name for this kind of problem?

Thanks in advance!

# Answer
Note that the above LP allows you to have a negative weight cycle. That cycle could be edge disjoint from the flow that goes from $s$ to $t$. The cycle still satisfies the flow conservation and capacity constraints. Therefore, the solution of the above LP is not necessarily the shortest trail.

For example, consider the following graph such that each edge has capacity $1$ and weight $-1$.

The LP will assign flow $1$ to edges $(s,t)$, $(a,b)$, $(b,c)$, and $(c,a)$; and it will assign flow $0$ to the edges $(s,a)$ and $(b,t)$. Thus, the cost of the optimal solution is $-4$.

However, the shortest trail is: $s \to a \to b \to t$ of cost $-3$.
> 0 votes

---
Tags: shortest-path, linear-programming, network-flow
---


# Question
Title: Number of unique prefixes in canonical huffman tree
I am trying to implement decompression algorithm based on huffman trees. I am trying to validate my assumptions.

Assume that you have alphabet of 350 symbols. Maximum encoded code length is 15 bits. How many different combinations of first 9 bits of each code longer than 9 bits can be encoded in this tree ?

I am only interested in these first 9 bits of codes which have length \> 9 bits, since they determine memory requirement of the algorithm..

Tree is ordered by bit length, so that shorter codes lexicographically precede longer ones.

---

By my thinking there are 2 edge cases:

1. Each code has same length: whole tree can be encoded on $log2(350) \approx 8.5 \< 9$ bits and i don't need to worry about codes with length \> 9, since there aren't any.
2. Tree is maximally right-heavy, as many code as possible have length of 15 bits. Last 6 bits can encode $2^6 = 64$ symbols, since we need to encode 350 symbols, we can get the factor of 6 to cover all symbols by extending maximally branching tree upwards 3 bits. In this case codes which have maximum bit length share 6 bit prefix, have 3 bits different and then have 6 bit suffix that is irrelevant at this point.

Thanks to the ordering constraint, codes with similar lexicographic value and similar lengths will be grouped (will share same region of the tree, therefore same prefix)

---

In other cases, there is no way to create tree(provided maximum code length, number of encoded symbols and ordering of the code is satisfied) that would require more space.

If I assume most codes have bit length of let's say 11, that means I need to store $$2^{11-9=2} = 4 $$ codes for each prefix. In order to encode 350 symbols, I would extend the branching upwards 7 bits, creating at most 128 unique blocks(each block groups codes with same 9 bit prefix) , and I would need to store $128\*4=512$ additional codes.

And since tree is ordered, longest codes will always be on the "right" and will be lexicographically grouped.

---

By these assumptions I came to the conclusion that I need to be able to store $512 + (8 * 64) = 1024$ codes. first 9 bits can be stored directly, and if code has length \> 9, there is maximum of 8 different 9-bit prefixes, and for each unique prefix I need to store $2^6=64$ available combinations for 6 bit suffix.

Seems about right, but I would still like for someone to prove me wrong if I am.

# Answer
> 1 votes
Your worst case scenario is when you have many 10 bit codewords. The trick is to consider the worst possible case starting from the right.

```
0,
100,
101000,
1010010,
10100110,
101001110,
1010011110, ... (total 2)
1010011111,
1010100000, ... (total 32)
1010111111,
1011000000, ... (total 64)
1011111110,
1011111111,
1100000000, ... (total 256)
1111111101,
1111111110,
1111111111,

```

total 354 codes of length 10 meaning 177 different 9bit prefixes.

---
Tags: coding-theory, encoding-scheme, huffman-coding
---


title: Huffman Coding vs Arithmetic Coding

text:
# Question
Title: Huffman Coding vs Arithmetic Coding
Are there conditions under which given text $T$ that huffman code and arithmetic code will produce the exact encoding of $T$?

# Answer
> 0 votes
yes, if all probabilities are in form of $2^{-k}$ then the arithmetic encoding will be the same as huffman encoding. both achieving the expected length of $H(X)$ (entropy).

In such conditions branching in arithmetic coding will be exact and behave the same way huffman coding does.

---
Tags: information-theory, hamming-code
---


# Question
Title: Alghorithm to calculate x, y positions of a grid with the following numbers (details inside)
I have a 2D array grid where each cell has a number in it, i would need a alghorithm that returns me the value of that cell depending on the X, Y position (0, 0 is bottom left)

This is the grid in question, it can be infinite in size and "grows" in such a way that it always adds first the right outer edge, starting from the bottom and then goes to the left until it comes back to the edge. For example the next full "square" of this itteration would be:

What i would need a function that given x, y positions would return me that number. Example:

```
getValue(0, 0) = 0
getValue(0, 1) = 1
getValue(0, 2) = 4
getValue(1, 0) = 3
getValue(3, 3) = 12
getValue(6, 6) = 42
getValue(6, 0) = 48

```

The function should ofcourse calculate this value in some fashion and not get it from some premade grid of finite size, since the input of those value could be very large.

# Answer
> 2 votes
I am not sure if there is a direct way to compute the entries given the row and column, but here's one that works. Let $M$ be your matrix. The value of $M\[i,j\]$ is given by:

$$ M\[i,j\]=\begin{cases} j^2 + i & \text{if $j \ge i$ }\\ i^2 + 2i - j & \text{otherwise} \end{cases} $$

This comes from the observation that the values in the bottom row are perfect squares, that is $M\[0,j\] = j^2$ while those on the leftmost column are one less than a perfect square, $M\[i,0\] = (i+1)^2 - 1 = i^2 + 2i $. Other entries can be determined by computing their distance from either of the two.

---
Tags: algorithms, number-theory
---


# Question
Title: Looking for efficient algorithm to pick out a unique equivalence class representative for 2D arrays with lots of symmetries
Given 2D arrays (number of rows between 0 and 10, number of columns between 0 and 10, elements are integers between 0 and 31) Two arrays $A,B$ are *equivalent* $A\sim B$ if $A$ can be transformed into $B$ via permutations of

* rows
* columns
* alphabet

e.g. $\begin{pmatrix} 1&2&3\\ 2&2&3 \end{pmatrix} \sim \begin{pmatrix} 1&1&2\\ 1&3&2 \end{pmatrix} $ by

* permuting the two rows
* permuting columns 1 and 2
* permuting the digits 2-\>1, 3-\>2, 1-\>3.

I am looking for an efficient algorithm to pick out a unique member for these equivalence classes for lookup in a cache table. Currently what I am doing is:

Loop through all permutations of rows
Loop through all permutations of colunms
Permute digits so that this array is lexicographically minimum (the first digit is 0, the next un-mapped digit is 1 etc). And taking the minimum (again, lexicographically) of these.

Obviously, one can improve on that by only considering as the first row any row that has the greatest multiplicity of characters. But I'm sure there is massive speedup to be had here. I am just not seeing a great way of finding it.

**Edit**
I want a function that is a many-to-one mapping of these 2D arrays to a representative of the equivalent class, i.e. all matrices that are equivalent are mapped to the same output. I want this operation to be quick, fewer operations is better.

Ideally each equivalence class can be mapped to a hashable object (like an integer or string) But if the output is a unique class representative that works too.

# Answer
Your problem is related to graph isomorphism, for which there is no known polynomial-time algorithm. Therefore, you should not expect any efficient algorithm that works on all cases.

In particular, your problem is GI-hard, so there is unlikely to be any efficient algorithm that works correctly on all problem instances (unless the matrices are quite small). In practice, you can use a software package like nauty, bliss, etc.

Why? Well, I will show that if there is a polynomial-time algorithm for your problem, then there is a polynomial-time algorithm for testing isomorphism of two bipartite graphs. It is known that the latter implies a polynomial-time algorithm for graph isomorphism. But no such algorithm is known, and it is a famous open problem whether such an algorithm exists. So don't hold your breath waiting for a polynomial-time algorithm for your problem, either.

Here is the reduction. Let $G\_1,G\_2$ be two bipartite graphs, and $A\_1,A\_2$ be their $n\times n$ adjacency matrices (here $n=|V\_1|+|V\_2|$). Then $G\_1,G\_2$ are isomorphic iff their adjacency matrices are equivalent up to row/column swaps. (You don't have to worry about permutations of the alphabet, since the alphabet is $\\{0,1\\}$, and a swap of 0/1 will increase the number of 1's in the adjacency matrix.) If we had a polynomial-time algorithm for your problem, we could apply it to $A\_1,A\_2$ to get their canonical representatives $R\_1,R\_2$; now $R\_1=R\_2$ iff $A\_1,A\_2$ are row/column-swap-equivalent, i.e., iff $G\_1,G\_2$ are isomorphic.

If you have to solve your problem in practice, you could use existing software tools for graph isomorphism, e.g., nauty, bliss, etc., to compute a canonical representative for the equivalence class under graph isomorphisms of the colored complete bipartite graph induced by your matrix. Specifically, if you have a $m\times m$ matrix $M$, then the corresponding bipartite graph has $2m$ vertices, with an edge from $i$ to $j$ carrying color $M\[i,j\]$ for each $i,j$.

See also https://math.stackexchange.com/q/159992/14578, https://mathoverflow.net/q/59991/37212, https://en.wikipedia.org/wiki/Graph\_canonization.
> 2 votes

# Answer
If you are literally looping through all row permutations, and for each one looping through all column permutations, then you're spending at least $O(n!^2 \cdot poly(n))$ time on that; note that if you define the lexicographical order based on rows, so in your example `1,2,3,2,2,3` vs `1,1,2,1,3,2`. Then you can do much better by simply iterating only over column permutations, and for each column permutation you don't need to loop over row permutations; once your columns are fixed just sort the rows lexicographically. This brings you down from $O(n!^2 \cdot poly(n))$ to $O(n! \cdot poly(n))$.

As you correctly suggest, you can assume without loss of generality that your first row will start with as many $1$s (or $0$s) as possible. That means that you don't even need to consider all column permutations, but only the ones that: make some row start with $M$ occurrences of the same digit where $M$ is maximized. So in particular, given there are only $31$ possible values, you can do:

```
for each $v \in \{0, ..., 31\}$:
 let $m_v$ be the maximum number of occurrences of $v$ in some row of the matrix.

let $S$ be the set of $v$'s that maximize $m_v$.
initialize $C = \emptyset$ as the set of the column permutations to try.
for each $v \in S$:
   let $R$ be the set of rows in which $v$ appears $m_v$ times.
      for each row $r \in R$:
         add to $C$ all the column permutations that leave all occurrences of $v$ at the beginning.

```

This will likely give you a much smaller set of column permutations to try, although your parameters are small enough that it might end up wasting time in cases where the number of permutations to consider are not significantly reduced (e.g., some row contains only a single number).

For a more theoretical discussion, refer to this math stackexchange equivalent question.
> 2 votes

---
Tags: algorithms, optimization, sorting
---


# Question
Title: Finding a vector of maximum Hamming distance from a subspace of $(\mathbb{Z}/2\mathbb{Z})^n$
Let $W$ be a linear subspace of the vector space $V = (\mathbb{Z}/2\mathbb{Z})^n$. Let $k = \dim(W)$. For $v \in V$, define the distance from $v$ to $W$ to be $d(v,W):=\min\_{w\in W} d(v,w)$ where $d(v,w)$ is the Hamming distance.

Given such a subspace $W$ (more precisely, receiving a basis of $k$ vectors as input), how can I find a vector $v \in V$ such that $d(v,W)$ is as large as possible?

The cases I'm interested in have $n$ in the thousands, but $k$ being quite small, usually less than 20. I have been able to solve some smaller instances of this problem ($n$ being a few hundred, $k$ being at most 6 or so) using the SAT/SMT solver Z3 by creating $n$ Boolean variables and explicitly writing out $d(v,w)\geq r$ for all $2^k$ elements of $W$ as clauses. The inequality is encoded using a pseudo-boolean constraint (`pb-ge` in Z3) stating that at least $r$ of the $n$ literals must be true in each clause. I then use a binary search to find the maximum value of $r$ where the formula is satisfiable.

Example: Let $n = 100$ and $W$ be the subspace spanned by the following three elements (I'll compress the notation a bit and write a vector like $(a,b,c)$ as $abc$):

1011000001001001000110000000110010000010111011100101010000010101001000000011001000011001110010000000 0100101000001010101011010000000001001000101111100010000010000001011101000001100100010001000100010010 1110010000000000110001011000110001000010011000001000101001001100100110100001010000011000001000110100

Then a solution to the problem is given by the following vector $v$:

1101101110110101010011101111011100111101110000010110110111111011101110011101100011101110110001101011

which has Hamming distance at least 64 from every linear combination of the three vectors above. Distance 65 from every linear combination is not possible.

Some additional questions:

* Does this problem have a name?
* Is there a faster (in practise, not necessarily in theory) algorithm than what I am currently doing?
* If so, is there an implementation that I can use?

# Answer
> 2 votes
Your problem is very likely NP-hard. If you don't add the restriction that $W$ is sub-space, but just receive a set of boolean vectors $W$, then it is NP-hard and known as a *Covering Radius* proven NP-hard by Frances and Litman. Of course it might be that $W$ being a sub-space somehow makes the problem easier, but I can't see a particular way for that to happen.

# Answer
> 0 votes
You may be interested in some linear algebra over finite field $\mathbb{F}\_2$. Basically, vectors in the linear complement to $W$ should have the maximal Hamming distance. The trouble is that linear algebra over finite fields is not as straightforward as over $\mathbb{C}$. Nevertheless, linear algebra over $\mathbb{F}\_2$ has been applied to Hamming codes.

---
Tags: algorithms, optimization, satisfiability, linear-algebra, hamming-distance
---


# Question
Title: Proving that this Huffman tree construction is valid
**"Abstract":**
I have recently crafted a new algorithm for constructing code trees which I believe are optimal (the same thing that is constructed using Huffman's algorithm, at Wikipedia). It is based on one observation which is in form of an illegal property (i.e. code trees with that property are not optimal) and several other propertires which aren't exactly illegal in the same sense but help recognize a more favorable code tree. This ambiguity at the end is exactly what I fail to analyze and hope someone will help me at. I will try to explain all of my notation so people with any background can understand this.

**The main goal:**
Produce a simple algorithm which builds an optimal code tree for a sorted set of frequencies in linear time.
The sample C++ code is here, look at the function `ht`.

For that sake let's say we are given a sorted array of "frequencies" $f$ of length $n$: $f(a)\ge f(b)$ whenever $1\le a\le b\le n$. *(We can think of $f(i)$ as of the probability that the $i$-th symbol will occur in a string, but they are not normalized - their sum isn't 1)*.
The length of the code for the $i$-th symbol I will call $h(i)$.

**The main observation:**
The lengths of the codes should be ordered oppositely of the frequencies: $a\le b\Rightarrow h(a)\le h(b)$. If for some $a\<b$ we have that $f(a)\>f(b)+f(b+1)$, then an optimal $h$ must satisfy $h(a)\<h(b+1)$.

Now let me give the argument for proving this. Assume the opposite: $h(a)=h(b+1)=:H$ (we define $H$ to equal this). Consider the range of all indices which map to $H$ under $h$ (the preimage of $h$), say this range has indices $x\le y$. So now we have that $h(x-1)\<h(x)=H=h(y)\<h(y+1)$ (assuming $x-1$ and $y+1$ are valid indices, of course). We must have that $y\ge b+1\ge a+2\ge x+2$. Now the claim is (which I have proven, but won't write it here in attempt to keep this question short) that if we change the values of $h(x)$, $h(y-1)$ and $h(y)$ to $h(x)-1$, $h(y-1)+1$ and $h(y)+1$, then this new $h$ still admits a valid binary tree (code tree), which has the lower value of $\sum f(i)h(i)$, which is the very thing we want to minimize.

An opposite respectively holds: if for some $a\<b$ we have that $f(a)\<f(b)+f(b+1)$, then an optimal $h$ must satisfy $h(a)+1\ge h(b)$ *(which is similar to $h(a)+1\le h(b+1)$ from before)*. This means that the values of $h$ can't get too high either. In some sense they are in tight relationships.

**The algorithm:**
Using these two observations I meditated on this procedure:

1. Set the current index, $c$, to $1$ and currect weight, $t$, to $0$.
2. While $c\le n$:
2.1. Find the least index $b$ such that $f(a)\ge f(b-1)+f(b)$ if such exists, otherwise set $b=n+1$.
2.2. Set $h(i)$ to $t$ for all $i$ for which $a\le i\<b$, and then set $c$ to $b$ and increment $t$.

Now the problem is that the sum $\sum2^{-h(i)}$ should be a power of $2$, but this procedure doesn't guarantee it. Now, I know that I can increment some of the values of $h$ so that they don't cross the bounds I described in my observations. I performed this correction using this:

1. Define the $i$-th weigth, $w(i)$, to be $2^{-h(i)}$.
2. Calculate the sum $S:=\sum w(i)$.
3. Find the smallest power of $2$, $P$, which is strictly greater than $S$, and then calculate their difference $D:=P-S$.
4. Set the currect index, $c$, to $1$.
*Now we proceed to cut the $D$... down to $0$.*
5. While $c\le n$:
5.1. If $D\ge w(c)$, set $D$ to $D-w(c)$ and decrement $h(c)$.
5.2. Increment $c$.
6. (renormalization) Recalculate $w$'s and $S$. $S$ will be a power of $2$: $S=2^m$ for some non-negative integer $m$.
7. Add $m$ to every $h(i)$.

This should produce the optimal lengths $h$ of binary codes for frequencies $f$. That is my hypothesis. I would appreciate if someone could tell me some illegal property and then analyze my algorithm to see whether it avoids it or not, ultimately maybe prove it or give a counter-example. My reach is the discovery of these tight bounds, but I fail to confidently analyze the rest.

# Answer
I liked your observations really good but unfortunately your algorithm cannot handle more than 1 depth difference at a time. I tested it with f = \[6,1,1,1,1\]. the h = \[2, 2, 2, 3, 3\] while the actual algorithm output is \[1,3,3,3,3\]. For testing I had to rewrite your code in python so I can understand it easier.

```
import math

def test(f, h):
    n = len(f)
    j = 0
    ph = h[0] = 32
    cs = 0x100000000
    ts = 0x100000000
    for i in range(1, n):
        if f[i-1] + f[i] <= f[j]:
            j = i
            ph -= 1
            cs >>= 1
        h[i] = ph
        ts += cs
    bts = math.ceil(math.log2(ts-1))
    ex = (1 << bts) - ts
    for i in range(n):
        cv = 1 << h[i]
        if (cv<=ex):
            ex-=cv
            h[i] += 1
    for i in range(n):
        h[i] = bts - h[i]
    r=0
    for i in range(n):
        r += f[i]*int(h[i])

f = [6,1,1,1,1]
h = [0]*len(f)
test(f, h)
print(f)
print(h)

```
> 0 votes

---
Tags: algorithms, huffman-coding, linear-complexity
---


# Question
Title: Can a linear programming method be used to solve systems of inequalities with OR (disparate) compound inequalities?
I recently discovered linear programming and it seemed perfect for a CS problem I wanted to solve a few months ago. This task involved solving a large quantity of inequalities at once.

For example, one such system could be

```
X1,X2,X3,X4 >= 0
X1 >= X3 + 3.0 or X1 < X3 - 7.2
X2 >= X4 + 5
X2 >= X3 + 3.0 or X2 < X3 - 5.3
X2 >= X1 + 7.2 or X2 < X1 - 5.3

```

And then some reasonably complex objective function in terms of X1, X2, X3, X4. In fact, the function mostly just needs to aim to reduce the spread of the variables, whilst finding *a* solution.

(Optimally, the program would aim to find a solution that meets as many inequalities as possible, to allow it to find a "close enough" solution when there is no actual solution)

I can't find anyone else talking about the limitations of linear programming, but I understand these inequalities are only "kinda" linear. If anyone out there, perhaps with a formal higher CS education, I'd much appreciate it.

If this is not possible with normal linear programming algorithms, any leads into possible solutions would be much appreciated.

Thanks all in advance!

# Answer
First off, a couple of observations.

If you allow three inequalities in each "compound inequality", then the problem of finding a feasible solution is NP-complete, since any 3-SAT problem can be recast as this problem.

The problem in parentheses, where you try to fit the maximum number of constraints, is NP-hard, for essentially the same reason: MAX-2-SAT is NP-hard.

OK, with that out of the way, this is called disjunctive programming, and the usual way to solve problems of this form is to introduce boolean variables to handle the disjunction, which turns it into a mixed-integer linear programming problem which is, again, NP-complete in general.

The feasibility problem (as opposed to the optimisation problem) can be directly implemented as a SMT problem and also has a natural expression in CLP(R).
> 2 votes

---
Tags: algorithms, linear-programming, linear-algebra
---


title: Collinear convex hull

text:
# Question
Title: Collinear convex hull
Is there an algorithm where I provide a list of non-overlapping squares, for example:

```
sq1 = [(0, 0), (0, 1), (1, 1), (1, 0), (0, 0)]
sq2 = [(1, 0), (1, 1), (2, 1), (2, 0), (1, 0)]
sq3 = [(1, 1), (1, 2), (2, 2), (2, 1), (1, 1)]

```

and it will return some sort of "collinear convex hull" where the results will be?:

```
res = [(0,0), (0,1), (1,1), (1,2), (2,2), (2,0), (0,0)]

```

If I try the regular convex hull algorighm, it returns

Update: Every square will share at least one side with another, but if for examples there is an empty square in the middle of a 9x9 grid:

```
sq1 = [(0, 0), (0, 1), (1, 1), (1, 0), (0, 0)]
sq2 = [(0, 1), (0, 2), (1, 2), (1, 1), (0, 1)]
sq3 = [(0, 2), (0, 3), (1, 3), (1, 2), (0, 2)]
sq4 = [(1, 2), (1, 3), (2, 3), (2, 2), (1, 2)]
sq5 = [(2, 2), (2, 3), (3, 3), (3, 2), (2, 2)]
sq6 = [(2, 1), (2, 2), (3, 2), (3, 1), (2, 1)]
sq7 = [(2, 0), (2, 1), (3, 1), (3, 0), (2, 0)]
sq8 = [(1, 0), (1, 1), (2, 1), (2, 0), (1, 0)]

```

Then the result would be:

```
ret = [(0, 0), (0, 3), (3, 3), (3, 0), (0, 0)]

```

So ignoring the "hole" in the middle. This would be the same results generated by the "regular" Convex Hull algorithm.

However, if instead I have:

```
sq1 = [(0, 0), (0, 1), (1, 1), (1, 0), (0, 0)]
sq2 = [(0, 1), (0, 2), (1, 2), (1, 1), (0, 1)]
sq3 = [(0, 2), (0, 3), (1, 3), (1, 2), (0, 2)]
sq4 = [(1, 2), (1, 3), (2, 3), (2, 2), (1, 2)]
sq5 = [(2, 2), (2, 3), (3, 3), (3, 2), (2, 2)]
sq6 = [(2, 1), (2, 2), (3, 2), (3, 1), (2, 1)]
sq7 = [(2, 0), (2, 1), (3, 1), (3, 0), (2, 0)]

```

Then the result should be:

```
ret = [(0, 0), (0, 3), (3, 3), (3, 0), (2, 0), (2, 2), (1, 2), (1, 0), (0, 0)]

```

# Answer
The problem is to find the outer boundary of the union of the squares. We state two claims that help design an $O(n)$ algorithm, where $n$ are the number of given squares.

Let $S\_1,\dotsc,S\_n$ be the set of given squares. Each square boundary is composed of four line segments. Let $L = \\{\ell\_1,\dotsc,\ell\_m\\}$ be the multiset of all the line segments of all squares. By the definition of the boundary, the following claim holds:

*Claim 1:* A line segment $\ell\_i \in L$ forms the boundary of the union if and only if it appears exactly once in the multiset $L$.

The above claim is easy to see. That is, if a line segment $\ell\_i$ appears more than once in $L$, then it is shared by some two squares thus it is not a part of the boundary of the union. Now, we state the second claim.

Let $L'$ be the set of line segments that appears exactly once in $L$. Since each square shares at least one side with another square, the following claim holds:

*Claim 2:* Each line segment $\ell\_i \in L'$ shares each of its end point with one other line segment in $L'$.

Using claim $1$ and $2$, the following algorithm finds the outer boundary $B$ of the union of the squares:

1. Given $L$, find $L'$ using a hash map in $O(n)$ time.
2. Let $E$ be the set of all end points of the line segments in $L'$. Create a hash map $H$ such that each endpoint in $E$ maps to the two line segment in $L'$ which incident on it. It can be done in $O(n)$ time.
3. Let $e\_l$ be an endpoint in $E$ that has the least $x$ coordinate value. This endpoint is definitely a part of the outer boundary. Add $e\_{l}$ to set $B$.
4. Let $\ell\_e$ be one of the line segment in $L'$ that is incident on $e\_l$. The line segment $\ell\_e$ can be found in $O(1)$ time using hash map $H$.
5. Let $e'$ be the other end point of $\ell\_e$. Add $e'$ to $B$.
6. Repeat step $4$ with $e\_l$ replaced with $e'$ till the complete boundary is traversed. The complete boundary is traversed when $e\_l$ is encountered again.

The step $4$ and $5$ can be implemented in $O(1)$ time using hash map. Therefore, the overall running time is linear in $n$, i.e., $O(n)$.
> 1 votes

---
Tags: algorithms, convex-hull
---


# Question
Title: Find directed spanning tree of unweighted directed graph in $O(|V| + |E|)$
A directed tree (also called an arborescence) of $G$ is a directed subgraph of $G$ in which there exists a vertex $v$ such that there is a unique path from $v$ to every other vertex in the graph.

Please help with an $O(|V| + |E|)$ algorithm that finds a directed spanning tree in $G$ or notifies if there is none.

# Answer
If an arborescence exists in $G$, its root must be a node in a strongly connected component with in-degree $0$, as any node inside it is unreachable from the outside. Similarly we find that if more than one strongly connected component with in-degree $0$ exists, no arborescence is possible, as either strongly connected component will not be reachable from the other.

Thus to find such an arborescence, run Tarjan's strongly connected components algorithm which takes $O(|V| + |E|)$ time. Loop over all the strongly connected components and find one with in-degree $0$, which takes $O(|V|)$ time. Keep looping and if you find a second one with in-degree $0$, report that an arborescence does not exist.

Once you found the unique strongly connected component with in-degree $0$, simply pick any node in it and construct an arborescence rooted at it using a $O(|V| + |E|)$ depth-first search, as every other node is reachable from this one.
> 2 votes

---
Tags: algorithms, graphs
---


# Question
Title: Check whether set of strings is prefix-free via lexicographic sort?
I have a set of strings and would like to establish whether the set has the prefix property, which basically means that no string in the set is a prefix of any other string in the set. So `{a, b}` is prefix-free (has the prefix property) while `{a, b, ba}` is not prefix-free (lacks the prefix property) because the entire string `b` is a prefix of `ba`.

One can of course implement this with a double-loop for quadratic performance. In JavaScript (so you can pop open your browser’s JS Console and try it, if so inclined):

```
function isPrefixCode(strings) {
  for (const i of strings) {
    for (const j of strings) {
      if (j === i) {
        continue;
      }
      if (i.startsWith(j)) {
        return false;
      }
    }
  }
  return true;
}
isPrefixCode(new Set('a b c'.split(' '))) // true
isPrefixCode(new Set('ba b c'.split(' '))) // false

```

I *think* one can do better by sorting the set of strings lexicographically ($N \log N$), then comparing each element to its previous one (linear). So:

```
function isPrefixCodeLinear(strings) {
  strings = Array.from(strings).sort();
  for (const [i, s] of strings.entries()) {
    if (i === 0) {
      continue;
    }
    const prev = strings[i - 1];
    if (s.startsWith(prev)) {
      return false;
    };
  }
  return true;
}
isPrefixCodeLinear(new Set('a b c'.split(' '))) // true
isPrefixCodeLinear(new Set('ba b c'.split(' '))) // false

```

This linearithmic algorithm seems to work for the tests I’ve come up with (and ~100x speedup over the quadratic double-loop algorithm on a 1000-string example), but I’d like to ask

1. if this approach based on lexicographic sorting is guaranteed to work,
2. if this approach has a name, and
3. if the prefix property has a more common term in computer science, or
4. if there are other algorithms that can solve it.

(I found this question on StackOverflow, about finding whether any entry in a set of strings is prefixed by a specific given string, How to search whether a string is a prefix of strings stored in a set?, which is a related problem to mine, but here I want to consider not just any one string but all the strings in the set.)

# Answer
1. Yes. The common prefix is maximal with the closest predecessor (if you're treating the empty string as less than any other, which you are). Edit: in general if a prefix key exists it will be the immediate predecessor or there will be another key in between which shares the same prefix, and your test will fail on that. eg ABC, ABCD, ABCE will fail on the first pair even though the last key also contains ABC and is non-consecutive. The LCP is indeed maximal with the closest ~~predecessor~~ neighbor, but that ~~predecessor~~ neighbor may not be a prefix; I just wanted to clarify that.
2. There are situations where the longest common prefix is useful; in particular to augment a suffix array, which is a sorted list of suffixes. Look up LCP Array. The LCP+1 (roughly) is called the distinguishing prefix; string sorting algos express their complexity in terms of O(n log n + D), where D is the sum of all the distinguishing prefixes of all the keys. So it's a familiar idea.
3. "Prefix free" is the term that I remember.
4. You can put them in a trie and look for strings that end on an intermediate node. It's a variant of sorting.
> 2 votes

# Answer
I had to solve this problem recently. Here's the Python implementation I came up with, which includes a (rough) proof using a mixture of Python and mathematical notation:

```
def is_prefix_free(values: Iterable[str]) -> bool:
    '''determine if a list of strings is prefix-free
       (i.e., no element of 'values' is a prefix of any other)

    Args:
        values: any iterable of strings
    Returns:
        True iff there is no solution (i, j) to the following
        statements:

            values[i].startswith(values[j])
            i >= 0
            j >= 0
            i != j

    Approach:

        We sort 'values' and examine adjacent pairs: once sorted, iff
        'svalues[i]' is a prefix of 'svalues[j]' (i != j), then there
        must exist an adjecent pair of 'svalues[k], svalues[k+1]' s.t.
        'svalues[k]' is a prefix of 'svalues[k+1]'.

    Rough proof of validity for this approach:

        Let s := svalues (as defined in 'Approach'; for brevity).

        The approach assumes that the list is prefix-free IFF the sorted
        list is pairwise prefix-free. We can validate this by showing
        that each condition implies the other.

        It's trivial to demonstrate that presence of an adjecent prefix
        pair in the sorted list implies the presence of an
        (unrestricted) prefix pair in the unsorted list, as these lists
        contain the same elements.

        The rest of this proof focuses on proving the converse: that
        the presence of an (unrestricted) prefix pair in the unsorted
        list implies presence of an adjecent prefix pair in the sorted
        list.

        Per the problem, we assume:

            i != j                                                  [0]

        Suppose the assumptions given in 'Approach' are untrue,
                i.e.,:
            s[j].startswith(s[i]), but                              [1]
            ∄k | s[k+1].startswith(s[k])                            [2]
        We show that this leads to contradictions in all cases.

        ∀ a,b: s[a] < s[b] => a < b                                 [3]

        If s[i] = s[j]: contradiction!                              [4]

            i != j  (per [0])

            i < j                                                   [5]
                We may assume this is without loss of generality:
                we may swap i and j if necessary to ensure this
                condition without violating any earlier
                assumption.

            j != i+1                                                [6]
                Suppose j = i+1
                    s[i] = s[j]  (per [4])
                =>  s[i] = s[i+1]
                =>  contradiction! (k=i, per[2])

            i < i+1 < j                                             [7]
                    i < i+1  (trivial algebraic proof)
                    i < j  (per [5])
                    j != i+1  (per[6])
                    (no value exists between i, i+1)

            s[i] = s[i+1] = s[j]  (per [3], [4], [7])               [8]

            contradiction! (k=i, per[2])
                s[i+1].startswith(s[i])
                    s[i] = s[i+1]  (per [8])
                    ∀ v: v.startswith(v)  (trivial proof)

        Otherwise: contradiction!                                   [9]

            i < i+1 < j, and                                        [10]
            s[i] < s[i+1] < s[j]                                    [11]

                i < j                                               [12]
                    i != j  (per [0])
                    Suppose: j < i                                  [13]
                            s[j] ≤ s[i]  (per [3])                  [14]
                            s[i] ≤ s[j]  (per [1], [A1])            [15]
                            s[i] = s[j]  (per [14], [15])
                         => contradiction!  (per [9])

                s[i] != s[i+1]                                      [16]
                    otherwise: contradiction! (with k=i, per[2])

                i+1 != j                                            [17]
                s[i+1] != s[j]                                      [18]
                        s[j].startswith(s[i])  (per [1])            [19]
                        not s[i+1].startswith(s[i])  (per [2])      [20]
                     => s[i+1], s[j] are distinct values            [21]
                                (per [19], [20])
                     => i+1 != j  (per [21], [A2])

                i < i+1                                             [22]
                    (simple algebraic proof)

                i+1 < j                                             [23]
                    i+1 != j  (per [17])
                    i < j  (per [12])
                    (no value exists between i, i+1)

                s[i] < s[i+1]  (per [3], [16], [22])                [24]

                s[i+1] < s[j]                                       [25]
                    i+1 < j  (per [23])
                    s[i+1] != s[j]  (per [18])
                    (per [3])

            ∃ p ≥ 0 s.t. s[i][:p] = s[i+1][:p], and                 [26]
            s[i][p] != s[i+1][p]                                    [27]
                otherwise, one of the following would be true:
                    s[i+1].startswith(s[i])  (contradicts [2])
                    s[i].startswith(s[i+1])
                            (contradicts [3] given [A1])

            p < len(s[i])                                           [28]
                (otherwise s[i][p] would be undefined in [26])

            s[i][p] < s[i+1][p]                                     [29]
                s[i][:p] = s[i+1][:p]  (per [26])
                s[i][p] != s[i+1][p]  (per [27])
                (per [3])

            s[i][:p] = s[j][:p], and                                [30]
            s[i][p] = s[j][p]                                       [31]
                p < len(s[i])  (per [28])
                s[i] = s[j][:len(s[i])]
                    s[j].startswith(s[i])  (per [1])

            s[i][:p] = s[i+1][:p] = s[j][:p]                        [32]
                s[i][:p] ≤ s[i+1][:p] ≤ s[j][:p]  (per [3], [A3])
                s[i][:p] = s[j][:p]  (per [30])

            s[i+1][p] < s[j][p]  (per [32], [36], [A4])             [33]
                s[i][p] != s[i+1][p]  (per [27])                    [34]
                s[i][p] = s[j][p]  (per [31])                       [35]
                s[i+1][p] != s[j][p]  (per [34], [35])              [36]

            s[i][p] < s[i+1][p] < s[j][p]                           [37]
                s[i][p] < s[i+1][p]  (per [29])
                s[i+1][p] < s[j][p]  (per [33])

            Contradiction!
                    s[i][p] < s[i+1][p] < s[j][p]  (per [37])
                =>  s[i][p] < s[j][p]
                =>  s[i][p] != s[j][p]                              [38]
                    s[i][p] = s[j][p]  (per [31])
                    ([38] conflicts with [31])

        Annex (proofs left as an exercise):

            s[b].startswith(s[a])  =>  a ≤ b  (assuming [3])        [A1]

            s[a] != s[b]  =>  a != b                                [A2]

            ∀ q: s[a] ≤ s[b]  =>  s[a][:q] ≤ s[b][:q]               [A3]

            Given:                                                  [A4]
                0 ≤ a < b
                q ≥ 0
                s[a][:q] = s[b][:q]
                s[a][q] != s[b][q]
            =>  s[a][q] < s[b][q]  (per above, [3])
    '''
    values = sorted(values)
    for left, right in zip(values[:-1], values[1:]):
        if right.startswith(left):
            return False
    return True

```

For those who aren't Pythonistas: in Python, sequences and strings are zero-indexed. The slice notation for a string "`some_str[:p]`" means "the first `p` characters of `some_str`", while "`some_str[p]`" means "the `p`-th character, where `p=0` is the first character".

There are probably errors and omissions in the proof, so take it with a grain of salt.

There *must* be a much more elegant proof, but it's not obvious to me what approach one would take.
> 1 votes

# Answer
Here's another proof that doesn't use contradiction:

```
        Given:

            values[q].startswith(values[p])                         [1]

        Assumptions:

            Let s := sorted(values)                                 [2]
            Let i := s.index(values[p])                             [3]
            Let j := s.index*(values[q]), j != i                    [4]
                    i.e., choose the first index matching
                    'values[q]' that isn't also the index 'i';
                     in Python, one might write:
                         j = s[i+1:].index(values[q]) + i+1

        We want to show:

            s[k+1].startswith(s[k]) for at least one k ≥ 0

        Proof:

            s[i] = values[p]  (per [3])                             [5]
            s[j] = values[q]  (per [4])                             [6]

            s[j].startswith(s[i])  (per [1], [5], [6])              [7]

            0 ≤ i < j  (per [2], [4], [7], [A2])                    [8]

            if j == i+1:
                solution: k = i
            otherwise:                                              [9]

            i < i+1 < j  (per [8], [9])                             [10]

            if s[i] == s[j]:                                        [11]
                s[i] == s[i+1] == s[j]                              [12]
                        (per [1], [10], [11], [A3])
                s[i+1].startswith(s[i])  (per [12], [A1])
                solution: k = i
            otherwise...                                            [13]

            s[i] < s[j]  (per [7], [13], [A2])                      [14]

            if s[i] == s[i+1]:                                      [15]
                solution: k = i
            otherwise...                                            [16]

            s[i] < s[i+1]  (per [2], [16])                          [17]

            if s[i+1] = s[j]:                                       [18]
                if j = i+2:                                         [19]
                    s[i+1] = s[i+2]  (per [18], [19])
                    solution: k = i+1
                otherwise:                                          [20]
                    i+1 < i+2 < j (per [10], [20])                  [21]
                    s[i+1] = s[j]  (per [18])                       [22]
                    s[i+1] = s[i+2] = s[j]
                            (per [2], [21], [22], [A3])
                    solution: k = i+1
            otherwise...                                            [23]

            s[i+1] < s[j]  (per [2], [23])                          [24]

            s[i] < s[i+1] < s[j]  (per [17], [24])                  [25]

            let I := len(s[i])                                      [26]

            s[j][:I] = s[i]  (per [7], [26], definition of prefix)  [27]

            s[i][:I] = s[i]  (per [26], trivial proof)              [28]

            s[i][:I] = s[j][:I]  (per [27], [28])                   [29]

            s[i][:I] = s[i+1][:I] = s[j][:I]                        [30]
                    (per [2], [10], [26], [29], [A4])

            s[i][:I] = s[i+1][:I]  (per [30])                       [31]
            s[i] < s[i+1]  (per [17])                               [32]
            s[i+1].startswith(s[i])  (per [31], [32], [A5])
            solution: k = i

    Annex (proofs left as an exercise):

        Given 's', a sorted list of strings:

            s[a] = s[b]                                             [A1]
        =>  s[b].startswith(s[a])

            s[b].startswith(s[a])                                   [A2]
        =>  s[a] ≤ s[b]
        =>  a ≤ b

            a < b < c, and                                          [A3]
            s[a] = s[c]
        =>  s[a] = s[b] = s[b]

            a < b < c, and                                          [A4]
            s[a][:q] = s[c][:q]
        =>  s[a][:q] = s[b][:q] = s[c][:q]

            a < b, and                                              [A5]
            s[a] < s[b], and
            s[a][:len(s[a])] = s[b][:len(s[a])]
        =>  s[b].startswith(s[a])

```
> 1 votes

---
Tags: strings, sets, substrings
---