Talk:DPLL algorithm - Revision history

Qwerfjkl (bot): Implementing WP:PIQA (Task 26)

2024-01-27T13:46:38Z

← Previous revision		Revision as of 13:46, 27 January 2024
Line 1:		Line 1:
	{{WikiProject ~~Computer~~ ~~science~~\|~~importance~~=~~high~~\|~~class=start}}~~		{{WikiProject banner shell\|class=Start\|
			{{WikiProject Computer science\|importance=high}}
			}}

	== Subsumption ==		== Subsumption ==

SineBot: Signing comment by 2601:14D:4400:570:EC40:8323:DAA4:F6F9 - "Added question and link to the 1958 NSA report."

2022-10-06T13:35:18Z

Signing comment by 2601:14D:4400:570:EC40:8323:DAA4:F6F9 - "Added question and link to the 1958 NSA report."

← Previous revision		Revision as of 13:35, 6 October 2022
Line 101:		Line 101:
	Would it be worthwhile to update the page w/ information in the originating 1958 NSA report?		Would it be worthwhile to update the page w/ information in the originating 1958 NSA report?

	Link to paper and exposition - [https://link.springer.com/content/pdf/bbm:978-3-319-41842-1/1.pdf]		Link to paper and exposition - [https://link.springer.com/content/pdf/bbm:978-3-319-41842-1/1.pdf] <!-- Template:Unsigned IP --><small class="autosigned">— Preceding [[Wikipedia:Signatures\|unsigned]] comment added by [[Special:Contributions/2601:14D:4400:570:EC40:8323:DAA4:F6F9\|2601:14D:4400:570:EC40:8323:DAA4:F6F9]] ([[User talk:2601:14D:4400:570:EC40:8323:DAA4:F6F9#top\|talk]]) 13:34, 6 October 2022 (UTC)</small> <!--Autosigned by SineBot-->

2601:14D:4400:570:EC40:8323:DAA4:F6F9: Added question and link to the 1958 NSA report.

2022-10-06T13:34:16Z

Added question and link to the 1958 NSA report.

← Previous revision		Revision as of 13:34, 6 October 2022
Line 96:		Line 96:
	:Assigning an appropriate truth value to a pure literal preserves satisfiability. In the example, if the original CNF can be satisfied, then the reduced one can be satisfied, too, since it is a subproblem. Vice versa, if the reduced CNF is satisfied by an assignment, then extending it by y:=FALSE will yield a satsifying assignment for the original CNF. So, we don't need both branches.		:Assigning an appropriate truth value to a pure literal preserves satisfiability. In the example, if the original CNF can be satisfied, then the reduced one can be satisfied, too, since it is a subproblem. Vice versa, if the reduced CNF is satisfied by an assignment, then extending it by y:=FALSE will yield a satsifying assignment for the original CNF. So, we don't need both branches.
	:I guess the name "pure literal elimination" is motivated by the fact that a pure literal is needed to apply the rule. Maybe, it should merely be read as "elimination (of clauses) ''based'' on pure literals", rather than as "elimination of pure literals (and nothing else)". The literal if eliminated by eliminating the clause it is contained in. - [[User:Jochen Burghardt\|Jochen Burghardt]] ([[User talk:Jochen Burghardt\|talk]]) 14:39, 2 May 2021 (UTC)		:I guess the name "pure literal elimination" is motivated by the fact that a pure literal is needed to apply the rule. Maybe, it should merely be read as "elimination (of clauses) ''based'' on pure literals", rather than as "elimination of pure literals (and nothing else)". The literal if eliminated by eliminating the clause it is contained in. - [[User:Jochen Burghardt\|Jochen Burghardt]] ([[User talk:Jochen Burghardt\|talk]]) 14:39, 2 May 2021 (UTC)

			== 1958 & NSA ==

			Would it be worthwhile to update the page w/ information in the originating 1958 NSA report?

			Link to paper and exposition - [https://link.springer.com/content/pdf/bbm:978-3-319-41842-1/1.pdf]

Christian75: Undid revision 1021270041 by 37.224.184.241 (talk)

2022-02-25T08:42:34Z

Undid revision 1021270041 by 37.224.184.241 (talk)

← Previous revision		Revision as of 08:42, 25 February 2022
Line 1:		Line 1:
			{{WikiProject Computer science\|importance=high\|class=start}}

	== Subsumption ==		== Subsumption ==

37.224.184.241 at 20:10, 3 May 2021

2021-05-03T20:10:07Z

← Previous revision		Revision as of 20:10, 3 May 2021
Line 1:		Line 1:
	{{WikiProject Computer science\|importance=high\|class=start}}

	== Subsumption ==		== Subsumption ==

Jochen Burghardt: /* Pure literal elimination */

2021-05-02T14:39:03Z

Pure literal elimination

← Previous revision		Revision as of 14:39, 2 May 2021
Line 91:		Line 91:
	:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)		:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)
	::::{{Ping\|Jochen Burghardt}} I correct the sentence, to remove this ambiguity. Please inspect it. Thanks, [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:36, 2 May 2021 (UTC)		::::{{Ping\|Jochen Burghardt}} I correct the sentence, to remove this ambiguity. Please inspect it. Thanks, [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:36, 2 May 2021 (UTC)

			:Now that I've typed it in, I'll show my reply anyway:
			:For example, in the CNF (w ∨ x ∨ ¬z) ∧ (x ∨ ¬y ∨ z) ∧ (¬w ∨ ¬y ∨ z) ∧ (¬w ∨ ¬x ∨ z) the variable y occurse only negated, it is hence pure. By assigning FALSE to y, all clauses containing ¬y can be satisfied. The remaining problem is just to satisfy the clauses that don't contain ¬y, that is, those remaining after deleting all ''clauses'' containing ¬y. In the example: (w ∨ x ∨ ¬z) ∧ (¬w ∨ ¬x ∨ z). Deleting only the literal ¬y everywhere would leave an unneccessarily complicated problem.
			:Assigning an appropriate truth value to a pure literal preserves satisfiability. In the example, if the original CNF can be satisfied, then the reduced one can be satisfied, too, since it is a subproblem. Vice versa, if the reduced CNF is satisfied by an assignment, then extending it by y:=FALSE will yield a satsifying assignment for the original CNF. So, we don't need both branches.
			:I guess the name "pure literal elimination" is motivated by the fact that a pure literal is needed to apply the rule. Maybe, it should merely be read as "elimination (of clauses) ''based'' on pure literals", rather than as "elimination of pure literals (and nothing else)". The literal if eliminated by eliminating the clause it is contained in. - [[User:Jochen Burghardt\|Jochen Burghardt]] ([[User talk:Jochen Burghardt\|talk]]) 14:39, 2 May 2021 (UTC)

Hooman Mallahzadeh: /* Pure literal elimination */

2021-05-02T14:36:37Z

Pure literal elimination

← Previous revision		Revision as of 14:36, 2 May 2021
Line 90:		Line 90:
	::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)		::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)
	:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)		:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)
			::::{{Ping\|Jochen Burghardt}} I correct the sentence, to remove this ambiguity. Please inspect it. Thanks, [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:36, 2 May 2021 (UTC)

Hooman Mallahzadeh: /* Pure literal elimination */

2021-05-02T14:28:11Z

Pure literal elimination

← Previous revision		Revision as of 14:28, 2 May 2021
Line 89:		Line 89:
	:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm.		:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm.
	::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)		::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)
			:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)

