diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java
index 10cc940d..5de12377 100644
--- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java
+++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java
@@ -92,7 +92,7 @@ private SmusComputation() {
      */
     public static <P extends Proposition> List<P> computeSmus(
             final List<P> propositions, final List<Formula> additionalConstraints, final FormulaFactory f) {
-        final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, null, null);
+        final OptimizationConfig cfg = OptimizationConfig.sat(null);
         return computeSmus(propositions, additionalConstraints, f, cfg);
     }
 
@@ -114,7 +114,7 @@ public static <P extends Proposition> List<P> computeSmus(
             final List<Formula> additionalConstraints,
             final FormulaFactory f,
             final OptimizationHandler handler) {
-        final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, null);
+        final OptimizationConfig cfg = OptimizationConfig.sat(handler);
         return computeSmus(propositions, additionalConstraints, f, cfg);
     }
 
@@ -154,7 +154,7 @@ public static List<Formula> computeSmusForFormulas(
             final List<Formula> formulas,
             final List<Formula> additionalConstraints,
             final FormulaFactory f) {
-        final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, null, null);
+        final OptimizationConfig cfg = OptimizationConfig.sat(null);
         return computeSmusForFormulas(formulas, additionalConstraints, f, cfg);
     }
 
@@ -171,7 +171,7 @@ public static List<Formula> computeSmusForFormulas(
             final List<Formula> additionalConstraints,
             final FormulaFactory f,
             final OptimizationHandler handler) {
-        final OptimizationConfig cfg = new OptimizationConfig(SAT_OPTIMIZATION, null, handler, null);
+        final OptimizationConfig cfg = OptimizationConfig.sat(handler);
         return computeSmusForFormulas(formulas, additionalConstraints, f, cfg);
     }
 
diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
index e2aa195e..fde8a8a6 100644
--- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
+++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java
@@ -114,7 +114,7 @@ public static PrimeCompiler getWithMaximization() {
      * @return the prime result
      */
     public PrimeResult compute(final Formula formula, final PrimeResult.CoverageType type) {
-        return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, null, null));
+        return compute(formula, type, OptimizationConfig.sat(null));
     }
 
     /**
@@ -135,7 +135,7 @@ public PrimeResult compute(
             final Formula formula,
             final PrimeResult.CoverageType type,
             final OptimizationHandler handler) {
-        return compute(formula, type, new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, handler, null));
+        return compute(formula, type, OptimizationConfig.sat(handler));
     }
 
     /**
diff --git a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
index 35c8e1f9..1b4cf7ee 100644
--- a/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
+++ b/src/main/java/org/logicng/solvers/maxsat/OptimizationConfig.java
@@ -3,11 +3,26 @@
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.handlers.MaxSATHandler;
 import org.logicng.handlers.OptimizationHandler;
+import org.logicng.handlers.SATHandler;
 import org.logicng.solvers.MaxSATSolver;
 import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
 
 import java.util.Objects;
 
+/**
+ * Configuration for optimization via a SAT or MaxSAT solver.
+ * <p>
+ * Some algorithms use optimization internally.  If they use many incremental
+ * solving steps, they usually use the SAT solver based
+ * {@link org.logicng.solvers.functions.OptimizationFunction}.  For some cases
+ * however it can be more performant to use a MaxSAT solver based optimization
+ * with the drawback of generating the solver again in each step.
+ * <p>
+ * These algorithms can be configured with this config object.
+ *
+ * @version 2.6.0
+ * @since 2.6.0
+ */
 public class OptimizationConfig {
     public enum OptimizationType {
         SAT_OPTIMIZATION,
@@ -24,7 +39,7 @@ public enum OptimizationType {
     private final OptimizationHandler optimizationHandler;
     private final MaxSATHandler maxSATHandler;
 
-    public OptimizationConfig(
+    private OptimizationConfig(
             final OptimizationType optType,
             final MaxSATConfig maxConfig,
             final OptimizationHandler optHandler,
@@ -36,22 +51,62 @@ public OptimizationConfig(
         this.maxSATHandler = maxHandler;
     }
 
-    public OptimizationType getOptimizationType() {
-        return this.optimizationType;
+    /**
+     * Generate a MaxSAT solver based configuration
+     * @param optType the optimization type (MaxSAT algorithm)
+     * @param maxConfig the optional MaxSAT solver configuration
+     * @param maxHandler the optional MaxSAT solver handler
+     * @return the configuration
+     */
+    public static OptimizationConfig maxsat(
+            final OptimizationType optType,
+            final MaxSATConfig maxConfig,
+            final MaxSATHandler maxHandler
+    ) {
+        if (optType == OptimizationType.SAT_OPTIMIZATION) {
+            throw new IllegalArgumentException("SAT Optimization cannot be parametrized with MaxSat config and handler");
+        }
+        return new OptimizationConfig(optType, maxConfig, null, maxHandler);
+    }
+
+    /**
+     * Generate a SAT solver based configuration
+     * @param optHandler the optional optimization handler
+     * @return the configuration
+     */
+    public static OptimizationConfig sat(final OptimizationHandler optHandler) {
+        return new OptimizationConfig(OptimizationType.SAT_OPTIMIZATION, null, optHandler, null);
     }
 
-    public MaxSATConfig getMaxSATConfig() {
-        return this.maxSATConfig;
+    /**
+     * Returns the optimization type.
+     * @return the optimization type
+     */
+    public OptimizationType getOptimizationType() {
+        return this.optimizationType;
     }
 
+    /**
+     * Returns the optional optimization handler.
+     * @return the optional optimization handler
+     */
     public OptimizationHandler getOptimizationHandler() {
         return this.optimizationHandler;
     }
 
+    /**
+     * Returns the optional MaxSAT handler.
+     * @return the optional MaxSAT handler
+     */
     public MaxSATHandler getMaxSATHandler() {
         return this.maxSATHandler;
     }
 
+    /**
+     * Generates a MaxSAT solver with the current configuration.
+     * @param f the formula factory
+     * @return the MAxSAT solver
+     */
     public MaxSATSolver genMaxSATSolver(final FormulaFactory f) {
         switch (this.optimizationType) {
             case MAXSAT_INCWBO:
@@ -71,6 +126,46 @@ public MaxSATSolver genMaxSATSolver(final FormulaFactory f) {
         }
     }
 
+    /**
+     * Starts the solver of this config's handler (if present)
+     */
+    public void startHandler() {
+        if (this.optimizationHandler != null) {
+            this.optimizationHandler.started();
+        }
+        if (this.maxSATHandler != null) {
+            this.maxSATHandler.started();
+        }
+    }
+
+    /**
+     * Return the SAT handler of this config's handler (if present)
+     * @return the SAT handler
+     */
+    public SATHandler satHandler() {
+        if (this.optimizationHandler != null) {
+            return this.optimizationHandler.satHandler();
+        }
+        if (this.maxSATHandler != null) {
+            return this.maxSATHandler.satHandler();
+        }
+        return null;
+    }
+
+    /**
+     * Returns whether this config's handler (if present) was aborted.
+     * @return whether this config's handler was aborted
+     */
+    public boolean aborted() {
+        if (this.optimizationHandler != null) {
+            return this.optimizationHandler.aborted();
+        }
+        if (this.maxSATHandler != null) {
+            return this.maxSATHandler.aborted();
+        }
+        return false;
+    }
+
     @Override
     public boolean equals(final Object object) {
         if (this == object) {
diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
index e5e78f80..594e2e70 100644
--- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
+++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java
@@ -28,19 +28,29 @@
 
 package org.logicng.transformations.simplification;
 
+import org.logicng.backbones.Backbone;
+import org.logicng.backbones.BackboneGeneration;
+import org.logicng.backbones.BackboneType;
 import org.logicng.configurations.ConfigurationType;
+import org.logicng.datastructures.Assignment;
+import org.logicng.explanations.smus.SmusComputation;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.FormulaTransformation;
 import org.logicng.formulas.Literal;
 import org.logicng.handlers.OptimizationHandler;
+import org.logicng.primecomputation.PrimeCompiler;
+import org.logicng.primecomputation.PrimeResult;
+import org.logicng.solvers.maxsat.OptimizationConfig;
 import org.logicng.util.FormulaHelper;
 
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.List;
 import java.util.SortedSet;
 import java.util.TreeSet;
+import java.util.stream.Collectors;
 
 /**
  * An advanced simplifier for formulas.
@@ -59,7 +69,7 @@
  * </ul>
  * The first and the last two steps can be configured using the {@link AdvancedSimplifierConfig}. Also, the handler and the rating
  * function can be configured. If no rating function is specified, the {@link DefaultRatingFunction} is chosen.
- * @version 2.3.0
+ * @version 2.6.0
  * @since 2.0.0
  */
 public final class AdvancedSimplifier implements FormulaTransformation {
@@ -113,25 +123,26 @@ public Formula apply(final Formula formula, final boolean cache) {
         final AdvancedSimplifierConfig config = this.initConfig != null
                 ? this.initConfig
                 : (AdvancedSimplifierConfig) formula.factory().configurationFor(ConfigurationType.ADVANCED_SIMPLIFIER);
-        //start(config.handler); // TODO activate
+        final OptimizationConfig cfg = config.optimizationConfig;
+        cfg.startHandler();
         final FormulaFactory f = formula.factory();
         Formula simplified = formula;
         final SortedSet<Literal> backboneLiterals = new TreeSet<>();
         if (config.restrictBackbone) {
-            //final Backbone backbone = BackboneGeneration // TODO activate
-            //        .compute(Collections.singletonList(formula), formula.variables(), BackboneType.POSITIVE_AND_NEGATIVE, satHandler(config.handler));
-            //if (backbone == null || aborted(config.handler)) {
-            //    return null;
-            //}
-            //if (!backbone.isSat()) {
-            //    return f.falsum();
-            //}
-            //backboneLiterals.addAll(backbone.getCompleteBackbone());
-            //simplified = formula.restrict(new Assignment(backboneLiterals));
+            final Backbone backbone = BackboneGeneration
+                    .compute(Collections.singletonList(formula), formula.variables(), BackboneType.POSITIVE_AND_NEGATIVE, cfg.satHandler());
+            if (backbone == null || cfg.aborted()) {
+                return config.returnIntermediateResult ? formula : null;
+            }
+            if (!backbone.isSat()) {
+               return f.falsum();
+            }
+            backboneLiterals.addAll(backbone.getCompleteBackbone());
+            simplified = formula.restrict(new Assignment(backboneLiterals));
         }
         final Formula simplifyMinDnf = computeMinDnf(f, simplified, config);
         if (simplifyMinDnf == null) {
-            return null;
+            return config.returnIntermediateResult ? simplified : null;
         }
         simplified = simplifyWithRating(simplified, simplifyMinDnf, config);
         if (config.factorOut) {
@@ -149,19 +160,18 @@ public Formula apply(final Formula formula, final boolean cache) {
     }
 
     private Formula computeMinDnf(final FormulaFactory f, final Formula simplified, final AdvancedSimplifierConfig config) {
-        //final PrimeResult primeResult = //TODO
-        //        PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.handler);
-        //if (primeResult == null || aborted(config.handler)) {
-        //    return null;
-        //}
-        //final List<SortedSet<Literal>> primeImplicants = primeResult.getPrimeImplicants();
-        //final List<Formula> minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f),
-        //        Collections.singletonList(simplified), f, config.handler);
-        //if (minimizedPIs == null || aborted(config.handler)) {
-        //    return null;
-        //}
-        //simplified = f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList()));
-        return simplified;
+        final PrimeResult primeResult =
+               PrimeCompiler.getWithMinimization().compute(simplified, PrimeResult.CoverageType.IMPLICANTS_COMPLETE, config.optimizationConfig);
+        if (primeResult == null || config.optimizationConfig.aborted()) {
+            return null;
+        }
+        final List<SortedSet<Literal>> primeImplicants = primeResult.getPrimeImplicants();
+        final List<Formula> minimizedPIs = SmusComputation.computeSmusForFormulas(negateAllLiterals(primeImplicants, f),
+               Collections.singletonList(simplified), f, config.optimizationConfig);
+        if (minimizedPIs == null || config.optimizationConfig.aborted()) {
+            return null;
+        }
+        return f.or(negateAllLiteralsInFormulas(minimizedPIs, f).stream().map(f::and).collect(Collectors.toList()));
     }
 
     private List<Formula> negateAllLiterals(final Collection<SortedSet<Literal>> literalSets, final FormulaFactory f) {
diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
index 83c8d063..cdfada01 100644
--- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
+++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifierConfig.java
@@ -28,6 +28,8 @@
 
 package org.logicng.transformations.simplification;
 
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION;
+
 import org.logicng.configurations.Configuration;
 import org.logicng.configurations.ConfigurationType;
 import org.logicng.handlers.OptimizationHandler;
@@ -35,7 +37,7 @@
 
 /**
  * The configuration object for the {@link AdvancedSimplifier}.
- * @version 2.3.0
+ * @version 2.6.0
  * @since 2.3.0
  */
 
@@ -44,6 +46,7 @@ public class AdvancedSimplifierConfig extends Configuration {
     boolean restrictBackbone;
     boolean factorOut;
     boolean simplifyNegations;
+    boolean returnIntermediateResult;
     RatingFunction<?> ratingFunction;
     OptimizationConfig optimizationConfig;
 
@@ -53,6 +56,7 @@ public String toString() {
                 "restrictBackbone=" + this.restrictBackbone +
                 ", factorOut=" + this.factorOut +
                 ", simplifyNegations=" + this.simplifyNegations +
+                ", returnIntermediateResult=" + this.returnIntermediateResult +
                 ", ratingFunction=" + this.ratingFunction +
                 ", optimizationConfig=" + this.optimizationConfig +
                 '}';
@@ -67,6 +71,7 @@ private AdvancedSimplifierConfig(final Builder builder) {
         this.restrictBackbone = builder.restrictBackbone;
         this.factorOut = builder.factorOut;
         this.simplifyNegations = builder.simplifyNegations;
+        this.returnIntermediateResult = builder.returnIntermediateResult;
         this.ratingFunction = builder.ratingFunction;
         this.optimizationConfig = builder.optimizationConfig;
     }
@@ -87,15 +92,17 @@ public static class Builder {
         boolean restrictBackbone = true;
         boolean factorOut = true;
         boolean simplifyNegations = true;
-        private RatingFunction<?> ratingFunction = new DefaultRatingFunction();
-        private OptimizationConfig optimizationConfig = null;
+        boolean returnIntermediateResult = false;
+        private RatingFunction<?> ratingFunction = DefaultRatingFunction.get();
+        private OptimizationConfig optimizationConfig = OptimizationConfig.sat(null);
 
         private Builder() {
             // Initialize only via factory
         }
 
         /**
-         * Sets the flag for whether the formula should be restricted with the backbone. The default is 'true'.
+         * Sets the flag for whether the formula should be restricted with the
+         * backbone. The default is 'true'.
          * @param restrictBackbone flag for the restriction
          * @return the current builder
          */
@@ -105,7 +112,8 @@ public Builder restrictBackbone(final boolean restrictBackbone) {
         }
 
         /**
-         * Sets the flag for whether the formula should be factorized. The default is 'true'.
+         * Sets the flag for whether the formula should be factorized. The
+         * default is 'true'.
          * @param factorOut flag for the factorisation
          * @return the current builder
          */
@@ -115,7 +123,8 @@ public Builder factorOut(final boolean factorOut) {
         }
 
         /**
-         * Sets the flag for whether negations shall be simplified. The default is 'true'.
+         * Sets the flag for whether negations shall be simplified. The
+         * default is 'true'.
          * @param simplifyNegations flag
          * @return the current builder
          */
@@ -125,8 +134,11 @@ public Builder simplifyNegations(final boolean simplifyNegations) {
         }
 
         /**
-         * Sets the rating function. The aim of the simplification is to minimize the formula with respect to this rating function,
-         * e.g. finding a formula with a minimal number of symbols when represented as string. The default is the {@code DefaultRatingFunction}.
+         * Sets the rating function. The aim of the simplification is to
+         * minimize the formula with respect to this rating function,
+         * e.g. finding a formula with a minimal number of symbols when
+         * represented as string. The default is the
+         * {@code DefaultRatingFunction}.
          * @param ratingFunction the desired rating function
          * @return the current builder
          */
@@ -136,22 +148,40 @@ public Builder ratingFunction(final RatingFunction<?> ratingFunction) {
         }
 
         /**
-         * Sets the handler to control the computation. The default is 'no handler'.
+         * Sets the handler to control the computation. The default is
+         * 'no handler'.
          * @param handler the optimization handler
          * @return the current builder
          * @deprecated use the {@link #optimizationConfig}
          */
         @Deprecated
         public Builder handler(final OptimizationHandler handler) {
-            this.optimizationConfig = new OptimizationConfig(OptimizationConfig.OptimizationType.SAT_OPTIMIZATION, null, handler, null);
+            this.optimizationConfig = OptimizationConfig.sat(handler);
             return this;
         }
 
+        /**
+         * Sets the optimization config of the computation.  The default is a
+         * config with a SAT based optimization without a handler.
+         * @param config the optimization config
+         * @return the current builder
+         */
         public Builder optimizationConfig(final OptimizationConfig config) {
             this.optimizationConfig = config;
             return this;
         }
 
+        /**
+         * Sets whether the intermediate result should be returned in case of
+         * a handler abortion.  The default is 'false'.
+         * @param returnIntermediateResult the flag
+         * @return the current builder
+         */
+        public Builder returnIntermediateResult(final boolean returnIntermediateResult) {
+            this.returnIntermediateResult = returnIntermediateResult;
+            return this;
+        }
+
         /**
          * Builds the configuration.
          * @return the configuration.
diff --git a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
index bc445360..e4a24068 100644
--- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
+++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java
@@ -35,7 +35,6 @@
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3;
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL;
 import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO;
-import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.SAT_OPTIMIZATION;
 
 import org.junit.jupiter.api.Test;
 import org.junit.jupiter.params.ParameterizedTest;
@@ -68,13 +67,13 @@ public class SmusComputationTest extends TestWithExampleFormulas {
 
     public static Collection<Object[]> configs() {
         final List<Object[]> configs = new ArrayList<>();
-        configs.add(new Object[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_INCWBO, null, null, null), "INCWBO"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_SU, null, null, null), "LINEAR_SU"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_US, null, null, null), "LINEAR_US"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_MSU3, null, null, null), "MSU3"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_OLL, null, null, null), "OLL"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_WBO, null, null, null), "WBO"});
+        configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"});
         return configs;
     }
 
diff --git a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java
index 78963778..b9530d06 100644
--- a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java
+++ b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java
@@ -78,23 +78,23 @@ public class PrimeCompilerTest extends TestWithExampleFormulas {
 
     public static Collection<Object[]> configs() {
         final List<Object[]> configs = new ArrayList<>();
-        configs.add(new Object[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_INCWBO, null, null, null), "INCWBO"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_SU, null, null, null), "LINEAR_SU"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_US, null, null, null), "LINEAR_US"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_MSU3, null, null, null), "MSU3"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_OLL, null, null, null), "OLL"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_WBO, null, null, null), "WBO"});
+        configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"});
         return configs;
     }
 
     public static Collection<Object[]> fastConfigs() {
         final List<Object[]> configs = new ArrayList<>();
-        configs.add(new Object[]{new OptimizationConfig(SAT_OPTIMIZATION, null, null, null), "SAT"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_SU, null, null, null), "LINEAR_SU"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_LINEAR_US, null, null, null), "LINEAR_US"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_MSU3, null, null, null), "MSU3"});
-        configs.add(new Object[]{new OptimizationConfig(MAXSAT_OLL, null, null, null), "OLL"});
+        configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"});
         return configs;
     }
 
diff --git a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java
index be2b3cad..ec902ca3 100644
--- a/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java
+++ b/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java
@@ -29,8 +29,16 @@
 package org.logicng.transformations.simplification;
 
 import static org.assertj.core.api.Assertions.assertThat;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_INCWBO;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_SU;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_LINEAR_US;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_MSU3;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_OLL;
+import static org.logicng.solvers.maxsat.OptimizationConfig.OptimizationType.MAXSAT_WBO;
 
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.MethodSource;
 import org.logicng.LongRunningTag;
 import org.logicng.RandomTag;
 import org.logicng.TestWithExampleFormulas;
@@ -43,46 +51,80 @@
 import org.logicng.io.parsers.ParserException;
 import org.logicng.io.readers.FormulaReader;
 import org.logicng.predicates.satisfiability.TautologyPredicate;
+import org.logicng.solvers.maxsat.OptimizationConfig;
 import org.logicng.util.FormulaCornerCases;
 import org.logicng.util.FormulaRandomizer;
 import org.logicng.util.FormulaRandomizerConfig;
 
 import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Paths;
+import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.Collection;
 import java.util.List;
 
 /**
  * Unit Tests for the class {@link AdvancedSimplifier}.
- * @version 2.3.0
+ * @version 2.6.0
  * @since 2.0.0
  */
 public class AdvancedSimplifierTest extends TestWithExampleFormulas {
 
-    private final AdvancedSimplifier simplifier = new AdvancedSimplifier();
+    public static Collection<Object[]> configs() {
+        final List<Object[]> configs = new ArrayList<>();
+        configs.add(new Object[]{OptimizationConfig.sat(null), "SAT"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_INCWBO, null, null), "INCWBO"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_SU, null, null), "LINEAR_SU"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_LINEAR_US, null, null), "LINEAR_US"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_MSU3, null, null), "MSU3"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_OLL, null, null), "OLL"});
+        configs.add(new Object[]{OptimizationConfig.maxsat(MAXSAT_WBO, null, null), "WBO"});
+        return configs;
+    }
 
-    @Test
-    public void testConstants() {
-        assertThat(this.f.falsum().transform(this.simplifier)).isEqualTo(this.f.falsum());
-        assertThat(this.f.verum().transform(this.simplifier)).isEqualTo(this.f.verum());
+    @ParameterizedTest
+    @MethodSource("configs")
+    public void testConstants(final OptimizationConfig cfg) {
+        final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build());
+        assertThat(this.f.falsum().transform(simplifier)).isEqualTo(this.f.falsum());
+        assertThat(this.f.verum().transform(simplifier)).isEqualTo(this.f.verum());
     }
 
-    @Test
-    public void testCornerCases() {
+    @ParameterizedTest
+    @MethodSource("configs")
+    public void testCornerCases(final OptimizationConfig cfg) {
+        final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build());
         final FormulaCornerCases cornerCases = new FormulaCornerCases(this.f);
-        cornerCases.cornerCases().forEach(this::computeAndVerify);
+        cornerCases.cornerCases().forEach(it -> computeAndVerify(it, simplifier));
     }
 
-    @Test
+    @ParameterizedTest
+    @MethodSource("configs")
     @RandomTag
-    public void testRandomized() {
+    public void testRandomized(final OptimizationConfig cfg) {
+        final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build());
         for (int i = 0; i < 100; i++) {
             final FormulaFactory f = new FormulaFactory();
             final FormulaRandomizer randomizer = new FormulaRandomizer(f, FormulaRandomizerConfig.builder().numVars(8).weightPbc(2).seed(i * 42).build());
             final Formula formula = randomizer.formula(5);
-            computeAndVerify(formula);
+            computeAndVerify(formula, simplifier);
         }
     }
 
+    @ParameterizedTest
+    @MethodSource("configs")
+    public void testOriginalFormula(final OptimizationConfig cfg) throws IOException {
+        final AdvancedSimplifier simplifier = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().optimizationConfig(cfg).build());
+        Files.lines(Paths.get("src/test/resources/formulas/simplify_formulas.txt"))
+                .filter(s -> !s.isEmpty())
+                .forEach(s -> {
+                    final FormulaFactory f = new FormulaFactory();
+                    final Formula formula = parse(f, s);
+                    computeAndVerify(formula, simplifier);
+                });
+    }
+
     @Test
     public void testTimeoutHandlerSmall() {
         final List<TimeoutOptimizationHandler> handlers = Arrays.asList(
@@ -92,7 +134,8 @@ public void testTimeoutHandlerSmall() {
         );
         final Formula formula = parse(this.f, "a & b | ~c & a");
         for (final TimeoutOptimizationHandler handler : handlers) {
-            testHandler(handler, formula, false);
+            testHandler(handler, formula, false, false);
+            testHandler(handler, formula, false, true);
         }
     }
 
@@ -105,7 +148,8 @@ public void testTimeoutHandlerLarge() throws IOException, ParserException {
         );
         final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", this.f);
         for (final TimeoutOptimizationHandler handler : handlers) {
-            testHandler(handler, formula, true);
+            testHandler(handler, formula, true, false);
+            testHandler(handler, formula, true, true);
         }
     }
 
@@ -113,14 +157,16 @@ public void testTimeoutHandlerLarge() throws IOException, ParserException {
     public void testPrimeCompilerIsCancelled() {
         final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 0);
         final Formula formula = parse(this.f, "a&(b|c)");
-        testHandler(handler, formula, true);
+        testHandler(handler, formula, true, false);
+        testHandler(handler, formula, true, true);
     }
 
     @Test
     public void testSmusComputationIsCancelled() {
         final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 5);
         final Formula formula = parse(this.f, "a&(b|c)");
-        testHandler(handler, formula, true);
+        testHandler(handler, formula, true, false);
+        testHandler(handler, formula, true, true);
     }
 
     @LongRunningTag
@@ -132,7 +178,7 @@ public void testCancellationPoints() {
         for (int numOptimizationStarts = 1; numOptimizationStarts < 30; numOptimizationStarts++) {
             for (int numSatHandlerStarts = 1; numSatHandlerStarts < 500; numSatHandlerStarts++) {
                 final OptimizationHandler handler = new BoundedOptimizationHandler(numSatHandlerStarts, numOptimizationStarts);
-                testHandler(handler, formula, true);
+                testHandler(handler, formula, true, false);
             }
         }
     }
@@ -164,20 +210,28 @@ public void testAdvancedSimplifierConfig() {
         }
     }
 
-    private void computeAndVerify(final Formula formula) {
-        final Formula simplified = formula.transform(this.simplifier);
+    private void computeAndVerify(final Formula formula, final AdvancedSimplifier simplifier) {
+        final Formula simplified = formula.transform(simplifier);
         assertThat(formula.factory().equivalence(formula, simplified).holds(new TautologyPredicate(this.f)))
                 .as("Minimized formula is equivalent to original Formula")
                 .isTrue();
     }
 
-    private void testHandler(final OptimizationHandler handler, final Formula formula, final boolean expAborted) {
-        final AdvancedSimplifier simplifierWithHandler = new AdvancedSimplifier(AdvancedSimplifierConfig.builder().handler(handler).build());
+    private void testHandler(final OptimizationHandler handler, final Formula formula, final boolean expAborted, final boolean expIntermediate) {
+        final AdvancedSimplifier simplifierWithHandler = new AdvancedSimplifier(AdvancedSimplifierConfig.builder()
+                .optimizationConfig(OptimizationConfig.sat(handler))
+                .returnIntermediateResult(expIntermediate)
+                .build());
         final Formula simplified = formula.transform(simplifierWithHandler);
         assertThat(handler.aborted()).isEqualTo(expAborted);
         if (expAborted) {
             assertThat(handler.aborted()).isTrue();
-            assertThat(simplified).isNull();
+            if (!expIntermediate) {
+                assertThat(simplified).isNull();
+            } else {
+                assertThat(simplified).isNotNull();
+                assertThat(simplified.isEquivalentTo(formula)).isTrue();
+            }
         } else {
             assertThat(handler.aborted()).isFalse();
             assertThat(simplified).isNotNull();