Add content

1 files changed, 25 insertions, 0 deletions

diff --git a/content/zettel/2d2.md b/content/zettel/2d2.md
new file mode 100644
index 0000000..83d335a
--- /dev/null
+++ b/content/zettel/2d2.md
@@ -0,0 +1,25 @@
++++
+title = "Davis–Putnam–Logemann–Loveland (DPLL) algorithm"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2d1"]
+forwardlinks = ["2d3"]
+zettelid = "2d2"
++++
+
+This is a backtracking algorithm that is used to solve SAT problems, and
+is still used in the most efficient SAT solvers. The two main rules of
+reduction are the following:
+
+Unit propagation
+:   This consists of removing every clause that contains a unit clause's
+    literal and discarding the complement of the unit clause's literal.
+    This can be repeated for a large reduction in the formula.
+
+Pure literal elimination
+:   If a pure propositional variable (one where it's complement is not
+    present anywhere in the formula), is present in a clause, this
+    clause can also be removed as it can trivially be set to true using
+    the pure variable. It is therefore not a constraint on the
+    satisfiability of the system.