--- solvers/glucose30/core/Solver.h
+++ solvers/glucose30/core/Solver.h
@@ -29,6 +29,9 @@
 #ifndef Glucose30_Solver_h
 #define Glucose30_Solver_h
 
+#include <vector>
+#include <atomic>
+#include <unordered_map>
 #include "glucose30/mtl/Vec.h"
 #include "glucose30/mtl/Heap.h"
 #include "glucose30/mtl/Alg.h"
@@ -182,7 +185,22 @@
     uint64_t nbRemovedClauses,nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 
+public:
+    bool gctsGeometric=false, gctsSymmetry=false;
+    uint64_t geometricOrbitPatterns=0;
+    uint64_t geometricChecks=0, geometricUnits=0, geometricConflicts=0, geometricTouches=0;
 protected:
+    struct AnchorSection {CRef reason;std::vector<int> roles;int zeros=0;bool active=true,queued=false;};
+    std::vector<AnchorSection> anchorSections;
+    std::vector<std::vector<int>> anchorIncidence;
+    std::unordered_map<CRef,int> anchorByReason;
+    std::vector<int> anchorQueue;size_t anchorHead=0;
+    void anchorAttach(CRef);
+    void anchorOrbit(const vec<Lit>&, unsigned int);
+    void anchorDetach(CRef);
+    void anchorChange(int,int);
+    CRef anchorPropagate();
+    void anchorRelocate(ClauseAllocator&);
     long curRestart;
     // Helper structures:
     //
@@ -276,7 +294,7 @@
     //
     int64_t             conflict_budget;    // -1 means no budget.
     int64_t             propagation_budget; // -1 means no budget.
-    bool                asynch_interrupt;
+    std::atomic<bool>   asynch_interrupt;
 
 
     // Variables added for incremental mode
--- solvers/glucose30/core/Solver.cc
+++ solvers/glucose30/core/Solver.cc
@@ -35,6 +35,13 @@
 #include "glucose30/utils/System.h"
 
 extern void gcts_trace(int, int, int);
+extern void gcts_learn(const Glucose30::vec<Glucose30::Lit>&);
+extern int gcts_anchor_candidate(int);
+extern int gcts_symmetry_candidate(int,int);
+extern void gcts_orbit_record(const Glucose30::vec<Glucose30::Lit>&);
+#include <vector>
+#include <set>
+#include <algorithm>
 using namespace Glucose30;
 #pragma GCC diagnostic ignored "-Wsign-compare"
 