Hooman Mallahzadeh: /* Pure literal elimination */

2021-05-02T14:16:21Z

Pure literal elimination

← Previous revision		Revision as of 14:16, 2 May 2021
Line 87:		Line 87:
	{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}		{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}
	I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)		I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)
	:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:13, 2 May 2021 (UTC)		:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm.
			::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)

Hooman Mallahzadeh: /* Pure literal elimination */

2021-05-02T14:13:43Z

Pure literal elimination

← Previous revision		Revision as of 14:13, 2 May 2021
Line 87:		Line 87:
	{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}		{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}
	I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)		I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)
			:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:13, 2 May 2021 (UTC)

← Previous revision		Revision as of 14:36, 2 May 2021
Line 90:		Line 90:
	::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)		::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)
	:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)		:::{{Ping\|Jochen Burghardt}} Yes you are right, here {{Quote\|In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula.}} So we are in "true branch" and all clauses are deleted, sorry I've make a mistake. You are right. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:28, 2 May 2021 (UTC)
			::::{{Ping\|Jochen Burghardt}} I correct the sentence, to remove this ambiguity. Please inspect it. Thanks, [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:36, 2 May 2021 (UTC)

← Previous revision		Revision as of 14:16, 2 May 2021
Line 87:		Line 87:
	{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}		{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}
	I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)		I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)
	:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:13, 2 May 2021 (UTC)		:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm.
			::Or the title should be "Clause elimination" instead of "Pure literal elimination"!!!! [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:16, 2 May 2021 (UTC)

← Previous revision		Revision as of 14:13, 2 May 2021
Line 87:		Line 87:
	{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}		{{Quote\|Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses/literal do not constrain the search anymore and can be deleted.}}
	I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)		I think the correct word is literal. Thanks,[[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 13:58, 2 May 2021 (UTC)
			:Yes you are right, if pure literals become true, all clauses is eliminated. But in search we have two branches, false and true, perhaps here title should be "Pure true literal elimination", because in false case, it remains in the search algorithm. [[User:Hooman Mallahzadeh\|Hooman Mallahzadeh]] ([[User talk:Hooman Mallahzadeh\|talk]]) 14:13, 2 May 2021 (UTC)