Skip to content

Instantly share code, notes, and snippets.

@buhii

buhii/DPLL.ipynb

Created January 10, 2021 13:51
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save buhii/cb99b67127cea0504289788227cb13cf to your computer and use it in GitHub Desktop.
Save buhii/cb99b67127cea0504289788227cb13cf to your computer and use it in GitHub Desktop.
Download ZIP
DPLL.ipynb
Display the source blob
Display the rendered blob
Raw
DPLL.ipynb
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[¬x1, x3, x5]\n",
"[ x1]\n",
"True\n"
]
}
],
"source": [
"class Lit:\n",
" def __init__(self, lit):\n",
" assert lit != 0, \"lit is 0\"\n",
" self.lit = lit\n",
"\n",
" def is_not(self):\n",
" return self.lit < 0\n",
" \n",
" def __abs__(self):\n",
" return abs(self.lit)\n",
"\n",
" def __repr__(self):\n",
" op_not = \"¬\" if self.lit < 0 else \" \"\n",
" return f\"{op_not}x{abs(self.lit)}\"\n",
" \n",
" def __neg__(self):\n",
" return Lit(-self.lit)\n",
"\n",
"\n",
"print([Lit(-1), Lit(3), Lit(5)])\n",
"print([-Lit(-1)])\n",
"print(Lit(-1).is_not())"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(1, False)\n",
"None\n",
"None\n",
"(1, False)\n",
"None\n",
"(3, True)\n"
]
}
],
"source": [
"class Clause:\n",
" \n",
" UNKNOWN = \"unknown\"\n",
" \n",
" def __init__(self, lits):\n",
" self.lits = lits\n",
" \n",
" def __repr__(self):\n",
" return \"( \" + \" ∨ \".join(map(str, self.lits)) + \" )\"\n",
" \n",
" def assign(self, assignments):\n",
" for lit in self.lits:\n",
" v = abs(lit)\n",
" if v not in assignments:\n",
" return self.UNKNOWN\n",
"\n",
" b = assignments[v]\n",
" if lit.is_not():\n",
" b = not b\n",
" \n",
" if b:\n",
" return True\n",
" return False\n",
"\n",
" def unit_propagate(self, assignments):\n",
" unknown_lit = None\n",
" \n",
" for lit in self.lits:\n",
" v = abs(lit)\n",
" if v in assignments: \n",
" b = assignments[v]\n",
" if lit.is_not():\n",
" b = not b\n",
" if b:\n",
" # Because clause is True, unit_propagate is impossible\n",
" return None\n",
" else:\n",
" if unknown_lit is not None:\n",
" # Because multiple unknown literals exist, unit_propagate is impossible\n",
" return None\n",
" unknown_lit = lit\n",
"\n",
" if unknown_lit is None:\n",
" return\n",
"\n",
" return abs(unknown_lit), not unknown_lit.is_not()\n",
"\n",
"\n",
"print(Clause([Lit(-1)]).unit_propagate({}))\n",
"print(Clause([Lit(-1), Lit(2)]).unit_propagate({}))\n",
"print(Clause([Lit(-1), Lit(2)]).unit_propagate({1: False}))\n",
"print(Clause([Lit(-1), Lit(2)]).unit_propagate({2: False}))\n",
"print(Clause([Lit(-1), Lit(2)]).unit_propagate({2: False, 1: True}))\n",
"print(Clause([Lit(-1), Lit(-2), Lit(3)]).unit_propagate({2: True, 1: True}))"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"variables: ['x1', 'x2', 'x3']\n",
"( x1 ∨ ¬x3 ) ∧\n",
"( x2 ∨ x3 ∨ ¬x1 )\n",
"('sat', {1: True, 2: True})\n"
]
}
],
"source": [
"class Solver(object):\n",
" \n",
" SAT = \"sat\"\n",
" UNSAT = \"unsat\"\n",
" \n",
" def __init__(self, clauses):\n",
" self.clauses = clauses\n",
"\n",
" variables = set()\n",
" for clause in self.clauses:\n",
" for lit in clause.lits:\n",
" variables.add(abs(lit))\n",
" self.variables = variables\n",
" \n",
" def __repr__(self):\n",
" return \" ∧\\n\".join(map(str, self.clauses))\n",
"\n",
" @classmethod\n",
" def read_dimacs(cls, text):\n",
" clauses = []\n",
" \n",
" for i, line in enumerate(text.splitlines()):\n",
" if not line:\n",
" continue\n",
" if line.startswith(\"c\"):\n",
" # comment line\n",
" continue\n",
" if line.startswith(\"p\"):\n",
" # TODO: check the problem type, the number of variables and the number of clauses\n",
" # p cnf 3 2\n",
" continue\n",
" if not line.endswith(\"0\"):\n",
" raise ValueError(f\"Invalid DIMACS format at line {i + 1}: \\\"{line}\\\"\")\n",
" lits = [Lit(int(l)) for l in line[:-1].split()]\n",
" clauses.append(Clause(lits))\n",
"\n",
" return cls(clauses)\n",
"\n",
" def solve(self):\n",
" return self.DPLL()\n",
" \n",
" def DPLL(self, implications={}, decisions={}):\n",
" \n",
" def bcp():\n",
" for clause in self.clauses:\n",
" result = clause.unit_propagate(implications | decisions)\n",
" if result is not None:\n",
" implications[result[0]] = result[1]\n",
" return True\n",
" return False\n",
" \n",
" def get_unassigned():\n",
" assigned = set((implications | decisions).keys())\n",
" return list(self.variables - assigned)\n",
" \n",
" def evaluate(assignments):\n",
" for clause in self.clauses:\n",
" result = clause.assign(assignments)\n",
" if result == Clause.UNKNOWN:\n",
" return Clause.UNKNOWN\n",
" if not result:\n",
" return False\n",
" return True\n",
" \n",
" def decide():\n",
" val = get_unassigned()[0]\n",
" return val\n",
"\n",
" while bcp():\n",
" pass\n",
"\n",
" result = evaluate(implications | decisions)\n",
" \n",
" if result == True:\n",
" return solver.SAT, implications | decisions\n",
"\n",
" if result == False:\n",
" pass\n",
" \n",
" if result == Clause.UNKNOWN:\n",
" val = decide()\n",
" \n",
" vt = self.DPLL(implications | {}, decisions | {val: True})\n",
" if vt is not None and vt[0] == solver.SAT:\n",
" return vt\n",
" vf = self.DPLL(implications | {}, decisions | {val: False})\n",
" if vf is not None and vf[0] == solver.SAT:\n",
" return vf\n",
" \n",
"\n",
"solver = Solver.read_dimacs(\"\"\"\n",
"1 -3 0\n",
"2 3 -1 0\n",
"\"\"\")\n",
"print(\"variables:\", [f\"x{v}\" for v in sorted(solver.variables)])\n",
"print(solver)\n",
"print(solver.solve())"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"variables: ['x1', 'x2', 'x3', 'x4', 'x5', 'x6', 'x7', 'x8']\n",
"( ¬x1 ∨ ¬x2 ∨ ¬x3 ) ∧\n",
"( ¬x1 ∨ ¬x4 ∨ ¬x5 ) ∧\n",
"( ¬x2 ∨ x3 ∨ x7 ∨ ¬x8 ) ∧\n",
"( ¬x1 ∨ ¬x6 ∨ ¬x5 ∨ x8 ) ∧\n",
"( ¬x4 ∨ ¬x7 ∨ x8 ) ∧\n",
"( ¬x2 ∨ ¬x4 ∨ ¬x6 ) ∧\n",
"( ¬x1 ∨ ¬x3 ∨ ¬x5 ∨ ¬x7 )\n",
"('sat', {3: False, 5: False, 6: False, 7: True, 1: True, 2: True, 4: True, 8: True})\n"
]
}
],
"source": [
"solver = Solver.read_dimacs(\"\"\"\n",
"-1 -2 -3 0\n",
"-1 -4 -5 0\n",
"-2 3 7 -8 0\n",
"-1 -6 -5 8 0\n",
"-4 -7 8 0\n",
"-2 -4 -6 0\n",
"-1 -3 -5 -7 0\n",
"\"\"\")\n",
"print(\"variables:\", [f\"x{v}\" for v in sorted(solver.variables)])\n",
"print(solver)\n",
"print(solver.solve())"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"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.9.1"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment