diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java
index 7c699fdc..4c6d327f 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCALKCardinalityNetwork implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildALK(result, vars, rhs);
   }
 
@@ -58,7 +59,7 @@ public void build(final CCResult result, final Variable[] vars, int rhs) {
    * @param vars   the variables
    * @param rhs    the right-hand side
    */
-  void buildForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildALKForIncremental(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java
index c94de5f8..6d0ed806 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
@@ -50,7 +51,7 @@ final class CCALKModularTotalizer implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildALK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
index 6f9a4c5b..c323f669 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCALKTotalizer implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildALK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
index 28b22178..b0fe51d1 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCAMKCardinalityNetwork implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildAMK(result, vars, rhs);
   }
 
@@ -63,7 +64,7 @@ public CCIncrementalData incrementalData() {
    * @param vars   the variables
    * @param rhs    the right-hand side
    */
-  void buildForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildAMKForIncremental(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java
index a05f0b02..f5189294 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
@@ -50,7 +51,7 @@ final class CCAMKModularTotalizer implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, Variable[] vars, int rhs) {
     this.totalizer.buildAMK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
index b74d70a7..14eb7a1b 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -49,7 +50,7 @@ final class CCAMKTotalizer implements CCAtMostK {
 
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildAMK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java
index b87f25fa..5384624f 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -62,7 +63,7 @@
  */
 final class CCAMOBimander implements CCAtMostOne {
 
-  private CCResult result;
+  private EncodingResult result;
   private LNGVector<LNGVector<Literal>> groups;
   private LNGVector<Literal> bits;
   private int numberOfBits;
@@ -80,7 +81,7 @@ final class CCAMOBimander implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.encodeIntern(new LNGVector<Literal>(vars));
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java
index b76ebfd4..25b751e7 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java
@@ -51,6 +51,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -70,7 +71,7 @@ final class CCAMOBinary implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     final int numberOfBits = (int) Math.ceil((Math.log(vars.length) / Math.log(2)));
     final int twoPowNBits = (int) Math.pow(2, numberOfBits);
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java
index 080941c8..8ab28ce3 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -62,7 +63,7 @@
  */
 final class CCAMOCommander implements CCAtMostOne {
 
-  private CCResult result;
+  private EncodingResult result;
   private int k;
   private LNGVector<Literal> literals;
   private LNGVector<Literal> nextLiterals;
@@ -80,7 +81,7 @@ final class CCAMOCommander implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.currentLiterals.clear();
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java
index 129ec397..ee8bb00a 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java
@@ -49,6 +49,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -65,7 +66,7 @@ final class CCAMOLadder implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     final Variable[] seqAuxiliary = new Variable[vars.length - 1];
     for (int i = 0; i < vars.length - 1; i++)
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java
index e87893e1..9102b628 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -63,7 +64,7 @@
 final class CCAMONested implements CCAtMostOne {
 
   private int groupSize;
-  private CCResult result;
+  private EncodingResult result;
 
   /**
    * Constructs the nested AMO encoder.
@@ -74,7 +75,7 @@ final class CCAMONested implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.encodeIntern(new LNGVector<Literal>(vars));
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java
index 12b2992d..b9e48ddb 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -37,7 +38,7 @@
  */
 final class CCAMOProduct implements CCAtMostOne {
   private final int recursiveBound;
-  private CCResult result;
+  private EncodingResult result;
 
   /**
    * Constructs the naive AMO encoder.
@@ -47,7 +48,7 @@ final class CCAMOProduct implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.productRec(vars);
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java
index c85382c6..7a1946c9 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -46,7 +47,7 @@ final class CCAMOPure implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     for (int i = 0; i < vars.length; i++)
       for (int j = i + 1; j < vars.length; j++)
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java
index 95713fef..9721336e 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -43,7 +44,7 @@ interface CCAtLeastK {
    * @param rhs    the right hand side {@code k} of the constraint
    * @throws IllegalArgumentException if the right hand side of the cardinality constraint is negative
    */
-  void build(final CCResult result, final Variable[] vars, int rhs);
+  void build(final EncodingResult result, final Variable[] vars, int rhs);
 
   /**
    * Returns the incremental data for the current encoded constraint.
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java
index 5144efeb..c59fd5cb 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -44,7 +45,7 @@ interface CCAtMostK {
    * @param rhs    the right hand side {@code k} of the constraint
    * @throws IllegalArgumentException if the right hand side of the cardinality constraint is negative
    */
-  void build(final CCResult result, final Variable[] vars, int rhs);
+  void build(final EncodingResult result, final Variable[] vars, int rhs);
 
   /**
    * Returns the incremental data for the current encoded constraint.
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java
index 59ec9e14..c4ec4113 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -42,5 +43,5 @@ interface CCAtMostOne {
    * @param result the result for the encoding
    * @param vars   the variables {@code var_1 ... var_n}
    */
-  void build(final CCResult result, final Variable... vars);
+  void build(final EncodingResult result, final Variable... vars);
 }
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java b/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java
index 55e6469d..6198e6a1 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -76,7 +77,7 @@ final class CCCardinalityNetworks {
     this.sorting = new CCSorting();
   }
 
-  void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
@@ -96,7 +97,7 @@ void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
     }
   }
 
-  void buildAMKForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildAMKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
     for (final Variable var : vars)
@@ -107,7 +108,7 @@ void buildAMKForIncremental(final CCResult result, final Variable[] vars, int rh
     this.incData = new CCIncrementalData(result, CCConfig.AMK_ENCODER.CARDINALITY_NETWORK, rhs, output);
   }
 
-  void buildALK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
@@ -128,7 +129,7 @@ void buildALK(final CCResult result, final Variable[] vars, int rhs) {
     }
   }
 
-  void buildALKForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildALKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
     for (final Variable var : vars)
@@ -140,7 +141,7 @@ void buildALKForIncremental(final CCResult result, final Variable[] vars, int rh
     this.incData = new CCIncrementalData(result, CCConfig.ALK_ENCODER.CARDINALITY_NETWORK, rhs, vars.length, output);
   }
 
-  void buildEXK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildEXK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java
index 8c3b642b..816ba777 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCEXKCardinalityNetwork implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildEXK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCEXKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCEXKTotalizer.java
index d57a278b..7a5bbedb 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCEXKTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCEXKTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -49,7 +50,7 @@ final class CCEXKTotalizer implements CCExactlyK {
 
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildEXK(result, vars, rhs);
   }
 
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java b/src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java
index 1ee61109..9d9e00ba 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java
@@ -31,6 +31,7 @@
 import org.logicng.collections.ImmutableFormulaList;
 import org.logicng.configurations.Configuration;
 import org.logicng.configurations.ConfigurationType;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
@@ -107,7 +108,7 @@ public CCEncoder(final FormulaFactory f) {
    * @return the CNF encoding of the cardinality constraint
    */
   public ImmutableFormulaList encode(final PBConstraint cc) {
-    final CCResult result = CCResult.resultForFormula(f);
+    final EncodingResult result = EncodingResult.resultForFormula(f);
     this.encodeConstraint(cc, result);
     return new ImmutableFormulaList(FType.AND, result.result());
   }
@@ -117,7 +118,7 @@ public ImmutableFormulaList encode(final PBConstraint cc) {
    * @param cc     the cardinality constraint
    * @param result the result of the encoding
    */
-  public void encode(final PBConstraint cc, final CCResult result) {
+  public void encode(final PBConstraint cc, final EncodingResult result) {
     this.encodeConstraint(cc, result);
   }
 
@@ -127,7 +128,7 @@ public void encode(final PBConstraint cc, final CCResult result) {
    * @return the encoding of the constraint and the incremental data
    */
   public Pair<ImmutableFormulaList, CCIncrementalData> encodeIncremental(final PBConstraint cc) {
-    final CCResult result = CCResult.resultForFormula(f);
+    final EncodingResult result = EncodingResult.resultForFormula(f);
     final CCIncrementalData incData = this.encodeIncremental(cc, result);
     return new Pair<>(new ImmutableFormulaList(FType.AND, result.result()), incData);
   }
@@ -138,11 +139,11 @@ public Pair<ImmutableFormulaList, CCIncrementalData> encodeIncremental(final PBC
    * @param result the result of the encoding
    * @return the incremental data
    */
-  public CCIncrementalData encodeIncremental(final PBConstraint cc, final CCResult result) {
+  public CCIncrementalData encodeIncremental(final PBConstraint cc, final EncodingResult result) {
     return this.encodeIncrementalConstraint(cc, result);
   }
 
-  private CCIncrementalData encodeIncrementalConstraint(final PBConstraint cc, final CCResult result) {
+  private CCIncrementalData encodeIncrementalConstraint(final PBConstraint cc, final EncodingResult result) {
     if (!cc.isCC())
       throw new IllegalArgumentException("Cannot encode a non-cardinality constraint with a cardinality constraint encoder.");
     final Variable[] ops = litsAsVars(cc.operands());
@@ -184,7 +185,7 @@ public CCConfig config() {
    * @param cc     the constraint
    * @param result the result
    */
-  private void encodeConstraint(final PBConstraint cc, final CCResult result) {
+  private void encodeConstraint(final PBConstraint cc, final EncodingResult result) {
     if (!cc.isCC())
       throw new IllegalArgumentException("Cannot encode a non-cardinality constraint with a cardinality constraint encoder.");
     final Variable[] ops = litsAsVars(cc.operands());
@@ -224,7 +225,7 @@ private void encodeConstraint(final PBConstraint cc, final CCResult result) {
    * @param vars   the variables of the constraint
    * @return the CNF encoding of the constraint
    */
-  private List<Formula> amo(final CCResult result, final Variable... vars) {
+  private List<Formula> amo(final EncodingResult result, final Variable... vars) {
     if (vars.length <= 1)
       return new ArrayList<>();
     switch (this.config().amoEncoder) {
@@ -291,7 +292,7 @@ private List<Formula> amo(final CCResult result, final Variable... vars) {
    * @param result the result
    * @param vars   the variables of the constraint
    */
-  private void exo(final CCResult result, final Variable... vars) {
+  private void exo(final EncodingResult result, final Variable... vars) {
     if (vars.length == 0)
       return;
     if (vars.length == 1) {
@@ -308,7 +309,7 @@ private void exo(final CCResult result, final Variable... vars) {
    * @param vars   the variables of the constraint
    * @param rhs    the right hand side of the constraint
    */
-  private void amk(final CCResult result, final Variable[] vars, int rhs) {
+  private void amk(final EncodingResult result, final Variable[] vars, int rhs) {
     if (rhs < 0)
       throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
     if (rhs >= vars.length) // there is no constraint
@@ -349,7 +350,7 @@ private void amk(final CCResult result, final Variable[] vars, int rhs) {
    * @param rhs    the right hand side of the constraint
    * @return the incremental data
    */
-  private CCIncrementalData amkIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  private CCIncrementalData amkIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     if (rhs < 0)
       throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
     if (rhs >= vars.length) // there is no constraint
@@ -389,7 +390,7 @@ private CCIncrementalData amkIncremental(final CCResult result, final Variable[]
    * @param vars   the variables of the constraint
    * @param rhs    the right hand side of the constraint
    */
-  private void alk(final CCResult result, final Variable[] vars, int rhs) {
+  private void alk(final EncodingResult result, final Variable[] vars, int rhs) {
     if (rhs < 0)
       throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
     if (rhs > vars.length) {
@@ -438,7 +439,7 @@ private void alk(final CCResult result, final Variable[] vars, int rhs) {
    * @param rhs    the right hand side of the constraint
    * @return the incremental data
    */
-  private CCIncrementalData alkIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  private CCIncrementalData alkIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     if (rhs < 0)
       throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
     if (rhs > vars.length) {
@@ -486,7 +487,7 @@ private CCIncrementalData alkIncremental(final CCResult result, final Variable[]
    * @param vars   the variables of the constraint
    * @param rhs    the right hand side of the constraint
    */
-  private void exk(final CCResult result, final Variable[] vars, int rhs) {
+  private void exk(final EncodingResult result, final Variable[] vars, int rhs) {
     if (rhs < 0)
       throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
     if (rhs > vars.length) {
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCExactlyK.java b/src/main/java/org/logicng/cardinalityconstraints/CCExactlyK.java
index df50ff71..5c8a92c6 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCExactlyK.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCExactlyK.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -43,7 +44,7 @@ interface CCExactlyK {
    * @param rhs    the right hand side {@code k} of the constraint
    * @throws IllegalArgumentException if the right hand side of the cardinality constraint is negative
    */
-  void build(final CCResult result, final Variable[] vars, int rhs);
+  void build(final EncodingResult result, final Variable[] vars, int rhs);
 
   /**
    * Returns the incremental data for the current encoded constraint.
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java b/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java
index 06ebef25..3e17c7a8 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.Literal;
 
@@ -65,7 +66,7 @@
  * @since 1.1
  */
 public final class CCIncrementalData {
-  private final CCResult result;
+  private final EncodingResult result;
   private final CCConfig.AMK_ENCODER amkEncoder;
   private final CCConfig.ALK_ENCODER alkEncoder;
   private final LNGVector<? extends Literal> vector1;
@@ -83,7 +84,7 @@ public final class CCIncrementalData {
    * @param vector2    the second internal vector
    * @param mod        the modulo value
    */
-  CCIncrementalData(final CCResult result, CCConfig.AMK_ENCODER amkEncoder, int rhs,
+  CCIncrementalData(final EncodingResult result, CCConfig.AMK_ENCODER amkEncoder, int rhs,
                     final LNGVector<? extends Literal> vector1, final LNGVector<? extends Literal> vector2, int mod) {
     this.result = result;
     this.amkEncoder = amkEncoder;
@@ -102,7 +103,7 @@ public final class CCIncrementalData {
    * @param rhs     the current right-hand-side
    * @param vector1 the first internal vector
    */
-  CCIncrementalData(final CCResult result, CCConfig.AMK_ENCODER encoder, int rhs, final LNGVector<? extends Literal> vector1) {
+  CCIncrementalData(final EncodingResult result, CCConfig.AMK_ENCODER encoder, int rhs, final LNGVector<? extends Literal> vector1) {
     this(result, encoder, rhs, vector1, null, -1);
   }
 
@@ -116,7 +117,7 @@ public final class CCIncrementalData {
    * @param vector2    the second internal vector
    * @param mod        the modulo value
    */
-  CCIncrementalData(final CCResult result, CCConfig.ALK_ENCODER alkEncoder, int rhs, int nVars,
+  CCIncrementalData(final EncodingResult result, CCConfig.ALK_ENCODER alkEncoder, int rhs, int nVars,
                     final LNGVector<? extends Literal> vector1, final LNGVector<? extends Literal> vector2, int mod) {
     this.result = result;
     this.alkEncoder = alkEncoder;
@@ -137,7 +138,7 @@ public final class CCIncrementalData {
    * @param nVars      the number of variables
    * @param vector1    the first internal vector
    */
-  CCIncrementalData(final CCResult result, CCConfig.ALK_ENCODER alkEncoder, int rhs, int nVars, final LNGVector<? extends Literal> vector1) {
+  CCIncrementalData(final EncodingResult result, CCConfig.ALK_ENCODER alkEncoder, int rhs, int nVars, final LNGVector<? extends Literal> vector1) {
     this(result, alkEncoder, rhs, nVars, vector1, null, -1);
   }
 
@@ -160,7 +161,7 @@ public void newUpperBoundForSolver(int rhs) {
     computeUBConstraint(result, rhs);
   }
 
-  private void computeUBConstraint(final CCResult result, int rhs) {
+  private void computeUBConstraint(final EncodingResult result, int rhs) {
     if (rhs >= this.currentRHS)
       throw new IllegalArgumentException("New upper bound " + rhs + " + does not tighten the current bound of " + this.currentRHS);
     this.currentRHS = rhs;
@@ -219,7 +220,7 @@ public void newLowerBoundForSolver(int rhs) {
     computeLBConstraint(result, rhs);
   }
 
-  private void computeLBConstraint(final CCResult result, int rhs) {
+  private void computeLBConstraint(final EncodingResult result, int rhs) {
     if (rhs <= this.currentRHS)
       throw new IllegalArgumentException("New lower bound " + rhs + " + does not tighten the current bound of " + this.currentRHS);
     this.currentRHS = rhs;
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java
index 0ec1bbb3..009ff618 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCModularTotalizer.java
@@ -50,6 +50,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
@@ -69,7 +70,7 @@ final class CCModularTotalizer {
   private LNGVector<Literal> cardinalityUpOutvars;
   private LNGVector<Literal> cardinalityLwOutvars;
   private int currentCardinalityRhs;
-  private CCResult result;
+  private EncodingResult result;
   private CCIncrementalData incData;
 
   /**
@@ -83,7 +84,13 @@ final class CCModularTotalizer {
     this.inlits = new LNGVector<>();
   }
 
-  void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
+  /**
+   * Builds an at-most-k constraint.
+   * @param result the result of the encoding
+   * @param vars the variables of the constraint
+   * @param rhs the right hand side of the constraint
+   */
+  void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
     int mod = this.initialize(result, rhs, vars.length);
     for (final Variable var : vars)
       this.inlits.push(var);
@@ -95,7 +102,13 @@ void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
             this.cardinalityLwOutvars, mod);
   }
 
-  void buildALK(final CCResult result, final Variable[] vars, int rhs) {
+  /**
+   * Builds an at-least-k constraint.
+   * @param result the result of the encoding
+   * @param vars the variables of the constraint
+   * @param rhs the right hand side of the constraint
+   */
+  void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
     int newRHS = vars.length - rhs;
     int mod = this.initialize(result, newRHS, vars.length);
     for (final Variable var : vars)
@@ -108,11 +121,15 @@ void buildALK(final CCResult result, final Variable[] vars, int rhs) {
             this.cardinalityUpOutvars, this.cardinalityLwOutvars, mod);
   }
 
+  /**
+   * Returns the incremental data of this encoding.
+   * @return the incremental data of this encoding
+   */
   CCIncrementalData incrementalData() {
     return this.incData;
   }
 
-  private int initialize(final CCResult result, int rhs, int n) {
+  private int initialize(final EncodingResult result, int rhs, int n) {
     result.reset();
     this.result = result;
     this.cardinalityUpOutvars = new LNGVector<>();
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCSorting.java b/src/main/java/org/logicng/cardinalityconstraints/CCSorting.java
index 0aa2f54e..9fe46dbe 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCSorting.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCSorting.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -77,7 +78,15 @@ public CCSorting() {
     this.auxVars = new LNGVector<>();
   }
 
-  public void sort(int m, final LNGVector<Literal> input, final CCResult result, final LNGVector<Literal> output,
+  /**
+   * Generates a sorter encoding for the given input.
+   * @param m         the the counter
+   * @param input     the input literals
+   * @param result    the result of the encoding
+   * @param output    the output literals
+   * @param direction the sorting direction
+   */
+  public void sort(int m, final LNGVector<Literal> input, final EncodingResult result, final LNGVector<Literal> output,
                    final ImplicationDirection direction) {
     assert (m >= 0);
     if (m == 0) {
@@ -124,7 +133,7 @@ public void sort(int m, final LNGVector<Literal> input, final CCResult result, f
       directSorter(m, input, result, output, direction);
   }
 
-  private void comparator(final Literal x1, final Literal x2, final Literal y, final CCResult result,
+  private void comparator(final Literal x1, final Literal x2, final Literal y, final EncodingResult result,
                           final ImplicationDirection direction) {
     assert (!x1.equals(x2));
     if (direction == INPUT_TO_OUTPUT || direction == BOTH) {
@@ -135,7 +144,7 @@ private void comparator(final Literal x1, final Literal x2, final Literal y, fin
       result.addClause(y.negate(), x1, x2);
   }
 
-  private void comparator(final Literal x1, final Literal x2, final Literal y1, final Literal y2, final CCResult result,
+  private void comparator(final Literal x1, final Literal x2, final Literal y1, final Literal y2, final EncodingResult result,
                           final ImplicationDirection direction) {
     assert (!x1.equals(x2));
     assert (!y1.equals(y2));
@@ -151,7 +160,7 @@ private void comparator(final Literal x1, final Literal x2, final Literal y1, fi
     }
   }
 
-  private void recursiveSorter(int m, int l, final LNGVector<Literal> input, final CCResult result,
+  private void recursiveSorter(int m, int l, final LNGVector<Literal> input, final EncodingResult result,
                                final LNGVector<Literal> output, final ImplicationDirection direction) {
     int n = input.size();
     assert (output.size() == 0);
@@ -178,7 +187,7 @@ private void recursiveSorter(int m, int l, final LNGVector<Literal> input, final
     assert (output.size() == m);
   }
 
-  private void recursiveSorter(int m, final LNGVector<Literal> input, final CCResult result,
+  private void recursiveSorter(int m, final LNGVector<Literal> input, final EncodingResult result,
                                final LNGVector<Literal> output, final ImplicationDirection direction) {
     assert (m > 0);
     assert (input.size() > 0);
@@ -189,7 +198,7 @@ private void recursiveSorter(int m, final LNGVector<Literal> input, final CCResu
     this.recursiveSorter(m, l, input, result, output, direction);
   }
 
-  private void counterSorter(int k, final LNGVector<Literal> x, final CCResult formula,
+  private void counterSorter(int k, final LNGVector<Literal> x, final EncodingResult formula,
                              final LNGVector<Literal> output, final ImplicationDirection direction) {
     int n = x.size();
     auxVars.clear();
@@ -219,7 +228,7 @@ private void counterSorter(int k, final LNGVector<Literal> x, final CCResult for
       output.push(auxVars.get(n - 1).get(i));
   }
 
-  private void directSorter(int m, final LNGVector<Literal> input, final CCResult formula,
+  private void directSorter(int m, final LNGVector<Literal> input, final EncodingResult formula,
                             final LNGVector<Literal> output, final ImplicationDirection direction) {
     assert (direction == INPUT_TO_OUTPUT);
     int n = input.size();
@@ -248,7 +257,7 @@ private void directSorter(int m, final LNGVector<Literal> input, final CCResult
     }
   }
 
-  public void merge(int m, final LNGVector<Literal> inputA, final LNGVector<Literal> inputB, final CCResult formula,
+  public void merge(int m, final LNGVector<Literal> inputA, final LNGVector<Literal> inputB, final EncodingResult formula,
                     final LNGVector<Literal> output, final ImplicationDirection direction) {
     assert (m >= 0);
     if (m == 0) {
@@ -275,7 +284,7 @@ public void merge(int m, final LNGVector<Literal> inputA, final LNGVector<Litera
   }
 
   private void recursiveMerger(int c, final LNGVector<Literal> inputA, int a, final LNGVector<Literal> inputB, int b,
-                               final CCResult formula, final LNGVector<Literal> output,
+                               final EncodingResult formula, final LNGVector<Literal> output,
                                final ImplicationDirection direction) {
     assert (inputA.size() > 0);
     assert (inputB.size() > 0);
@@ -358,7 +367,7 @@ else if (i >= oddMerge.size()) {
     assert (output.size() == a + b || output.size() == c);
   }
 
-  private void directMerger(int m, final LNGVector<Literal> inputA, LNGVector<Literal> inputB, final CCResult formula,
+  private void directMerger(int m, final LNGVector<Literal> inputA, LNGVector<Literal> inputB, final EncodingResult formula,
                             LNGVector<Literal> output, final ImplicationDirection direction) {
     assert (direction == INPUT_TO_OUTPUT);
     int a = inputA.size();
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCTotalizer.java
index 694417a0..a74f7203 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCTotalizer.java
+++ b/src/main/java/org/logicng/cardinalityconstraints/CCTotalizer.java
@@ -50,6 +50,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -62,7 +63,7 @@ final class CCTotalizer {
   private enum Bound {LOWER, UPPER, BOTH}
 
   private LNGVector<Variable> cardinalityInvars;
-  private CCResult result;
+  private EncodingResult result;
   private CCIncrementalData incData;
 
   /**
@@ -79,7 +80,7 @@ private enum Bound {LOWER, UPPER, BOTH}
    * @param rhs    the right-hand side
    * @throws IllegalArgumentException if the right hand side of the constraint was negative
    */
-  void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Variable> cardinalityOutvars = this.initializeConstraint(result, vars);
     this.incData = new CCIncrementalData(result, CCConfig.AMK_ENCODER.TOTALIZER, rhs, cardinalityOutvars);
     this.toCNF(cardinalityOutvars, rhs, Bound.UPPER);
@@ -95,7 +96,7 @@ void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
    * @param rhs    the right-hand side
    * @throws IllegalArgumentException if the right hand side of the constraint was negative
    */
-  void buildALK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Variable> cardinalityOutvars = this.initializeConstraint(result, vars);
     this.incData = new CCIncrementalData(result, CCConfig.ALK_ENCODER.TOTALIZER, rhs, vars.length, cardinalityOutvars);
     this.toCNF(cardinalityOutvars, rhs, Bound.LOWER);
@@ -110,7 +111,7 @@ void buildALK(final CCResult result, final Variable[] vars, int rhs) {
    * @param rhs  the right-hand side
    * @throws IllegalArgumentException if the right hand side of the constraint was negative
    */
-  void buildEXK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildEXK(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Variable> cardinalityOutvars = this.initializeConstraint(result, vars);
     this.toCNF(cardinalityOutvars, rhs, Bound.BOTH);
     assert this.cardinalityInvars.size() == 0;
@@ -125,7 +126,7 @@ void buildEXK(final CCResult result, final Variable[] vars, int rhs) {
    * @param vars the variables
    * @return the auxiliary variables
    */
-  private LNGVector<Variable> initializeConstraint(final CCResult result, final Variable[] vars) {
+  private LNGVector<Variable> initializeConstraint(final EncodingResult result, final Variable[] vars) {
     result.reset();
     this.result = result;
     this.cardinalityInvars = new LNGVector<>(vars.length);
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAuxiliaryVariable.java b/src/main/java/org/logicng/datastructures/EncodingAuxiliaryVariable.java
similarity index 90%
rename from src/main/java/org/logicng/cardinalityconstraints/CCAuxiliaryVariable.java
rename to src/main/java/org/logicng/datastructures/EncodingAuxiliaryVariable.java
index 134cab94..df6a1823 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCAuxiliaryVariable.java
+++ b/src/main/java/org/logicng/datastructures/EncodingAuxiliaryVariable.java
@@ -26,18 +26,18 @@
 //                                                                       //
 ///////////////////////////////////////////////////////////////////////////
 
-package org.logicng.cardinalityconstraints;
+package org.logicng.datastructures;
 
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
 /**
- * An auxiliary variable for cardinality constraints.
+ * An auxiliary variable for encoding results.
  * <p></p>
  * This variable is used, if the result is added directly to a solver.  In this case no variable on the factory has
  * to be created.
  */
-final class CCAuxiliaryVariable extends Variable {
+final class EncodingAuxiliaryVariable extends Variable {
 
   final boolean negated;
 
@@ -46,7 +46,7 @@ final class CCAuxiliaryVariable extends Variable {
    * @param name    the literal name
    * @param negated {@code true} if the variables is negated, {@code false} otherwise
    */
-  CCAuxiliaryVariable(String name, boolean negated) {
+  EncodingAuxiliaryVariable(String name, boolean negated) {
     super(name, null);
     this.negated = negated;
   }
@@ -54,7 +54,7 @@ final class CCAuxiliaryVariable extends Variable {
 
   @Override
   public Literal negate() {
-    return new CCAuxiliaryVariable(this.name(), !this.negated);
+    return new EncodingAuxiliaryVariable(this.name(), !this.negated);
   }
 
   @Override
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCResult.java b/src/main/java/org/logicng/datastructures/EncodingResult.java
similarity index 75%
rename from src/main/java/org/logicng/cardinalityconstraints/CCResult.java
rename to src/main/java/org/logicng/datastructures/EncodingResult.java
index f2108d75..fdabe8e7 100644
--- a/src/main/java/org/logicng/cardinalityconstraints/CCResult.java
+++ b/src/main/java/org/logicng/datastructures/EncodingResult.java
@@ -26,7 +26,7 @@
 //                                                                       //
 ///////////////////////////////////////////////////////////////////////////
 
-package org.logicng.cardinalityconstraints;
+package org.logicng.datastructures;
 
 import org.logicng.collections.LNGIntVector;
 import org.logicng.collections.LNGVector;
@@ -41,11 +41,17 @@
 import java.util.List;
 
 /**
- * The result of a cardinality constraint encoding.
+ * The result of an encoding.
+ * <p></p>
+ * Encodings (normal forms, cardinality constraints, pseudo-Boolean constraint) are often used only when adding
+ * formulas to the SAT solver.  Therefore it is not necessary to generate all the formulas required for the encoding
+ * in the formula factory and therefore polluting the factory and the heap.  This class can be used to connect an
+ * encoding directly with a SAT solver and therefore introducing the variables only on the solver - not in the factory.
+ * When working with many encodings, this can be a large performance gain.
  * @version 1.1
  * @since 1.1
  */
-public final class CCResult {
+public final class EncodingResult {
   final FormulaFactory f;
   private List<Formula> result;
   private final MiniSat miniSat;
@@ -57,7 +63,7 @@ public final class CCResult {
    * @param miniSat    the MiniSat instance
    * @param cleaneLing the CleaneLing instance
    */
-  private CCResult(final FormulaFactory f, final MiniSat miniSat, final CleaneLing cleaneLing) {
+  private EncodingResult(final FormulaFactory f, final MiniSat miniSat, final CleaneLing cleaneLing) {
     this.f = f;
     this.miniSat = miniSat;
     this.cleaneLing = cleaneLing;
@@ -69,8 +75,8 @@ private CCResult(final FormulaFactory f, final MiniSat miniSat, final CleaneLing
    * @param f the formula factory
    * @return the result
    */
-  public static CCResult resultForFormula(final FormulaFactory f) {
-    return new CCResult(f, null, null);
+  public static EncodingResult resultForFormula(final FormulaFactory f) {
+    return new EncodingResult(f, null, null);
   }
 
   /**
@@ -79,8 +85,8 @@ public static CCResult resultForFormula(final FormulaFactory f) {
    * @param miniSat the solver
    * @return the result
    */
-  public static CCResult resultForMiniSat(final FormulaFactory f, final MiniSat miniSat) {
-    return new CCResult(f, miniSat, null);
+  public static EncodingResult resultForMiniSat(final FormulaFactory f, final MiniSat miniSat) {
+    return new EncodingResult(f, miniSat, null);
   }
 
   /**
@@ -89,15 +95,15 @@ public static CCResult resultForMiniSat(final FormulaFactory f, final MiniSat mi
    * @param cleaneLing the CleaneLing solver
    * @return the result
    */
-  public static CCResult resultForCleaneLing(final FormulaFactory f, final CleaneLing cleaneLing) {
-    return new CCResult(f, null, cleaneLing);
+  public static EncodingResult resultForCleaneLing(final FormulaFactory f, final CleaneLing cleaneLing) {
+    return new EncodingResult(f, null, cleaneLing);
   }
 
   /**
    * Adds a clause to the result
    * @param literals the literals of the clause
    */
-  void addClause(final Literal... literals) {
+  public void addClause(final Literal... literals) {
     if (this.miniSat == null && this.cleaneLing == null)
       this.result.add(this.f.clause(literals));
     else if (this.miniSat != null) {
@@ -109,8 +115,8 @@ else if (this.miniSat != null) {
           this.miniSat.underlyingSolver().addName(lit.name(), index);
         }
         int litNum;
-        if (lit instanceof CCAuxiliaryVariable)
-          litNum = !((CCAuxiliaryVariable) lit).negated ? index * 2 : (index * 2) ^ 1;
+        if (lit instanceof EncodingAuxiliaryVariable)
+          litNum = !((EncodingAuxiliaryVariable) lit).negated ? index * 2 : (index * 2) ^ 1;
         else
           litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
         clauseVec.push(litNum);
@@ -120,8 +126,8 @@ else if (this.miniSat != null) {
     } else {
       for (Literal lit : literals) {
         int index = this.cleaneLing.getOrCreateVarIndex(lit.variable());
-        if (lit instanceof CCAuxiliaryVariable)
-          this.cleaneLing.underlyingSolver().addlit(!((CCAuxiliaryVariable) lit).negated ? index : -index);
+        if (lit instanceof EncodingAuxiliaryVariable)
+          this.cleaneLing.underlyingSolver().addlit(!((EncodingAuxiliaryVariable) lit).negated ? index : -index);
         else
           this.cleaneLing.underlyingSolver().addlit(lit.phase() ? index : -index);
       }
@@ -134,7 +140,7 @@ else if (this.miniSat != null) {
    * Adds a clause to the result
    * @param literals the literals of the clause
    */
-  void addClause(final LNGVector<Literal> literals) {
+  public void addClause(final LNGVector<Literal> literals) {
     if (this.miniSat == null && this.cleaneLing == null)
       this.result.add(this.vec2clause(literals));
     else if (this.miniSat != null) {
@@ -143,8 +149,8 @@ else if (this.miniSat != null) {
         int index = this.miniSat.underlyingSolver().idxForName(lit.name());
         assert index != -1;
         int litNum;
-        if (lit instanceof CCAuxiliaryVariable)
-          litNum = !((CCAuxiliaryVariable) lit).negated ? index * 2 : (index * 2) ^ 1;
+        if (lit instanceof EncodingAuxiliaryVariable)
+          litNum = !((EncodingAuxiliaryVariable) lit).negated ? index * 2 : (index * 2) ^ 1;
         else
           litNum = lit.phase() ? index * 2 : (index * 2) ^ 1;
         clauseVec.push(litNum);
@@ -154,8 +160,8 @@ else if (this.miniSat != null) {
     } else {
       for (Literal lit : literals) {
         int index = this.cleaneLing.getOrCreateVarIndex(lit.variable());
-        if (lit instanceof CCAuxiliaryVariable)
-          this.cleaneLing.underlyingSolver().addlit(!((CCAuxiliaryVariable) lit).negated ? index : -index);
+        if (lit instanceof EncodingAuxiliaryVariable)
+          this.cleaneLing.underlyingSolver().addlit(!((EncodingAuxiliaryVariable) lit).negated ? index : -index);
         else
           this.cleaneLing.underlyingSolver().addlit(lit.phase() ? index : -index);
       }
@@ -180,22 +186,22 @@ private Formula vec2clause(final LNGVector<Literal> literals) {
    * Returns a new auxiliary variable.
    * @return a new auxiliary variable
    */
-  Variable newVariable() {
+  public Variable newVariable() {
     if (this.miniSat == null && this.cleaneLing == null)
       return this.f.newCCVariable();
     else if (miniSat != null) {
       final int index = this.miniSat.underlyingSolver().newVar(true, true);
       final String name = FormulaFactory.CC_PREFIX + "MINISAT_" + index;
       this.miniSat.underlyingSolver().addName(name, index);
-      return new CCAuxiliaryVariable(name, false);
+      return new EncodingAuxiliaryVariable(name, false);
     } else
-      return new CCAuxiliaryVariable(this.cleaneLing.createNewVariableOnSolver(FormulaFactory.CC_PREFIX + "CLEANELING"), false);
+      return new EncodingAuxiliaryVariable(this.cleaneLing.createNewVariableOnSolver(FormulaFactory.CC_PREFIX + "CLEANELING"), false);
   }
 
   /**
    * Resets the result.
    */
-  void reset() {
+  public void reset() {
     this.result = new ArrayList<>();
   }
 
diff --git a/src/main/java/org/logicng/pseudobooleans/PBBinaryMerge.java b/src/main/java/org/logicng/pseudobooleans/PBBinaryMerge.java
index 283e48ae..6360e7a7 100644
--- a/src/main/java/org/logicng/pseudobooleans/PBBinaryMerge.java
+++ b/src/main/java/org/logicng/pseudobooleans/PBBinaryMerge.java
@@ -51,7 +51,7 @@
 
 package org.logicng.pseudobooleans;
 
-import org.logicng.cardinalityconstraints.CCResult;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.cardinalityconstraints.CCSorting;
 import org.logicng.collections.LNGIntVector;
 import org.logicng.collections.LNGVector;
@@ -179,7 +179,7 @@ private void binary_merge(LNGVector<Literal> literals, LNGIntVector coefficients
     }
     assert (bucket_card.size() == buckets.size());
     final LNGVector<Literal> carries = new LNGVector<>();
-    final CCResult tempResul = CCResult.resultForFormula(f); // TODO temporary solution
+    final EncodingResult tempResul = EncodingResult.resultForFormula(f); // TODO temporary solution
     for (int i = 0; i < buckets.size(); i++) {
       int k = (int) Math.ceil(new_less_then / Math.pow(2, i));
       if (config.binaryMergeUseWatchDog)
diff --git a/src/main/java/org/logicng/solvers/CleaneLing.java b/src/main/java/org/logicng/solvers/CleaneLing.java
index 322b15a7..ac85f850 100644
--- a/src/main/java/org/logicng/solvers/CleaneLing.java
+++ b/src/main/java/org/logicng/solvers/CleaneLing.java
@@ -30,7 +30,7 @@
 
 import org.logicng.cardinalityconstraints.CCEncoder;
 import org.logicng.cardinalityconstraints.CCIncrementalData;
-import org.logicng.cardinalityconstraints.CCResult;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.collections.LNGBooleanVector;
 import org.logicng.datastructures.Assignment;
 import org.logicng.datastructures.Tristate;
@@ -146,7 +146,7 @@ public void add(final Formula formula) {
       final PBConstraint constraint = (PBConstraint) formula;
       this.result = UNDEF;
       if (constraint.isCC()) {
-        final CCResult result = CCResult.resultForCleaneLing(this.f, this);
+        final EncodingResult result = EncodingResult.resultForCleaneLing(this.f, this);
         ccEncoder.encode(constraint, result);
       } else
         this.addClauseSet(formula.cnf()); //TODO not simply add the cnf here
@@ -158,7 +158,7 @@ public void add(final Formula formula) {
   public CCIncrementalData addIncrementalCC(PBConstraint cc) {
     if (!cc.isCC())
       throw new IllegalArgumentException("Cannot generate an incremental cardinality constraint on a pseudo-Boolean constraint");
-    final CCResult result = CCResult.resultForCleaneLing(this.f, this);
+    final EncodingResult result = EncodingResult.resultForCleaneLing(this.f, this);
     return ccEncoder.encodeIncremental(cc, result);
   }
 
diff --git a/src/main/java/org/logicng/solvers/MiniSat.java b/src/main/java/org/logicng/solvers/MiniSat.java
index 3d5e46c4..6e6a385d 100644
--- a/src/main/java/org/logicng/solvers/MiniSat.java
+++ b/src/main/java/org/logicng/solvers/MiniSat.java
@@ -30,7 +30,7 @@
 
 import org.logicng.cardinalityconstraints.CCEncoder;
 import org.logicng.cardinalityconstraints.CCIncrementalData;
-import org.logicng.cardinalityconstraints.CCResult;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.collections.LNGBooleanVector;
 import org.logicng.collections.LNGIntVector;
 import org.logicng.datastructures.Assignment;
@@ -172,7 +172,7 @@ public static MiniSat miniCard(final FormulaFactory f, final MiniSatConfig confi
   public CCIncrementalData addIncrementalCC(PBConstraint cc) {
     if (!cc.isCC())
       throw new IllegalArgumentException("Cannot generate an incremental cardinality constraint on a pseudo-Boolean constraint");
-    final CCResult result = CCResult.resultForMiniSat(this.f, this);
+    final EncodingResult result = EncodingResult.resultForMiniSat(this.f, this);
     return ccEncoder.encodeIncremental(cc, result);
   }
 
@@ -193,7 +193,7 @@ else if (constraint.comparator() == CType.EQ && constraint.rhs() == 1) {
           } else
             this.addClauseSet(constraint.cnf()); //TODO not simply add the cnf here
         } else {
-          final CCResult result = CCResult.resultForMiniSat(this.f, this);
+          final EncodingResult result = EncodingResult.resultForMiniSat(this.f, this);
           ccEncoder.encode(constraint, result);
         }
       } else