From f88127c0d2b192f776d03cd40b3aa9e6a8257ac0 Mon Sep 17 00:00:00 2001 From: udlbook <110402648+udlbook@users.noreply.github.com> Date: Thu, 27 Mar 2025 17:56:09 -0400 Subject: [PATCH] Created using Colab --- Trees/SAT_Tseitin.ipynb | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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",