Conjunctive Normal Form to Conjunctive XOR-based form

cnf_to_xnf.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from typing import List\n",
    "from IPython.display import display, Math"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Variable(object):\n",
    "    def __init__(self, index, inv=False):\n",
    "        self.index: int = index\n",
    "        self.inv: bool = inv\n",
    "\n",
    "    def __str__(self) -> str:\n",
    "        return f\"x{self.index}\" + (\"'\" if self.inv else \"\")\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return str(self)\n",
    "\n",
    "    def to_latex(self) -> str:\n",
    "        if self.inv:\n",
    "            return f\"\\overline{{x_{self.index}}}\"\n",
    "        else:\n",
    "            return f\"x_{self.index}\"\n",
    "\n",
    "class Disjunction(list):\n",
    "    def __str__(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" + \".join([el.to_latex() for el in self])\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return str(self)\n",
    "\n",
    "    def to_latex(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" \\lor \".join([el.to_latex() for el in self])\n",
    "\n",
    "class ExclusiveDisjunction(list):\n",
    "    def __str__(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" ^ \".join([el.to_latex() for el in self])\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return str(self)\n",
    "\n",
    "    def to_latex(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" \\oplus \".join([el.to_latex() for el in self])\n",
    "\n",
    "\n",
    "class Conjunction(list):\n",
    "    def __str__(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" * \".join([el.to_latex() for el in self])\n",
    "\n",
    "    def __repr__(self) -> str:\n",
    "        return str(self)\n",
    "\n",
    "\n",
    "    def to_latex(self) -> str:\n",
    "        if len(self) == 1:\n",
    "            return str(self[0])\n",
    "        return \"(%s)\" % \" \\land \".join([el.to_latex() for el in self])\n",
    "\n",
    "class CNF(Conjunction):\n",
    "    def __init__(self, clauses: List[List[Variable]]):\n",
    "        super().__init__()\n",
    "        for clause in clauses:\n",
    "            self.append(Disjunction(clause))\n",
    "\n",
    "V = Variable"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle ((x_0 \\lor x_1 \\lor \\overline{x_2}) \\land (x_0 \\lor \\overline{x_1} \\lor x_2))$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "cnf = CNF([\n",
    "    [V(0), V(1), V(2, inv=True)],\n",
    "    [V(0), V(1, inv=True), V(2)]\n",
    "])\n",
    "\n",
    "display(Math(cnf.to_latex()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle (((x_0 \\oplus x_1 \\oplus (x_0 \\land x_1)) \\oplus \\overline{x_2} \\oplus ((x_0 \\oplus x_1 \\oplus (x_0 \\land x_1)) \\land \\overline{x_2})) \\land ((x_0 \\oplus \\overline{x_1} \\oplus (x_0 \\land \\overline{x_1})) \\oplus x_2 \\oplus ((x_0 \\oplus \\overline{x_1} \\oplus (x_0 \\land \\overline{x_1})) \\land x_2)))$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "def dj_to_xdj(disj: Disjunction):\n",
    "    mut = disj.copy()\n",
    "    while len(mut) > 1:\n",
    "        xdj = ExclusiveDisjunction()\n",
    "        xdj.append(mut[0])\n",
    "        xdj.append(mut[1])\n",
    "        xdj.append(Conjunction([mut[0], mut[1]]))\n",
    "        mut = [xdj] + mut[2:]\n",
    "    return mut[0]\n",
    "\n",
    "dj_to_xdj(Disjunction([V(0), V(1), V(2)]))\n",
    "\n",
    "def cnf_to_cxf(cnf: CNF):\n",
    "    cxf = Conjunction()\n",
    "    for disjunction in cnf:\n",
    "        cxf.append(dj_to_xdj(disjunction))\n",
    "    return cxf\n",
    "\n",
    "\n",
    "display(Math(cnf_to_cxf(cnf).to_latex()))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3.10.6 64-bit",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.6"
  },
  "orig_nbformat": 4,
  "vscode": {
   "interpreter": {
    "hash": "e7370f93d1d0cde622a1f8e1c04877d8463912d04d973331ad4851f04de6915a"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}