From b3218f2bc3b7d542d385a944f235a3292ea91d0d Mon Sep 17 00:00:00 2001
From: Tilo Wiedera <tilo@wiedera.de>
Date: Mon, 1 Jun 2015 15:35:01 +0200
Subject: [PATCH] Reintroduce Fist Segment Constraints

---
 .../proof/solver/LinearProgramGenerator.java  | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/main/java/proof/solver/LinearProgramGenerator.java b/src/main/java/proof/solver/LinearProgramGenerator.java
index c085971..7c1b4e9 100644
--- a/src/main/java/proof/solver/LinearProgramGenerator.java
+++ b/src/main/java/proof/solver/LinearProgramGenerator.java
@@ -97,6 +97,27 @@ public String createLinearProgram(Map<CrossingIndex, Boolean> fixedVariables, JS
       }
     }
 
+    result.append("\n\\ First Segment Constraints");
+
+    // first segment constraints are generated for fully expanded edges only
+    // note that an edge will cross with at most every non-adjacent edge once
+    for (int e = 0; e < graph.getNumberOfEdges(); e++) {
+      int maxExpansions = graph.getNumberOfEdges();
+
+      for (int f = 0; f < graph.getNumberOfEdges(); f++) {
+        if (graph.areEdgesAdjacent(e, f)) {
+          maxExpansions--;
+        }
+      }
+
+      maxExpansions = Math.min(maxExpansions, graph.getClaimedLowerBound() - 2);
+
+      if (maxExpansions > 0 && expansions[e] == maxExpansions) {
+        result.append("\n" + sumVariables(e, expansions[e]) + sumVariables(e, 0, true) + " >= 0");
+        stats.increase("first segment constraints");
+      }
+    }
+
     for (int i = 0; i < jsonConstraints.length(); i++) {
       result.append("\n\\ Kuratowski Constraint " + i + "\n");
       result.append(generateKuratowski(jsonConstraints.getJSONObject(i)));