Duplicated literals in graph reason clause

[instr3]

This is not a crucial issue but I think might be useful for a little bit performance boost.

Issue: When using the graph literal graph-active-vertices-connected, it is possible that it will produce an conflict reason with duplicated literals. The analyzer seems to work fine under this condition though. Here is an example:

(bool b00)
(bool b01)
(bool b02)
(bool b03)
(bool b10)
(bool b11)
(bool b12)
(bool b13)
(bool b20)
(bool b21)
(bool b22)
(bool b23)
(bool b30)
(bool b31)
(bool b32)
(bool b33)
(graph-active-vertices-connected 16 24 b00 b01 b02 b03 b10 b11 b12 b13 b20 b21 b22 b23 b30 b31 b32 b33 0 1 1 2 2 3 4 5 5 6 6 7 8 9 9 10 10 11 12 13 13 14 14 15 0 4 1 5 2 6 3 7 4 8 5 9 6 10 7 11 8 12 9 13 10 14 11 15)
(graph-active-vertices-connected 16 24 (! b00) (! b01) (! b02) (! b03) (! b10) (! b11) (! b12) (! b13) (! b20) (! b21) (! b22) (! b23) (! b30) (! b31) (! b32) (! b33) 0 1 1 2 2 3 4 5 5 6 6 7 8 9 9 10 10 11 12 13 13 14 14 15 0 4 1 5 2 6 3 7 4 8 5 9 6 10 7 11 8 12 9 13 10 14 11 15)
(and b11)
(not b12)
(not b21)
(and b22)

Here is a test code to see the reason clause:

    for (int i = decision_order_.size() - 1; i >= 0; --i) {
        int v = decision_order_[i];
        if (p != lit_Undef && var(p) == var(lits_[v])) {
            abort();
        }

        if (state_[v] == kActive) union_find.AddActiveCount(v, -1);
        for (int w : adj_[v]) {
            if (activated[w]) union_find.Merge(v, w);
        }

        if (union_find.NumActiveClusters() >= 2) {
            union_find.Commit();
            activated[v] = true;
        } else {
            union_find.Redo();
            if (state_[v] == kActive) out_reason.push(lits_[v]);
            else if (state_[v] == kInactive) out_reason.push(~lits_[v]);
            if (state_[v] == kActive) std::cout << lits_[v].x << "," << " ";
            else if (state_[v] == kInactive) std::cout << (~lits_[v]).x << "," << " ";
        }
    }
    std::cout << std::endl;

And the output is:

16, 4, 22, 21, 15, 12, 22, 21, 15, 12, 
31, 22, 21, 15, 12, 22, 21, 15, 12, 
31, 22, 21, 15, 12, 22, 21, 15, 12, 
s UNSATISFIABLE

which contains duplicated literals (22, 21, 15, 12) in each conflict clause.

The reason is that the variables that can be decided during the intialization stage (in this case, b11 b12 b21 b22) were added twice to the variable decision_order_, once in here and once in ActiveVerticesConnected::propagate (since the initialization will call the propagate function on these variables). The solution should be as simple as remove line 95 in graph_solver.cpp, but I am not 100% sure if there could be any side effect.

Test output after the fix:

16, 4, 22, 21, 15, 12, 
31, 22, 21, 15, 12, 
31, 22, 21, 15, 12, 
s UNSATISFIABLE

I have created a pull request #4 for this.