diff --git a/__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts b/__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts
index d4d2506..0382853 100644
--- a/__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts
+++ b/__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts
@@ -1,8 +1,7 @@
 import each from "jest-each";
-import { regexBlank } from "../../../src/converter/dimacs/Syntax/CommonSyntax";
 import { DimacsParser } from "../../../src/converter/dimacs/DimacsParser";
+import { regexBlank } from "../../../src/converter/dimacs/Syntax/CommonSyntax";
 import { regexComment } from "../../../src/converter/dimacs/Syntax/DimacsSyntax";
-import { LogicalExpressionParser } from "../../../src/converter/dimacs/LogicalExpressionParser";
 import { regexNOT } from "../../../src/converter/dimacs/Syntax/LogicalExpressionSyntax";
 
 function isEquivalentLogicalExpression(f1: string, f2: string) {
@@ -19,36 +18,6 @@ function isEquivalentDimacs(f1: string, f2: string) {
 
 describe("Parsing", () => {
   let dimacsParser = new DimacsParser();
-  let logicalExpressionParser = new LogicalExpressionParser();
-
-  each([
-    [
-      "((1 or 2 or not 3) and (!4 and (not 5 and 6)) and 3 and (7 or 2))",
-      "c First comment\nc Some Comment\nc 1 => 1\np sat 7\n*(+( 1  2  -3 )*( -4 *( -5  6 )) 3 +( 7  2 ))",
-    ],
-    [
-      "(1 or (2 and 3) or (((1 and 4) or 5) and 6))",
-      "p sat 6\n+(1 *(2  3)*(+(*(1  4) 5) 6))",
-    ],
-    [
-      "(((1 and not 2 and 3 and 4) or 3) and 5)",
-      "c Sample DIMACS .sat file\np sat 5\n*(+(*(1  -2  3  4) 3) 5)",
-    ],
-    ["((1 and not 2) or 3)", "p sat 3\n+(*(1 -2) 3)"],
-    ["((1 and 2) or not 3)", "p sat 3\n+(*(1 2) -3)"],
-  ]).test(
-    "parsing bi-directional",
-    (logicalExpression: string, dimacs: string) => {
-      isEquivalentDimacs(
-        logicalExpressionParser.parseDimacs(logicalExpression),
-        dimacs
-      );
-      isEquivalentLogicalExpression(
-        dimacsParser.parseLogicalExpression(dimacs),
-        logicalExpression
-      );
-    }
-  );
 
   each([
     [
diff --git a/src/api/ToolboxAPI.ts b/src/api/ToolboxAPI.ts
index d0703f0..4b86d3c 100644
--- a/src/api/ToolboxAPI.ts
+++ b/src/api/ToolboxAPI.ts
@@ -10,6 +10,19 @@ import { SolveRequest } from "./data-model/SolveRequest";
  */
 export const baseUrl = () => process.env.NEXT_PUBLIC_API_BASE_URL;
 
+function invalidSolution(reason: string): Solution {
+  return {
+    id: -1,
+    status: SolutionStatus.INVALID,
+    solverName: "",
+    executionMilliseconds: 0,
+    solutionData: "",
+    debugData: "",
+    metaData: "",
+    error: `${reason}`,
+  };
+}
+
 export async function postProblem<T>(
   problemType: string,
   solveRequest: SolveRequest<T>
@@ -23,18 +36,19 @@ export async function postProblem<T>(
   })
     .then((response) => response.json())
     .then((json) => json as Solution)
-    .catch((reason) => {
-      return {
-        id: -1,
-        status: SolutionStatus.INVALID,
-        solverName: "",
-        executionMilliseconds: 0,
-        solutionData: "",
-        debugData: "",
-        metaData: "",
-        error: `${reason}`,
-      };
-    });
+    .catch(invalidSolution);
+}
+
+export async function fetchSolution(problemType: string, solutionId: number) {
+  return fetch(`${baseUrl()}/solution/${problemType}?id=${solutionId}`, {
+    method: "GET",
+    headers: {
+      "Content-Type": "application/json",
+    },
+  })
+    .then((response) => response.json())
+    .then((json) => json as Solution)
+    .catch(invalidSolution);
 }
 
 export async function fetchSolvers(
diff --git a/src/components/solvers/History.tsx b/src/components/solvers/History.tsx
new file mode 100644
index 0000000..6e8ea84
--- /dev/null
+++ b/src/components/solvers/History.tsx
@@ -0,0 +1,52 @@
+import {
+  Button,
+  Divider,
+  Heading,
+  List,
+  ListItem,
+  Stack,
+  Tooltip,
+} from "@chakra-ui/react";
+import { ProblemState } from "./HistoryStorage";
+
+interface HistoryProps<T> {
+  problemStates: ProblemState<T>[];
+
+  onRequestRollback: (problemState: ProblemState<T>) => void;
+}
+
+export const History = <T extends {}>(props: HistoryProps<T>) => {
+  if (props.problemStates.length == 0) return null;
+
+  function reloadState(state: ProblemState<T>) {
+    props.onRequestRollback(state);
+  }
+
+  return (
+    <Stack>
+      <Heading as="h3" size="md" textAlign="center">
+        History
+      </Heading>
+      <List>
+        {props.problemStates.map((x) => {
+          let problemString = x.problemInput.toString();
+          return (
+            <ListItem key={problemString}>
+              <Tooltip label={problemString}>
+                <Button
+                  width="200px"
+                  overflow="hidden"
+                  variant="link"
+                  onClick={(_) => reloadState(x)}
+                >
+                  {problemString}
+                </Button>
+              </Tooltip>
+              <Divider />
+            </ListItem>
+          );
+        })}
+      </List>
+    </Stack>
+  );
+};
diff --git a/src/components/solvers/HistoryStorage.ts b/src/components/solvers/HistoryStorage.ts
new file mode 100644
index 0000000..5fc8265
--- /dev/null
+++ b/src/components/solvers/HistoryStorage.ts
@@ -0,0 +1,30 @@
+import { SolutionIds } from "./ProgressHandler";
+
+export interface ProblemState<T> {
+  /**
+   * Problem input
+   */
+  problemInput: T;
+  /**
+   * Ids of the solutions of the problem input per problem type
+   */
+  solutionIds: SolutionIds;
+}
+
+export function getHistory<T>(problemTypes: string[]): ProblemState<T>[] {
+  let historyItem = localStorage.getItem(getStoreId(problemTypes));
+  if (historyItem === null) return [];
+
+  return JSON.parse(historyItem);
+}
+
+export function storeHistory<T>(
+  problemTypes: string[],
+  history: ProblemState<T>[]
+) {
+  localStorage.setItem(getStoreId(problemTypes), JSON.stringify(history));
+}
+
+export function getStoreId(problemTypes: string[]) {
+  return `problemStates-${problemTypes}`;
+}
diff --git a/src/components/solvers/ProgressHandler.tsx b/src/components/solvers/ProgressHandler.tsx
index de12e0b..2ade649 100644
--- a/src/components/solvers/ProgressHandler.tsx
+++ b/src/components/solvers/ProgressHandler.tsx
@@ -1,19 +1,26 @@
-import { Box, Center, HStack, VStack } from "@chakra-ui/react";
-import React, { useState } from "react";
-import { GoButton } from "./buttons/GoButton";
-import { postProblem } from "../../api/ToolboxAPI";
-import { SolutionView } from "./SolutionView";
-import { Container } from "../Container";
+import { Box, Center, HStack } from "@chakra-ui/react";
+import { useEffect, useState } from "react";
 import { Solution } from "../../api/data-model/Solution";
 import { SolveRequest } from "../../api/data-model/SolveRequest";
+import { fetchSolution, postProblem } from "../../api/ToolboxAPI";
+import { Container } from "../Container";
+import { GoButton } from "./buttons/GoButton";
+import { History } from "./History";
+import { getHistory, ProblemState, storeHistory } from "./HistoryStorage";
+import { SolutionView } from "./SolutionView";
 import { SolverPicker } from "./SolverPicker";
 
+export type SolutionIds = {
+  [problemTypeId: string]: number;
+};
+
 export interface ProgressHandlerProps<T> {
   /**
    * List of problem types that should be solved with the given input.
    */
   problemTypes: string[];
   problemInput: T;
+  setProblemInput: (t: T) => void;
 }
 
 export const ProgressHandler = <T extends {}>(
@@ -22,11 +29,26 @@ export const ProgressHandler = <T extends {}>(
   const [wasClicked, setClicked] = useState<boolean>(false);
   const [finished, setFinished] = useState<boolean>(false);
   const [solutions, setSolutions] = useState<Solution[]>();
+  const [problemStates, setProblemStates] = useState<ProblemState<T>[]>([]);
   const [solveRequest, setSolveRequest] = useState<SolveRequest<T>>({
     requestContent: props.problemInput,
     requestedSubSolveRequests: {},
   });
 
+  useEffect(() => {
+    // Handle problem states from local storage
+    if (problemStates.length == 0) {
+      let history = getHistory<T>(props.problemTypes);
+      if (history.length > 0) {
+        setProblemStates(history);
+      }
+    }
+  }, [problemStates, props.problemTypes]);
+
+  useEffect(() => {
+    storeHistory(props.problemTypes, problemStates);
+  }, [problemStates, props.problemTypes]);
+
   async function startSolving() {
     setClicked(true);
     setFinished(false);
@@ -39,7 +61,35 @@ export const ProgressHandler = <T extends {}>(
     setSolveRequest(newSolveRequest);
     Promise.all(
       props.problemTypes.map((problemType) =>
-        postProblem(problemType, newSolveRequest)
+        postProblem(problemType, newSolveRequest).then((s) => ({
+          problemType: problemType,
+          solution: s,
+        }))
+      )
+    ).then((result) => {
+      let solutionIdMap = result.reduce((acc, item) => {
+        acc[item.problemType] = item.solution.id;
+        return acc;
+      }, {} as SolutionIds);
+
+      let newProblemState: ProblemState<T> = {
+        problemInput: props.problemInput,
+        solutionIds: solutionIdMap,
+      };
+
+      setSolutions(result.map((x) => x.solution));
+      setProblemStates([...problemStates, newProblemState]);
+      setFinished(true);
+    });
+  }
+
+  async function loadSolution(ids: SolutionIds) {
+    setClicked(true);
+    setFinished(false);
+
+    Promise.all(
+      props.problemTypes.map((problemType) =>
+        fetchSolution(problemType, ids[problemType])
       )
     ).then((solutions) => {
       setSolutions(solutions);
@@ -86,6 +136,14 @@ export const ProgressHandler = <T extends {}>(
             </Box>
           ))
         : null}
+
+      <History
+        problemStates={problemStates}
+        onRequestRollback={(problemState) => {
+          props.setProblemInput(problemState.problemInput);
+          loadSolution(problemState.solutionIds);
+        }}
+      />
     </Container>
   );
 };
diff --git a/src/components/solvers/SAT/TextArea.tsx b/src/components/solvers/SAT/TextArea.tsx
index b18ca71..43db5dd 100644
--- a/src/components/solvers/SAT/TextArea.tsx
+++ b/src/components/solvers/SAT/TextArea.tsx
@@ -1,13 +1,12 @@
+import { Box } from "@chakra-ui/react";
+import { highlight } from "prismjs";
 import "prismjs/themes/prism-solarizedlight.css"; //TODO: use custom styling
-import React from "react";
 import Editor from "react-simple-code-editor";
-import { highlight } from "prismjs";
-import { Box, Container } from "@chakra-ui/react";
 import { SAT_language } from "./prism-SAT";
 
 interface TextAreaProps {
   problemString: string;
-  setProblemString: React.Dispatch<React.SetStateAction<string>>;
+  setProblemString: (problemString: string) => void;
 }
 
 export const TextArea = (props: TextAreaProps) => {
diff --git a/src/components/solvers/SAT/prism-SAT.ts b/src/components/solvers/SAT/prism-SAT.ts
index ba230f3..0cf8dc9 100644
--- a/src/components/solvers/SAT/prism-SAT.ts
+++ b/src/components/solvers/SAT/prism-SAT.ts
@@ -1,7 +1,7 @@
 import { regexVariable } from "../../../converter/dimacs/Syntax/CommonSyntax";
 import {
   regexAND,
-  regexNOTVariable,
+  regexNOT,
   regexOR,
 } from "../../../converter/dimacs/Syntax/LogicalExpressionSyntax";
 
@@ -16,7 +16,7 @@ export const SAT_language = {
   },
   "SAT-punctuation": /[()]/,
   negation: {
-    pattern: regexNOTVariable,
+    pattern: regexNOT,
     alias: "string",
   },
   "SAT-variable": {
diff --git a/src/components/solvers/TextInputMask.tsx b/src/components/solvers/TextInputMask.tsx
index ec44db7..8d83f93 100644
--- a/src/components/solvers/TextInputMask.tsx
+++ b/src/components/solvers/TextInputMask.tsx
@@ -1,24 +1,21 @@
-import { Divider, Text, Textarea } from "@chakra-ui/react";
+import { Divider, Textarea } from "@chakra-ui/react";
 import Head from "next/head";
-import React, { ReactElement, useState } from "react";
+import { ReactElement, useState } from "react";
 import { Container } from "../Container";
-import { Main } from "../Main";
-import { Help } from "./SAT/Help";
 import { EditorControls } from "./EditorControls";
 
 export interface TextInputMaskProperties {
   textPlaceholder: string;
-  onTextChanged: (text: string) => void;
+  text: string;
+  onTextChanged: (value: string) => void;
   body?: ReactElement;
 }
 
 export const TextInputMask = (props: TextInputMaskProperties) => {
-  const [text, setText] = useState<string>("");
   const [errorString, setErrorString] = useState("");
 
   function onTextChanged(text: string): void {
     try {
-      setText(text);
       props.onTextChanged(text);
 
       setErrorString("");
@@ -40,11 +37,11 @@ export const TextInputMask = (props: TextInputMaskProperties) => {
         errorText={errorString}
         idleText={props.textPlaceholder + " 👇"}
         onUpload={onTextChanged}
-        editorContent={text}
+        editorContent={props.text}
       />
       <Textarea
         placeholder={props.textPlaceholder}
-        value={text}
+        value={props.text}
         minHeight="10rem"
         isInvalid={errorString != ""}
         onChange={(x) => onTextChanged(x.target.value)}
diff --git a/src/converter/dimacs/LogicalExpressionParser.ts b/src/converter/dimacs/LogicalExpressionParser.ts
index e586eaf..fd36e7f 100644
--- a/src/converter/dimacs/LogicalExpressionParser.ts
+++ b/src/converter/dimacs/LogicalExpressionParser.ts
@@ -5,33 +5,20 @@ import {
   variableRule,
   blankRule,
 } from "./Syntax/CommonSyntax";
-import {
-  andRule,
-  negatedVariableRule,
-  negateRule,
-  orRule,
-} from "./Syntax/LogicalExpressionSyntax";
+import { andRule, negateRule, orRule } from "./Syntax/LogicalExpressionSyntax";
 
 // the order is important - tokens are applied from first to last
 const rules = [
   ...parenthesesRule,
   orRule,
   andRule,
-  negatedVariableRule,
+  negateRule,
   variableRule,
   blankRule,
 ];
-const rulesNegation = [negateRule, variableRule, blankRule];
-
-interface LeveledToken {
-  level: number;
-  token: Token;
-}
 
 export class LogicalExpressionParser {
   private lex: Lexer = new Lexer(rules);
-  private lexNegation: Lexer = new Lexer(rulesNegation);
-  private output: string = "";
 
   /**
    * Converts a logical expression to an expression in dimacs sat format
@@ -39,31 +26,12 @@ export class LogicalExpressionParser {
    * @param logicalExpression {string} logical expression
    * @returns {string} formula in dimacs sat format of the input
    */
-  public parseDimacs(logicalExpression: string): string {
-    this.output = "";
-
+  public validateLogicalExpression(logicalExpression: string): string[] {
     let tokens = this.lex.tokenize(logicalExpression);
-    if (tokens.length == 0) return this.output;
+    if (tokens.length == 0) return [];
 
     //Verify formula integrity
-    let errors = this.verifyTokens(tokens);
-    if (errors.length > 0) {
-      let errorStr = "";
-      for (let error of errors) errorStr += error + "\n";
-
-      throw new Error(errorStr);
-    }
-
-    //Handle variable comments and program start
-    let variables = this.convertVariables(tokens);
-    variables.forEach((num, str, _) => {
-      this.output += `c ${num} ${TokenName.variableAssignment} ${str}\n`;
-    });
-    this.output += `p sat ${variables.size}\n`;
-
-    this.parseFormula(tokens);
-
-    return this.output;
+    return this.verifyTokens(tokens);
   }
 
   private verifyTokens(tokens: Token[]): string[] {
@@ -71,6 +39,8 @@ export class LogicalExpressionParser {
     let wasOperator = false;
     let wasVariable = false;
     let wasClose = false;
+    let wasOpen = false;
+    let wasNegate = false;
 
     if (tokens.length > 0) {
       switch (tokens[0].name) {
@@ -94,8 +64,19 @@ export class LogicalExpressionParser {
         case TokenName.and:
           if (wasOperator)
             errors.push("Two operators (AND/OR) can't be next to each other");
+          if (wasOpen)
+            errors.push(
+              `Operator '${token.lexeme}' can't be after an opening parenthesis`
+            );
+          break;
+        case TokenName.negate:
+          if (wasClose)
+            errors.push(
+              `Negation '${token.lexeme}' is after a closing parenthesis`
+            );
+          if (wasVariable)
+            errors.push(`Negation '${token.lexeme}' is after a variable`);
           break;
-        case TokenName.negatedVariable:
         case TokenName.variable:
           if (wasVariable)
             errors.push(
@@ -110,184 +91,23 @@ export class LogicalExpressionParser {
           if (wasVariable)
             errors.push("Parenthesis can't be opened after a variable");
           break;
+        case TokenName.close:
+          if (wasOperator)
+            errors.push(
+              "Parenthesis can't be closed after an operator (AND/OR)"
+            );
+          if (wasNegate)
+            errors.push("Parenthesis can't be closed after a negation");
+          break;
       }
 
       wasOperator = token.name == TokenName.and || token.name == TokenName.or;
-      wasVariable =
-        token.name == TokenName.variable ||
-        token.name == TokenName.negatedVariable;
+      wasVariable = token.name == TokenName.variable;
+      wasOpen = token.name == TokenName.open;
       wasClose = token.name == TokenName.close;
+      wasNegate = token.name == TokenName.negate;
     }
 
     return errors;
   }
-  /**
-   * Converts any negative variable's negative prefix
-   * Converts all variables to numbers
-   * @param tokens {Token[]} array of tokens to search for variables
-   * @returns {Map<string, number>} variables mapped to their number representation
-   */
-  private convertVariables(tokens: Token[]): Map<string, number> {
-    let variables = new Map<string, number>();
-    const addToMap = (str: string): number => {
-      let number = variables.get(str);
-      if (number == undefined) {
-        number = variables.size + 1;
-        variables.set(str, number);
-      }
-
-      return number;
-    };
-
-    for (let i = 0; i < tokens.length; i++) {
-      switch (tokens[i].name) {
-        case TokenName.variable:
-          tokens[i].lexeme = addToMap(tokens[i].lexeme).toString();
-          break;
-        case TokenName.negatedVariable:
-          let negTokens = this.lexNegation.tokenize(tokens[i].lexeme);
-          if (negTokens.length != 2)
-            throw new Error(
-              "Can't parse negated variables that don't have two tokens"
-            );
-
-          let negToken = negTokens[1] as Token;
-          let varNumber = addToMap(negToken.lexeme);
-
-          //Replace negated variable with dimacs negative variable syntax
-          negToken.lexeme = `-${varNumber}`;
-          tokens[i] = negToken;
-          break;
-      }
-    }
-
-    return variables;
-  }
-
-  private getLeveledTokens(tokens: Token[]): LeveledToken[] {
-    let leveledTokens: LeveledToken[] = [];
-    let curLevel = 0;
-
-    for (let token of tokens) {
-      switch (token.name) {
-        case TokenName.open:
-          curLevel++;
-          break;
-        case TokenName.close:
-          curLevel--;
-          break;
-        default:
-          leveledTokens.push({ token: token, level: curLevel });
-          break;
-      }
-    }
-
-    return leveledTokens;
-  }
-
-  private parseFormula(tokens: Token[]) {
-    let leveledTokens = this.getLeveledTokens(tokens);
-
-    //Start recursive parsing of formula starting with or
-    this.processOR(leveledTokens);
-  }
-
-  private getOperatorPositions(
-    tokens: LeveledToken[],
-    operator: string,
-    level: number
-  ): number[] {
-    let positions: number[] = [];
-    for (let i = 0; i < tokens.length; i++) {
-      let token = tokens[i];
-      switch (token.token.name) {
-        case operator:
-          if (token.level == level) positions.push(i);
-          break;
-        default:
-          break;
-      }
-    }
-
-    //Always add token length
-    positions.push(tokens.length);
-
-    return positions;
-  }
-
-  private getMinLevel(tokens: LeveledToken[]): number {
-    let minLevel = undefined;
-
-    for (const token of tokens) {
-      if (minLevel == undefined || token.level < minLevel) {
-        minLevel = token.level;
-      }
-    }
-
-    return minLevel ?? -1;
-  }
-
-  private processAND(tokens: LeveledToken[]): LeveledToken[] {
-    if (tokens.length < 2) {
-      this.output += ` ${tokens[0].token.lexeme} `;
-      return tokens;
-    }
-
-    let level = this.getMinLevel(tokens);
-    let operatorPositions = this.getOperatorPositions(
-      tokens,
-      TokenName.and,
-      level
-    );
-    if (operatorPositions.length == 1) return this.processOR(tokens);
-
-    let returnTokens: LeveledToken[] = [];
-    let lastOr = -1;
-
-    this.output += `*(`;
-    for (let pos of operatorPositions) {
-      let before = tokens.slice(lastOr + 1, pos);
-      lastOr = pos;
-
-      let processedBefore = this.processOR(before);
-      returnTokens.push(...processedBefore);
-    }
-    this.output += `)`;
-
-    return returnTokens;
-  }
-
-  private processOR(tokens: LeveledToken[]): LeveledToken[] {
-    if (tokens.length < 2) {
-      this.output += ` ${tokens[0].token.lexeme} `;
-      return tokens;
-    }
-
-    let level = this.getMinLevel(tokens);
-    let operatorPositions = this.getOperatorPositions(
-      tokens,
-      TokenName.or,
-      level
-    );
-    if (operatorPositions.length == 1) return this.processAND(tokens);
-
-    let returnTokens: LeveledToken[] = [];
-    let lastOr = -1;
-
-    if (operatorPositions.length > 1) this.output += `+(`;
-    for (let pos of operatorPositions) {
-      let before = tokens.slice(lastOr + 1, pos);
-      lastOr = pos;
-
-      //Start processing nested expressions with OR
-      let processedBefore =
-        before[0].level != level
-          ? this.processOR(before)
-          : this.processAND(before);
-      returnTokens.push(...processedBefore);
-    }
-    if (operatorPositions.length > 1) this.output += `)`;
-
-    return returnTokens;
-  }
 }
diff --git a/src/converter/dimacs/Syntax/CommonSyntax.ts b/src/converter/dimacs/Syntax/CommonSyntax.ts
index 50cd601..83f872d 100644
--- a/src/converter/dimacs/Syntax/CommonSyntax.ts
+++ b/src/converter/dimacs/Syntax/CommonSyntax.ts
@@ -7,12 +7,10 @@ export enum TokenName {
   open = "open",
   close = "close",
   variable = "variable",
-  negatedVariable = "negatedVariable",
   variableAssignment = "=>",
 }
 
-export const variableRegexPart = "(?:[A-z]|\\d)+";
-export const regexVariable = new RegExp(variableRegexPart);
+export const regexVariable = /(?:[A-z]|\d)+/;
 export const regexBlank = /\s+/g;
 
 export const variableRule = new Rule({
diff --git a/src/converter/dimacs/Syntax/LogicalExpressionSyntax.ts b/src/converter/dimacs/Syntax/LogicalExpressionSyntax.ts
index e600194..ead78af 100644
--- a/src/converter/dimacs/Syntax/LogicalExpressionSyntax.ts
+++ b/src/converter/dimacs/Syntax/LogicalExpressionSyntax.ts
@@ -1,25 +1,15 @@
 import { Rule } from "@jlguenego/lexer";
-import { TokenName, variableRegexPart } from "./CommonSyntax";
+import { TokenName } from "./CommonSyntax";
 
-export const negateRegexPart = "(?:(?:not|NOT)\\s+|(?:!\\s*))";
-
-export const regexAND = /(?:&|and|AND) /;
-export const regexOR = /(?:\||or|OR) /;
-export const regexNOT = new RegExp(negateRegexPart, "g");
-export const regexNOTVariable = new RegExp(
-  `${negateRegexPart}\\s*${variableRegexPart}`
-);
+export const regexAND = /(?:&|and|AND)\b/;
+export const regexOR = /(?:\||or|OR)\b/;
+export const regexNOT = /not|NOT|!/g;
 
 export const negateRule = new Rule({
   name: TokenName.negate,
   pattern: regexNOT,
 });
 
-export const negatedVariableRule = new Rule({
-  name: TokenName.negatedVariable,
-  pattern: regexNOTVariable,
-});
-
 export const andRule = new Rule({
   name: TokenName.and,
   pattern: regexAND,
diff --git a/src/pages/solve/FeatureModelAnomaly.tsx b/src/pages/solve/FeatureModelAnomaly.tsx
index a803d78..cf35292 100644
--- a/src/pages/solve/FeatureModelAnomaly.tsx
+++ b/src/pages/solve/FeatureModelAnomaly.tsx
@@ -2,19 +2,17 @@ import {
   Box,
   Divider,
   Heading,
-  List,
   ListItem,
-  Spacer,
   Text,
   UnorderedList,
   VStack,
 } from "@chakra-ui/react";
 import { NextPage } from "next";
-import React, { useState } from "react";
+import { useState } from "react";
 import { MultiSelect, Option } from "react-multi-select-component";
+import { Layout } from "../../components/layout/Layout";
 import { ProgressHandler } from "../../components/solvers/ProgressHandler";
 import { TextInputMask } from "../../components/solvers/TextInputMask";
-import { Layout } from "../../components/layout/Layout";
 
 const anomalies: Option[] = [
   {
@@ -53,8 +51,9 @@ const FeatureModelAnomaly: NextPage = () => {
       </UnorderedList>
 
       <TextInputMask
-        textPlaceholder="Enter your feature model in UVL format"
+        text={uvl}
         onTextChanged={setUvl}
+        textPlaceholder="Enter your feature model in UVL format"
         body={
           <VStack>
             <Box width="300px">
@@ -71,6 +70,7 @@ const FeatureModelAnomaly: NextPage = () => {
             <ProgressHandler
               problemTypes={selectedAnomalies.map((option) => option.value)}
               problemInput={uvl}
+              setProblemInput={setUvl}
             />
           </VStack>
         }
diff --git a/src/pages/solve/MaxCut.tsx b/src/pages/solve/MaxCut.tsx
index 28c3be5..d3ca04c 100644
--- a/src/pages/solve/MaxCut.tsx
+++ b/src/pages/solve/MaxCut.tsx
@@ -8,13 +8,13 @@ import {
   Text,
 } from "@chakra-ui/react";
 import { NextPage } from "next";
-import React, { useState } from "react";
+import { useState } from "react";
 import { Container } from "../../components/Container";
+import { Layout } from "../../components/layout/Layout";
 import { GraphArea } from "../../components/solvers/Graph/GraphArea";
 import { ProgressHandler } from "../../components/solvers/ProgressHandler";
 import { TextInputMask } from "../../components/solvers/TextInputMask";
 import { parseGML } from "../../converter/graph/gml/GmlParser";
-import { Layout } from "../../components/layout/Layout";
 
 const MaxCut: NextPage = () => {
   const [graphData, setGraphData] = useState<any>(null);
@@ -47,6 +47,7 @@ const MaxCut: NextPage = () => {
 
       <TextInputMask
         textPlaceholder="Enter your graph in GML format"
+        text={graphString}
         onTextChanged={change}
         body={
           <Container>
@@ -62,6 +63,7 @@ const MaxCut: NextPage = () => {
             <ProgressHandler
               problemTypes={["max-cut"]}
               problemInput={graphString}
+              setProblemInput={change}
             />
           </Container>
         }
diff --git a/src/pages/solve/SAT.tsx b/src/pages/solve/SAT.tsx
index 09d977a..230a21e 100644
--- a/src/pages/solve/SAT.tsx
+++ b/src/pages/solve/SAT.tsx
@@ -4,7 +4,6 @@ import type { NextPage } from "next";
 import { TextArea } from "../../components/solvers/SAT/TextArea";
 import { ProgressHandler } from "../../components/solvers/ProgressHandler";
 import { Text, Divider, Heading, Spacer } from "@chakra-ui/react";
-import { DimacsParser } from "../../converter/dimacs/DimacsParser";
 import { LogicalExpressionParser } from "../../converter/dimacs/LogicalExpressionParser";
 import { Layout } from "../../components/layout/Layout";
 import { EditorControls } from "../../components/solvers/EditorControls";
@@ -16,6 +15,20 @@ const SAT: NextPage = () => {
   const [logicalExpressionString, setLogicalExpressionString] = useState("");
   const [errorString, setErrorString] = useState("");
 
+  function updateProblemString(newValue: string) {
+    setLogicalExpressionString(newValue);
+
+    let errors = logicalExpressionParser.validateLogicalExpression(
+      newValue.toString()
+    );
+
+    if (errors.length > 0) {
+      setErrorString(errors.toString());
+    } else {
+      setErrorString("");
+    }
+  }
+
   return (
     <Layout>
       <Head>
@@ -44,21 +57,13 @@ const SAT: NextPage = () => {
       />
       <TextArea
         problemString={logicalExpressionString}
-        setProblemString={(value) => {
-          setLogicalExpressionString(value);
-
-          try {
-            logicalExpressionParser.parseDimacs(value.toString());
-            setErrorString("");
-          } catch (e: any) {
-            setErrorString(e.message);
-          }
-        }}
+        setProblemString={updateProblemString}
       />
       <Divider />
       <ProgressHandler
         problemTypes={["sat"]}
         problemInput={logicalExpressionString}
+        setProblemInput={updateProblemString}
       />
     </Layout>
   );