DPLL algorithm - Revision history

JamesHDavenport: /* References */ DLL is 1962 in Comm ACM, not 1961

2025-02-21T23:35:34Z

References: DLL is 1962 in Comm ACM, not 1961

← Previous revision		Revision as of 23:35, 21 February 2025
Line 187:		Line 187:
	\| issue=7		\| issue=7
	\| pages = 394–397		\| pages = 394–397
	\| year=~~1961~~		\| year=1962
	\| url=https://archive.org/details/machineprogramfo00davi		\| url=https://archive.org/details/machineprogramfo00davi
	\| doi=10.1145/368273.368557\| hdl=2027/mdp.39015095248095		\| doi=10.1145/368273.368557\| hdl=2027/mdp.39015095248095

Zontasticality: fix grammar mistake

2025-02-19T18:20:35Z

fix grammar mistake

← Previous revision		Revision as of 18:20, 19 February 2025
Line 69:		Line 69:

	=== Formalization ===		=== Formalization ===
	The [[sequent calculus]]-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.<ref>{{Cite journal \|last=Nieuwenhuis \|first=Robert \|last2=Oliveras \|first2=Albert \|last3=Tinelli \|first3=Cesare \|date=2006-11-01 \|title=Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T) \|url=https://dl.acm.org/doi/10.1145/1217856.1217859 \|journal=J. ACM \|volume=53 \|issue=6 \|pages=937–977 \|doi=10.1145/1217856.1217859 \|issn=0004-5411}}</ref><ref>{{Cite journal \|last=Krstić \|first=Sava \|last2=Goel \|first2=Amit \|date=2007 \|editor-last=Konev \|editor-first=Boris \|editor2-last=Wolter \|editor2-first=Frank \|title=Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL \|url=https://link.springer.com/chapter/10.1007/978-3-540-74621-8_1 \|journal=Frontiers of Combining Systems \|language=en \|location=Berlin, Heidelberg \|publisher=Springer \|pages=1–27 \|doi=10.1007/978-3-540-74621-8_1 \|isbn=978-3-540-74621-8}}</ref>		The [[sequent calculus]]-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail to find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.<ref>{{Cite journal \|last=Nieuwenhuis \|first=Robert \|last2=Oliveras \|first2=Albert \|last3=Tinelli \|first3=Cesare \|date=2006-11-01 \|title=Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T) \|url=https://dl.acm.org/doi/10.1145/1217856.1217859 \|journal=J. ACM \|volume=53 \|issue=6 \|pages=937–977 \|doi=10.1145/1217856.1217859 \|issn=0004-5411}}</ref><ref>{{Cite journal \|last=Krstić \|first=Sava \|last2=Goel \|first2=Amit \|date=2007 \|editor-last=Konev \|editor-first=Boris \|editor2-last=Wolter \|editor2-first=Frank \|title=Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL \|url=https://link.springer.com/chapter/10.1007/978-3-540-74621-8_1 \|journal=Frontiers of Combining Systems \|language=en \|location=Berlin, Heidelberg \|publisher=Springer \|pages=1–27 \|doi=10.1007/978-3-540-74621-8_1 \|isbn=978-3-540-74621-8}}</ref>

	If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{		If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{

Zontasticality: add relevant citations for sequent calculus rules

2025-02-18T18:30:13Z

add relevant citations for sequent calculus rules

← Previous revision		Revision as of 18:30, 18 February 2025
Line 69:		Line 69:

	=== Formalization ===		=== Formalization ===
	The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.{{cn\|date=~~February~~ ~~2025~~}}		The [[sequent calculus]]-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.<ref>{{Cite journal \|last=Nieuwenhuis \|first=Robert \|last2=Oliveras \|first2=Albert \|last3=Tinelli \|first3=Cesare \|date=2006-11-01 \|title=Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T) \|url=https://dl.acm.org/doi/10.1145/1217856.1217859 \|journal=J. ACM \|volume=53 \|issue=6 \|pages=937–977 \|doi=10.1145/1217856.1217859 \|issn=0004-5411}}</ref><ref>{{Cite journal \|last=Krstić \|first=Sava \|last2=Goel \|first2=Amit \|date=2007 \|editor-last=Konev \|editor-first=Boris \|editor2-last=Wolter \|editor2-first=Frank \|title=Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL \|url=https://link.springer.com/chapter/10.1007/978-3-540-74621-8_1 \|journal=Frontiers of Combining Systems \|language=en \|location=Berlin, Heidelberg \|publisher=Springer \|pages=1–27 \|doi=10.1007/978-3-540-74621-8_1 \|isbn=978-3-540-74621-8}}</ref>

	If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{		If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{

AnomieBOT: Dating maintenance tags: {{Cn}}

2025-02-17T20:34:07Z

Dating maintenance tags: {{Cn}}

← Previous revision		Revision as of 20:34, 17 February 2025
Line 69:		Line 69:

	=== Formalization ===		=== Formalization ===
	The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.{{cn}}		The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.{{cn\|date=February 2025}}

	If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{		If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{

Jochen Burghardt: /* Formalization */

2025-02-17T20:13:41Z

Formalization

← Previous revision		Revision as of 20:13, 17 February 2025
Line 69:		Line 69:

	=== Formalization ===		=== Formalization ===
	The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.		The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.{{cn}}

	If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{		If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{

Zontasticality: add section for sequent calculus formalization

2025-02-17T16:13:23Z

add section for sequent calculus formalization

← Previous revision		Revision as of 16:13, 17 February 2025
Line 67:		Line 67:

	The Davis–Logemann–Loveland algorithm depends on the choice of ''branching literal'', which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals. Such choice functions are also called [[heuristic function]]s or branching heuristics.<ref>{{Cite book \| last1 = Marques-Silva \| first1 = João P.\| chapter = The Impact of Branching Heuristics in Propositional Satisfiability Algorithms \| doi = 10.1007/3-540-48159-1_5 \| title = Progress in Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Évora, Portugal, September 21–24, 1999 Proceedings \| editor1-first = Pedro \| editor1-last = Barahona \| editor2-first = José J. \| editor2-last = Alferes\| series = [[Lecture Notes in Computer Science\|LNCS]] \| volume = 1695 \| pages = 62–63 \| year = 1999 \| isbn = 978-3-540-66548-9 }}</ref>		The Davis–Logemann–Loveland algorithm depends on the choice of ''branching literal'', which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals. Such choice functions are also called [[heuristic function]]s or branching heuristics.<ref>{{Cite book \| last1 = Marques-Silva \| first1 = João P.\| chapter = The Impact of Branching Heuristics in Propositional Satisfiability Algorithms \| doi = 10.1007/3-540-48159-1_5 \| title = Progress in Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Évora, Portugal, September 21–24, 1999 Proceedings \| editor1-first = Pedro \| editor1-last = Barahona \| editor2-first = José J. \| editor2-last = Alferes\| series = [[Lecture Notes in Computer Science\|LNCS]] \| volume = 1695 \| pages = 62–63 \| year = 1999 \| isbn = 978-3-540-66548-9 }}</ref>

			=== Formalization ===
			The [[sequent calculus]] can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail or find a satisfying assignment, i.e. <math>A = (l_1, \neg l_2, l_3, ...)</math>.

			If a clause in the formula <math>\Phi</math> has exactly one unassigned literal <math>l</math> in <math>A</math>, with all other literals in the clause appearing negatively, extend <math>A</math> with <math>l</math>. ''This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.''<math display="block">\frac{
			\begin{array}{c}
			\{l_1, \dots, l_n, l\} \in \Phi \;\;\;
			\neg l_1, \dots, \neg l_n \in A \;\;\;\;\;
			l, \neg l \notin A
			\end{array}
			}{
			A := A \; l
			} \text{ (Propagate)}</math>If a literal <math>l</math> appears in the formula <math>\Phi</math> but its negation <math>\neg l</math> does not, and <math>l</math> and <math>\neg l</math> are not in <math>A</math>, extend <math>A</math> with <math>l</math>. ''This rule represents the idea that if a variable appears only purely positively or purely negatively in a formula, all the instances can be set to true or false to make their corresponding clauses true.''<math display="block">\frac{
			\begin{array}{c}
			l \text{ literal of } \Phi \;\;\;
			\neg l \text{ not literal of } \Phi \;\;\;\;\;
			l, \neg l \notin A
			\end{array}
			}{
			A := A \; l
			} \text{ (Pure)}</math>If a literal <math>l</math> is in the set of literals of <math>\Phi</math> and neither <math>l</math> nor <math>\neg l</math> is in <math>A</math>, then decide on the truth value of <math>l</math> and extend <math>A</math> with the decision literal <math>\bullet l</math>. ''This rule represents the idea that if you aren't forced to do an assignment, you must choose a variable to assign and make note which assignment was a choice so you can go back if the choice didn't result in a satisfying assignment.''<math display="block">\frac{
			\begin{array}{c}
			l \in \text{Lits}(\Phi) \;\;\;
			l, \neg l \notin A
			\end{array}
			}{
			A := A \;\bullet\; l
			} \text{ (Decide)}</math>If a clause <math>\{l_1, \dots, l_n\}</math> is in <math>\Phi</math>, and their negations <math>\neg l_1, \dots, \neg l_n</math> are in <math>A</math>, and <math>A</math> can be represented as <math>A = A' \;\bullet\; l \; N</math> where <math>\bullet \notin N</math>, then backtrack by setting <math>A</math> to <math>A' \; \neg l</math>. ''This rule represents the idea that if you reach a contradiction in trying to find a valid assignment, you need to go back to where you previously did a decision between two assignments and pick the other one.''<math display="block">\frac{
			\begin{array}{c}
			\{l_1, \dots, l_n\} \in \Phi \;\;\;
			\neg l_1, \dots, \neg l_n \in A \;\;\;\;\;
			A = A' \;\bullet\; l \; N \;\;\;\;\;
			\bullet \notin N
			\end{array}
			}{
			A := A' \; \neg l
			} \text{ (Backtrack)}</math>If a clause <math>\{l_1, \dots, l_n\}</math> is in <math>\Phi</math>, and their negations <math>\neg l_1, \dots, \neg l_n</math> are in <math>A</math>, and there is no conflict marker <math>\bullet</math> in <math>A</math>, then the DPLL algorithm fails. ''This rule represents the idea that if you reach a contradiction but there wasn't anything you could have done differently on the way there, the formula is unsatisfiable.''<math display="block">\frac{
			\begin{array}{c}
			\{l_1, \dots, l_n\} \in \Phi \;\;\;
			\neg l_1, \dots, \neg l_n \in A \;\;\;\;\;
			\bullet \notin A
			\end{array}
			}{
			\text{Fail}
			} \text{ (Fail)}</math>

	===Visualization===		===Visualization===

Jochen Burghardt: /* References */ now in side tab

2025-02-03T08:39:38Z

References: now in side tab

← Previous revision		Revision as of 08:39, 3 February 2025
Line 119:		Line 119:

	==References==		==References==
	{{commons category\|Davis-Putnam-Logemann-Loveland algorithm}}
	'''General'''		'''General'''
	* {{cite journal		* {{cite journal

Cedar101: /* Visualization */ set perrow

2025-02-02T15:27:09Z

Visualization: set perrow

← Previous revision		Revision as of 15:27, 2 February 2025
Line 76:		Line 76:
	* It ''does not'' use learning or non-chronological backtracking (introduced in 1996).		* It ''does not'' use learning or non-chronological backtracking (introduced in 1996).
	An example with visualization of a DPLL algorithm having chronological backtracking:		An example with visualization of a DPLL algorithm having chronological backtracking:
	<gallery>		<gallery perrow="4" widths="200px">
	Image:Dpll1.png\|All clauses making a CNF formula		Image:Dpll1.png\|All clauses making a CNF formula
	Image:Dpll2.png\|Pick a variable		Image:Dpll2.png\|Pick a variable

Urban Versis 32: Adding local short description: "Type of search algorithm", overriding Wikidata description "algorithm for solving the CNF-SAT problem"

2024-02-09T01:12:19Z

Adding local short description: "Type of search algorithm", overriding Wikidata description "algorithm for solving the CNF-SAT problem"

← Previous revision		Revision as of 01:12, 9 February 2024
Line 1:		Line 1:
			{{Short description\|Type of search algorithm}}
	{{Infobox algorithm		{{Infobox algorithm
	\|name=DPLL		\|name=DPLL

131.111.185.41: /* The algorithm */

2024-01-29T22:43:59Z

The algorithm

← Previous revision		Revision as of 22:43, 29 January 2024
Line 32:		Line 32:
	; [[Unit propagation]] : If a clause is a ''unit clause'', i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. Unit propagation consists in removing every clause containing a unit clause's literal and in discarding the complement of a unit clause's literal from every clause containing that complement. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.		; [[Unit propagation]] : If a clause is a ''unit clause'', i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. Unit propagation consists in removing every clause containing a unit clause's literal and in discarding the complement of a unit clause's literal from every clause containing that complement. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.

	; Pure literal elimination : If a [[propositional variable]] occurs with only one [[Polarity (mathematical logic)\|polarity]] in the formula, it is called ''pure''. A pure literal can always be assigned in a way that makes all clauses containing it true. Thus, when it is assigned such way, these clauses do not constrain the search anymore, and can be deleted.		; Pure literal elimination : If a [[propositional variable]] occurs with only one [[Polarity (mathematical logic)\|polarity]] in the formula, it is called ''pure''. A pure literal can always be assigned in a way that makes all clauses containing it true. Thus, when it is assigned in such a way, these clauses do not constrain the search anymore, and can be deleted.

	Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.		Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.