diff --git a/Trees/SAT_Tseitin.ipynb b/Trees/SAT_Tseitin.ipynb index fc279b8..aad361f 100644 --- a/Trees/SAT_Tseitin.ipynb +++ b/Trees/SAT_Tseitin.ipynb @@ -4,7 +4,7 @@ "metadata": { "colab": { "provenance": [], - "authorship_tag": "ABX9TyO30jtLgfo4lSQLEOV3NJw3", + "authorship_tag": "ABX9TyMFurTLUbk5qbN9tTBjrI+h", "include_colab_link": true }, "kernelspec": { @@ -40,7 +40,7 @@ "source": [ "# The Tseitin transformation\n", "\n", - "The purpose of this Python notebook is to check that the Tseitin transformation example in the text is correct. Once we have the formula in conjunctive normal form, we can use the Python SAT library Z3 to solve SAT problems.\n", + "The purpose of this Python notebook is to check that the Tseitin transformation example in the text is correct. \n", "\n", "Work through the cells below, running each cell in turn. In various places you will see the words \"TODO\". Follow the instructions at these places and write code to complete the functions.\n", "\n",