diff --git a/src/src_sharpSAT/Basics.cpp b/src/src_sharpSAT/Basics.cpp
index 3a908f6..a34afa8 100755
--- a/src/src_sharpSAT/Basics.cpp
+++ b/src/src_sharpSAT/Basics.cpp
@@ -21,6 +21,8 @@ unsigned int CSolverConf::secsTimeBound = 100000;
 
 unsigned int CSolverConf::maxCacheSize = 0;
 
+int CSolverConf::relevantVarCount = 0;
+
 int CSolverConf::nodeCount = 0;
 
 
diff --git a/src/src_sharpSAT/Basics.h b/src/src_sharpSAT/Basics.h
index e63cff5..caedce0 100755
--- a/src/src_sharpSAT/Basics.h
+++ b/src/src_sharpSAT/Basics.h
@@ -27,6 +27,8 @@ class CSolverConf
 
     static unsigned int maxCacheSize;   // maximum Cache Size in bytes
     
+    static int relevantVarCount; // Only count the first n variables in model enumeration
+    
     static int nodeCount; // Nodes currently in use
     
     static bool smoothNNF;
diff --git a/src/src_sharpSAT/Basics.h.bdg b/src/src_sharpSAT/Basics.h.bdg
index 13a5bd9..7b56234 100755
--- a/src/src_sharpSAT/Basics.h.bdg
+++ b/src/src_sharpSAT/Basics.h.bdg
@@ -27,6 +27,8 @@ public:
 
     static unsigned int maxCacheSize;   // maximum Cache Size in bytes
     
+    static int relevantVarCount; // Only count the first n variables in model enumeration
+    
     static int nodeCount; // Nodes currently in use
     
     static bool smoothNNF;
diff --git a/src/src_sharpSAT/Basics.h.ddnnf b/src/src_sharpSAT/Basics.h.ddnnf
index e63cff5..caedce0 100755
--- a/src/src_sharpSAT/Basics.h.ddnnf
+++ b/src/src_sharpSAT/Basics.h.ddnnf
@@ -27,6 +27,8 @@ public:
 
     static unsigned int maxCacheSize;   // maximum Cache Size in bytes
     
+    static int relevantVarCount; // Only count the first n variables in model enumeration
+    
     static int nodeCount; // Nodes currently in use
     
     static bool smoothNNF;
diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h
index 1b2fd09..eb1c67f 100644
--- a/src/src_sharpSAT/MainSolver/MainSolver.h
+++ b/src/src_sharpSAT/MainSolver/MainSolver.h
@@ -438,6 +438,11 @@ class CMainSolver: public CInstanceGraph
 		}
 	}
 	
+	int originalVariable(int var)
+	{
+	    return getOrigTranslation()[getVarTranslation()[var]];
+	}
+	
 	void translateLiterals(const vector<int> varTranslation) {
 		for (int i = 0; i < litNodes.size(); i++) {
 			if (litNodes[i]->getVal() < 0)
diff --git a/src/src_sharpSAT/main.cpp b/src/src_sharpSAT/main.cpp
index 464daad..94f3d31 100644
--- a/src/src_sharpSAT/main.cpp
+++ b/src/src_sharpSAT/main.cpp
@@ -117,6 +117,7 @@ int main(int argc, char *argv[])
 		cout << "\t -FrA [file] \t\t file to output the run statistics" << endl;
 		cout << "\t -Fgraph [file] \t file to output the backdoor or d-DNNF graph" << endl;
 		cout << "\t -Fnnf [file] \t\t file to output the nnf graph to" << endl;
+		cout << "\t -varcount [n]\t\t only count models projected to the first n variables" << endl;
 
         //Dimitar Shterionov:
         cout << "\t -smoothNNF \t\t post processing to smoothed d-DNNF" << endl;
@@ -209,6 +210,15 @@ int main(int argc, char *argv[])
 			CSolverConf::maxCacheSize = atoi(argv[i + 1]) * 1024 * 1024;
 			//cout <<"maxCacheSize:" <<CSolverConf::maxCacheSize<<"bytes\n";
 		}
+		else if (strcmp(argv[i], "-varcount") == 0)
+		{
+		    if (argc <= i + 1)
+		    {
+				toSTDOUT("wrong parameters"<<endl);
+				return -1;
+			}
+			CSolverConf::relevantVarCount = atoi(argv[i + 1]);
+		}
 		else
 			s = argv[i];
 	}