+++
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.