@@ -273,6 +280,7 @@
 
 void Solver::attachClause(CRef cr) {
     const Clause& c = ca[cr];
+    if(gctsGeometric&&c.learnt()){anchorAttach(cr);learnts_literals+=c.size();return;}
 
     assert(c.size() > 1);
     if(c.size()==2) {
@@ -290,6 +298,7 @@
 
 void Solver::detachClause(CRef cr, bool strict) {
     const Clause& c = ca[cr];
+    if(gctsGeometric&&c.learnt()){anchorDetach(cr);learnts_literals-=c.size();return;}
 
     assert(c.size() > 1);
     if(c.size()==2) {
@@ -319,7 +328,7 @@
 
   Clause& c = ca[cr];
 
-  if (certifiedUNSAT) {
+  if (certifiedUNSAT && !gctsSymmetry) {
     fprintf(certifiedOutput, "d ");
     for (int i = 0; i < c.size(); i++)
       fprintf(certifiedOutput, "%i ", var(c[i]) * (-2 * sign(c[i]) + 1));
@@ -458,6 +467,7 @@
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             if (x > 0 && x <= 8140 && !sign(trail[c])) gcts_trace(2, x, level);
+            if(gctsGeometric&&!sign(trail[c]))anchorChange(x,-1);
             assigns [x] = g3l_Undef;
 	    if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
                 polarity[x] = sign(trail[c]);
@@ -492,7 +502,7 @@
         }else
             next = order_heap.removeMin();
 
-    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
+    return next == var_Undef ? lit_Undef : mkLit(next, false);
 }
 
 
@@ -515,176 +525,29 @@
 |________________________________________________________________________________________________@*/
 void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors)
 {
-    int pathC = 0;
-    Lit p     = lit_Undef;
-
-    // Generate conflict clause:
-    //
-    out_learnt.push();      // (leave room for the asserting literal)
-    int index   = trail.size() - 1;
-
-    do{
-        assert(confl != CRef_Undef); // (otherwise should be UIP)
-        Clause& c = ca[confl];
-
-	// Special case for binary clauses
-	// The first one has to be SAT
-	if( p != lit_Undef && c.size()==2 && value(c[0])==g3l_False) {
-
-	  assert(value(c[1])==g3l_True);
-	  Lit tmp = c[0];
-	  c[0] =  c[1], c[1] = tmp;
-	}
-
-	if (c.learnt())
-            claBumpActivity(c);
-
-#ifdef DYNAMICNBLEVEL
-	// DYNAMIC NBLEVEL trick (see competition'09 companion paper)
-	if(c.learnt()  && c.lbd()>2) {
-	  unsigned int nblevels = computeLBD(c);
-	  if(nblevels+1<c.lbd() ) { // improve the LBD
-	    if(c.lbd()<=lbLBDFrozenClause) {
-	      c.setCanBeDel(false);
-	    }
-	    // seems to be interesting : keep it for the next round
-	    c.setLBD(nblevels); // Update it
-	  }
-	}
-#endif
-
-
-        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
-            Lit q = c[j];
-
-            if (!seen[var(q)] && level(var(q)) > 0){
-	      if(!isSelector(var(q)))
-                varBumpActivity(var(q));
-	      seen[var(q)] = 1;
-	      if (level(var(q)) >= decisionLevel()) {
-		pathC++;
-#ifdef UPDATEVARACTIVITY
-		// UPDATEVARACTIVITY trick (see competition'09 companion paper)
-		if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)  && ca[reason(var(q))].learnt())
-		  lastDecisionLevel.push(q);
-#endif
-
-	      } else {
-		if(isSelector(var(q))) {
-		  assert(value(q) == g3l_False);
-		  selectors.push(q);
-		} else
-		  out_learnt.push(q);
-	      }
-	    }
-        }
-
-        // Select next clause to look at:
-        while (!seen[var(trail[index--])]);
-        p     = trail[index+1];
-        confl = reason(var(p));
-        seen[var(p)] = 0;
-        pathC--;
-
-    }while (pathC > 0);
-    out_learnt[0] = ~p;
-
-    // Simplify conflict clause:
-    //
-    int i, j;
-
-    for(int i = 0;i<selectors.size();i++)
-      out_learnt.push(selectors[i]);
-
-    out_learnt.copyTo(analyze_toclear);
-    if (ccmin_mode == 2){
-        uint32_t abstract_level = 0;
-        for (i = 1; i < out_learnt.size(); i++)
-            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
-
-        for (i = j = 1; i < out_learnt.size(); i++)
-            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
-                out_learnt[j++] = out_learnt[i];
-
-    }else if (ccmin_mode == 1){
-        for (i = j = 1; i < out_learnt.size(); i++){
-            Var x = var(out_learnt[i]);
-
-            if (reason(x) == CRef_Undef)
-                out_learnt[j++] = out_learnt[i];
-            else{
-                Clause& c = ca[reason(var(out_learnt[i]))];
-                // Thanks to Siert Wieringa for this bug fix!
-                for (int k = ((c.size()==2) ? 0:1); k < c.size(); k++)
-                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
-                        out_learnt[j++] = out_learnt[i];
-                        break; }
-            }
-        }
-    }else
-        i = j = out_learnt.size();
-
-    max_literals += out_learnt.size();
-    out_learnt.shrink(i - j);
-    tot_literals += out_learnt.size();
-
-
-    /* ***************************************
-      Minimisation with binary clauses of the asserting clause
-      First of all : we look for small clauses
-      Then, we reduce clauses with small LBD.
-      Otherwise, this can be useless
-     */
-    if(!incremental && out_learnt.size()<=lbSizeMinimizingClause) {
-      minimisationWithBinaryResolution(out_learnt);
-    }
-    // Find correct backtrack level:
-    //
-    if (out_learnt.size() == 1)
-        out_btlevel = 0;
-    else{
-        int max_i = 1;
-        // Find the first literal assigned at the next-highest level:
-        for (int i = 2; i < out_learnt.size(); i++)
-            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
-                max_i = i;
-        // Swap-in this literal at index 1:
-        Lit p             = out_learnt[max_i];
-        out_learnt[max_i] = out_learnt[1];
-        out_learnt[1]     = p;
-        out_btlevel       = level(var(p));
-    }
-
-
-    // Compute the size of the clause without selectors (incremental mode)
-    if(incremental) {
-      szWithoutSelectors = 0;
-      for(int i=0;i<out_learnt.size();i++) {
-	if(!isSelector(var((out_learnt[i])))) szWithoutSelectors++;
-	else if(i>0) break;
+    std::vector<char> cut(nVars(),0);
+    int current=0;
+    auto add=[&](Lit q){Var v=var(q);if(level(v)==0)return;if(!cut[v]){cut[v]=sign(q)?-1:1;if(level(v)==decisionLevel())current++;varBumpActivity(v);}else if(cut[v]!=(sign(q)?-1:1))std::abort();};
+    for(int j=0;j<ca[confl].size();j++)add(ca[confl][j]);
+    // Eliminate every false-placement antecedent; decisions select tiles only.
+    // Also resolve until at most one current-level selected tile remains.
+    for(int pos=trail.size()-1;pos>=0;pos--){Var v=var(trail[pos]);if(!cut[v])continue;
+      if(cut[v]>0 || (level(v)==decisionLevel()&&current>1)){
+        CRef r=reason(v);if(r==CRef_Undef)std::abort();
+        if(level(v)==decisionLevel())current--;cut[v]=0;
+        Clause& c=ca[r];if(c.learnt())claBumpActivity(c);
+        for(int j=0;j<c.size();j++)if(var(c[j])!=v)add(c[j]);
       }
-    } else
-      szWithoutSelectors = out_learnt.size();
-
-    // Compute LBD
-    lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size());
-
-
-#ifdef UPDATEVARACTIVITY
-  // UPDATEVARACTIVITY trick (see competition'09 companion paper)
-  if(lastDecisionLevel.size()>0) {
-    for(int i = 0;i<lastDecisionLevel.size();i++) {
-      if(ca[reason(var(lastDecisionLevel[i]))].lbd()<lbd)
-	varBumpActivity(var(lastDecisionLevel[i]));
-    }
-    lastDecisionLevel.clear();
-  }
-#endif
-
-
-
-  for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
-  for(int j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
+    }
+    for(int v=1;v<nVars();v++)if(cut[v]){if(cut[v]>0)std::abort();out_learnt.push(mkLit(v,true));}
+    if(!out_learnt.size())std::abort();
+    int highest=0;for(int j=1;j<out_learnt.size();j++)if(level(var(out_learnt[j]))>level(var(out_learnt[highest])))highest=j;
+    Lit temp=out_learnt[0];out_learnt[0]=out_learnt[highest];out_learnt[highest]=temp;
+    out_btlevel=0;if(out_learnt.size()>1){int second=1;for(int j=2;j<out_learnt.size();j++)if(level(var(out_learnt[j]))>level(var(out_learnt[second])))second=j;temp=out_learnt[1];out_learnt[1]=out_learnt[second];out_learnt[second]=temp;out_btlevel=level(var(out_learnt[1]));}
+    if(out_btlevel>=level(var(out_learnt[0])))std::abort();
+    szWithoutSelectors=out_learnt.size();lbd=computeLBD(out_learnt,out_learnt.size());
+    max_literals+=out_learnt.size();tot_literals+=out_learnt.size();
+    gcts_learn(out_learnt);
 }
 
 
