Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java	(revision 56)
@@ -0,0 +1,54 @@
+package de.uni_hildesheim.sse.trans.convert;
+
+import java.util.List;
+
+import de.uni_hildesheim.sse.model.varModel.AbstractVariable;
+import de.uni_hildesheim.sse.model.varModel.Constraint;
+import de.uni_hildesheim.sse.model.varModel.Project;
+import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder;
+import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder;
+import de.uni_hildesheim.sse.model.varModel.filter.FilterType;
+import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder.VisibilityType;
+
+/**
+ * Converts a Boolean {@link Project} into CNF form.
+ * @author El-Sharkawy
+ *
+ */
+public class CNFConverter {
+    
+    /**
+     * Converts a Boolean {@link Project} into CNF form.
+     * @param project A Boolean {@link Project} containing only constraints with AND, OR, and NOT operations.
+     * @param converter A Strategy which is able to convert boolean formulas into CNF form.
+     */
+    public static void convert(Project project, ICNFConvertStrategy converter) {
+        // Store complete content of project (imports are not used in this project).
+        DeclarationFinder declfinder = new DeclarationFinder(project, FilterType.ALL, null);
+        ConstraintFinder constFinder = new ConstraintFinder(project);
+        
+        // Clear old content
+        project.clear();
+        
+        // 1. re-add Declarations
+        List<AbstractVariable> declarations = declfinder.getVariableDeclarations(VisibilityType.ALL);
+        for (AbstractVariable declaration : declarations) {
+            project.add(declaration);
+        }
+        
+        // 2. Convert the constraints
+        List<Constraint> constraints = constFinder.getConstraints();
+        for (Constraint constraint : constraints) {
+            DisjunctionChecker checker = new DisjunctionChecker(constraint);
+            if (checker.isDisjunctionTerm()) {
+                project.add(constraint);
+            } else {
+                List<Constraint> cnfConstraints = converter.convert(constraint);
+                for (Constraint cnfConstraint : cnfConstraints) {
+                    project.add(cnfConstraint);
+                }
+            }
+        }
+    }
+    
+}
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/DisjunctionChecker.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/DisjunctionChecker.java	(revision 55)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/DisjunctionChecker.java	(revision 56)
@@ -24,5 +24,5 @@
  * 
  */
-public class DisjunctionChecker implements IConstraintTreeVisitor {
+class DisjunctionChecker implements IConstraintTreeVisitor {
 
     private boolean isDisjunctionTerm;
@@ -35,5 +35,5 @@
      * @see #isDisjunctionTerm()
      */
-    public DisjunctionChecker(Constraint constraint) {
+    DisjunctionChecker(Constraint constraint) {
         isDisjunctionTerm = true;
         constraint.getConsSyntax().accept(this);
@@ -45,5 +45,5 @@
      * <tt>false</tt> otherwise.
      */
-    public boolean isDisjunctionTerm() {
+    boolean isDisjunctionTerm() {
         return isDisjunctionTerm;
     }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java	(revision 56)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ICNFConvertStrategy.java	(revision 56)
@@ -0,0 +1,20 @@
+package de.uni_hildesheim.sse.trans.convert;
+
+import java.util.List;
+
+import de.uni_hildesheim.sse.model.varModel.Constraint;
+
+/**
+ * Strategy for converting a boolean constraint into CNF form.
+ * @author El-Sharkawy
+ *
+ */
+public interface ICNFConvertStrategy {
+
+    /**
+     * Converts boolean formula into a CNF formula, which may consists of multiple disjunction terms.
+     * @param constraint The boolean constraint, which shall be converted.
+     * @return A list of constraints expressing the same formula.
+     */
+    public List<Constraint> convert(Constraint constraint);
+}