dr_domi/udlbook
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Created using Colab

Browse Source
This commit is contained in:
udlbook
2025-03-27 17:56:09 -04:00
parent a637eec888
commit f88127c0d2
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Trees/SAT_Tseitin.ipynb
View File

@@ -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",