blob: 83d335ab8b529e0d8d3a71d2d0e41dc79c4a665d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