@@ -773,6 +636,7 @@
     assigns[var(p)] = lbool(!sign(p));
     vardata[var(p)] = mkVarData(from, decisionLevel());
     trail.push_(p);
+    if(gctsGeometric&&!sign(p))anchorChange(var(p),1);
     if (var(p) > 0 && var(p) <= 8140 && !sign(p)) gcts_trace(1, var(p), decisionLevel());
 }
 
@@ -846,7 +710,9 @@
     int     num_props = 0;
     watches.cleanAll();
     watchesBin.cleanAll();
-    while (qhead < trail.size()){
+    while (qhead < trail.size() || (gctsGeometric&&anchorHead<anchorQueue.size())){
+        if(confl!=CRef_Undef)break;
+        if(qhead>=trail.size()){confl=anchorPropagate();continue;}
         Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
         vec<Watcher>&  ws  = watches[p];
         Watcher        *i, *j, *end;
@@ -1100,6 +966,7 @@
     starts++;
     gcts_trace(6, starts, decisionLevel());
     for (;;){
+        if(!withinBudget())return g3l_Undef;
         CRef confl = propagate();
         if (confl != CRef_Undef){
             // CONFLICT
@@ -1158,6 +1025,7 @@
                 claBumpActivity(ca[cr]);
                 uncheckedEnqueue(learnt_clause[0], cr);
             }
+            if(gctsSymmetry)anchorOrbit(learnt_clause,nblevels);
             varDecayActivity();
             claDecayActivity();
 
@@ -1623,6 +1491,7 @@
 
 void Solver::relocAll(ClauseAllocator& to)
 {
+    if(gctsGeometric)anchorRelocate(to);
     // All watchers:
     //
     // for (int i = 0; i < watches.size(); i++)
@@ -1673,3 +1542,37 @@
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+void Solver::anchorAttach(CRef cr){
+  if(anchorIncidence.size()<(size_t)nVars())anchorIncidence.resize(nVars());
+  AnchorSection s;s.reason=cr;Clause& c=ca[cr];int index=anchorSections.size();
+  for(int i=0;i<c.size();i++){if(!sign(c[i]))std::abort();int v=gcts_anchor_candidate(var(c[i]));if(v!=var(c[i]))std::abort();s.roles.push_back(v);if(value(v)==g3l_True)s.zeros++;anchorIncidence[v].push_back(index);}
+  if(s.zeros>=(int)s.roles.size()-1){s.queued=true;anchorQueue.push_back(index);}anchorByReason[cr]=index;anchorSections.push_back(std::move(s));
+}
+void Solver::anchorDetach(CRef cr){auto it=anchorByReason.find(cr);if(it==anchorByReason.end())std::abort();auto& s=anchorSections[it->second];s.active=false;std::vector<int>().swap(s.roles);anchorByReason.erase(it);}
+void Solver::anchorChange(int v,int delta){
+  if((size_t)v>=anchorIncidence.size())return;
+  for(int index:anchorIncidence[v]){auto& s=anchorSections[index];if(!s.active)continue;geometricTouches++;s.zeros+=delta;if(s.zeros<0||s.zeros>(int)s.roles.size())std::abort();if(s.zeros>=(int)s.roles.size()-1&&!s.queued){s.queued=true;anchorQueue.push_back(index);}}
+}
+CRef Solver::anchorPropagate(){
+  while(anchorHead<anchorQueue.size()){int index=anchorQueue[anchorHead++];auto& s=anchorSections[index];s.queued=false;if(!s.active||s.zeros<(int)s.roles.size()-1)continue;geometricChecks++;
+    int remaining=-1,missing=0;for(int v:s.roles)if(value(v)!=g3l_True){remaining=v;missing++;}
+    if((int)s.roles.size()-missing!=s.zeros)std::abort();
+    if(!missing){geometricConflicts++;return s.reason;}
+    if(missing==1&&value(remaining)==g3l_Undef){Clause& c=ca[s.reason];for(int i=0;i<c.size();i++)if(var(c[i])==remaining){Lit t=c[0];c[0]=c[i];c[i]=t;break;}geometricUnits++;uncheckedEnqueue(mkLit(remaining,true),s.reason);}
+  }
+  anchorQueue.clear();anchorHead=0;return CRef_Undef;
+}
+void Solver::anchorRelocate(ClauseAllocator& to){
+  anchorByReason.clear();for(size_t i=0;i<anchorSections.size();i++)if(anchorSections[i].active){ca.reloc(anchorSections[i].reason,to);anchorByReason[anchorSections[i].reason]=i;}
+  for(auto& list:anchorIncidence){size_t keep=0;for(int i:list)if(anchorSections[i].active)list[keep++]=i;list.resize(keep);}
+}
+
+void Solver::anchorOrbit(const vec<Lit>& source,unsigned int lbd){
+ std::set<std::vector<int>> emitted;std::vector<int> original;for(int i=0;i<source.size();i++)original.push_back(var(source[i]));std::sort(original.begin(),original.end());emitted.insert(original);
+ for(int g=1;g<16;g++){std::vector<int> members;for(int v:original)members.push_back(gcts_symmetry_candidate(v,g));std::sort(members.begin(),members.end());if(!emitted.insert(members).second)continue;
+   vec<Lit> image;for(int v:members)image.push(mkLit(v,true));
+   if(certifiedUNSAT){for(int v:members)fprintf(certifiedOutput,"%d ",-v);fprintf(certifiedOutput,"0\n");}gcts_orbit_record(image);geometricOrbitPatterns++;
+   CRef cr=ca.alloc(image,true);ca[cr].setLBD(lbd);ca[cr].setSizeWithoutSelectors(image.size());learnts.push(cr);anchorAttach(cr);learnts_literals+=image.size();claBumpActivity(ca[cr]);
+ }
+}