Certifying algorithm - Revision history

78.22.198.37 at 18:55, 22 January 2024

2024-01-22T18:55:11Z

← Previous revision		Revision as of 18:55, 22 January 2024
Line 20:		Line 20:
	\| doi = 10.1007/s10817-013-9289-2		\| doi = 10.1007/s10817-013-9289-2
	\| issue = 3		\| issue = 3
	\| journal = Journal of Automated Reasoning		\| journal = [[Journal of Automated Reasoning]]
	\| pages = 241–273		\| pages = 241–273
	\| title = A Framework for the Verification of Certifying Computations		\| title = A Framework for the Verification of Certifying Computations
Line 29:		Line 29:
	==Examples==		==Examples==
	Many examples of problems with checkable algorithms come from [[graph theory]].		Many examples of problems with checkable algorithms come from [[graph theory]].
	For instance, a classical algorithm for testing whether a graph is [[bipartite graph\|bipartite]] would simply output a Boolean value: true if the graph is bipartite, false otherwise. In contrast, a certifying algorithm might output a 2-coloring of the graph in the case that it is bipartite, or a cycle of odd length if it is not. Any graph is bipartite if and only if it can be 2-colored, and non-bipartite if and only if it contains an odd cycle. Both checking whether a 2-coloring is valid and checking whether a given odd-length sequence of vertices is a cycle may be performed more simply than testing bipartiteness.<ref name="mmns"/>		For instance, a classical algorithm for testing whether a graph is [[bipartite graph\|bipartite]] would simply output a Boolean value: true if the graph is bipartite, false otherwise. In contrast, a certifying algorithm might output a [[graph coloring\|2-coloring]] of the graph in the case that it is bipartite, or a [[cycle (graph theory)\|cycle]] of odd length if it is not. Any graph is bipartite if and only if it can be 2-colored, and non-bipartite if and only if it contains an odd cycle. Both checking whether a 2-coloring is valid and checking whether a given odd-length sequence of vertices is a cycle may be performed more simply than testing bipartiteness.<ref name="mmns"/>

	Analogously, it is possible to test whether a given directed graph is [[directed acyclic graph\|acyclic]] by a certifying algorithm that outputs either a [[topological sorting\|topological order]] or a directed cycle. It is possible to test whether an undirected graph is a [[chordal graph]] by a certifying algorithm that outputs either an elimination ordering (an ordering of all vertices such that, for every vertex, the neighbors that are later in the ordering form a [[Clique (graph theory)\|clique]]) or a chordless cycle. And it is possible to test whether a graph is [[planar graph\|planar]] by a certifying algorithm that outputs either a planar embedding or a [[Kuratowski's theorem\|Kuratowski subgraph]].<ref name="mmns"/>		Analogously, it is possible to test whether a given [[directed graph]] is [[directed acyclic graph\|acyclic]] by a certifying algorithm that outputs either a [[topological sorting\|topological order]] or a directed cycle. It is possible to test whether an undirected graph is a [[chordal graph]] by a certifying algorithm that outputs either an elimination ordering (an ordering of all vertices such that, for every vertex, the neighbors that are later in the ordering form a [[Clique (graph theory)\|clique]]) or a chordless cycle. And it is possible to test whether a graph is [[planar graph\|planar]] by a certifying algorithm that outputs either a planar embedding or a [[Kuratowski's theorem\|Kuratowski subgraph]].<ref name="mmns"/>

	The [[extended Euclidean algorithm]] for the [[greatest common divisor]] of two integers {{mvar\|x}} and {{mvar\|y}} is certifying: it outputs three integers {{mvar\|g}} (the divisor), {{mvar\|a}}, and {{mvar\|b}}, such that {{math\|''ax'' + ''by'' {{=}} ''g''}}. This equation can only be true of multiples of the greatest common divisor, so testing that {{mvar\|g}} is the greatest common divisor may be performed by checking that {{mvar\|g}} divides both {{mvar\|x}} and {{mvar\|y}} and that this equation is correct.<ref name="mmns"/>		The [[extended Euclidean algorithm]] for the [[greatest common divisor]] of two integers {{mvar\|x}} and {{mvar\|y}} is certifying: it outputs three integers {{mvar\|g}} (the divisor), {{mvar\|a}}, and {{mvar\|b}}, such that {{math\|''ax'' + ''by'' {{=}} ''g''}}. This equation can only be true of multiples of the greatest common divisor, so testing that {{mvar\|g}} is the greatest common divisor may be performed by checking that {{mvar\|g}} divides both {{mvar\|x}} and {{mvar\|y}} and that this equation is correct.<ref name="mmns"/>

Jarble: linking

2019-09-17T23:19:53Z

linking

← Previous revision		Revision as of 23:19, 17 September 2019
Line 1:		Line 1:
	In [[theoretical computer science]], a '''certifying algorithm''' is an algorithm that outputs, together with a solution to the problem it solves, a proof that the solution is correct. A certifying algorithm is said to be ''efficient'' if the combined runtime of the algorithm and a proof checker is slower by at most a constant factor than the best known non-certifying algorithm for the same problem.<ref name="mmns">{{citation		In [[theoretical computer science]], a '''certifying algorithm''' is an algorithm that outputs, together with a solution to the problem it solves, a proof that the solution is correct. A certifying algorithm is said to be ''efficient'' if the combined runtime of the algorithm and a [[proof checker]] is slower by at most a constant factor than the best known non-certifying algorithm for the same problem.<ref name="mmns">{{citation
	\| last1 = McConnell \| first1 = R.M.		\| last1 = McConnell \| first1 = R.M.
	\| last2 = Mehlhorn \| first2 = K. \| author2-link = Kurt Mehlhorn		\| last2 = Mehlhorn \| first2 = K. \| author2-link = Kurt Mehlhorn

OAbot: Open access bot: add arxiv identifier to citation with #oabot.

2018-05-16T12:31:17Z

Open access bot: add arxiv identifier to citation with #oabot.

← Previous revision		Revision as of 12:31, 16 May 2018
Line 23:		Line 23:
	\| pages = 241–273		\| pages = 241–273
	\| title = A Framework for the Verification of Certifying Computations		\| title = A Framework for the Verification of Certifying Computations
	\| volume = 52}}.</ref>		\| volume = 52\| arxiv = 1301.7462}}.</ref>

	Implementations of certifying algorithms that also include a checker for the proof generated by the algorithm may be considered to be more reliable than non-certifying algorithms. For, whenever the algorithm is run, one of three things happens: it produces a correct output (the desired case), it detects a bug in the algorithm or its implication (undesired, but generally preferable to continuing without detecting the bug), or both the algorithm and the checker are faulty in a way that masks the bug and prevents it from being detected (undesired, but unlikely as it depends on the existence of two independent bugs).<ref name="mmns"/>		Implementations of certifying algorithms that also include a checker for the proof generated by the algorithm may be considered to be more reliable than non-certifying algorithms. For, whenever the algorithm is run, one of three things happens: it produces a correct output (the desired case), it detects a bug in the algorithm or its implication (undesired, but generally preferable to continuing without detecting the bug), or both the algorithm and the checker are faulty in a way that masks the bug and prevents it from being detected (undesired, but unlikely as it depends on the existence of two independent bugs).<ref name="mmns"/>

David Eppstein: see also Sanity check; more cats

2016-08-22T00:04:01Z

David Eppstein: New article

2016-08-21T23:56:24Z

New article

New page

In [[theoretical computer science]], a '''certifying algorithm''' is an algorithm that outputs, together with a solution to the problem it solves, a proof that the solution is correct. A certifying algorithm is said to be ''efficient'' if the combined runtime of the algorithm and a proof checker is slower by at most a constant factor than the best known non-certifying algorithm for the same problem.<ref name="mmns">{{citation
| last1 = McConnell | first1 = R.M.
| last2 = Mehlhorn | first2 = K. | author2-link = Kurt Mehlhorn
| last3 = Näher | first3 = S.
| last4 = Schweitzer | first4 = P.
| date = May 2011
| doi = 10.1016/j.cosrev.2010.09.009
| issue = 2
| journal = Computer Science Review
| pages = 119–161
| title = Certifying algorithms
| volume = 5}}.</ref>

The proof produced by a certifying algorithm should be in some sense simpler than the algorithm itself, for otherwise any algorithm could be considered certifying (with its output verified by running the same algorithm again). Sometimes this is formalized by requiring that a verification of the proof take less time than the original algorithm, while for other problems (in particular those for which the solution can be found in [[linear time]]) simplicity of the output proof is considered in a less formal sense.<ref name="mmns"/> For instance, the validity of the output proof may be more apparent to human users than the correctness of the algorithm, or a checker for the proof may be more amenable to [[formal verification]].<ref name="mmns"/><ref>{{citation
| last1 = Alkassar | first1 = Eyad
| last2 = Böhme | first2 = Sascha
| last3 = Mehlhorn | first3 = Kurt | author3-link = Kurt Mehlhorn
| last4 = Rizkallah | first4 = Christine
| date = June 2013
| doi = 10.1007/s10817-013-9289-2
| issue = 3
| journal = Journal of Automated Reasoning
| pages = 241–273
| title = A Framework for the Verification of Certifying Computations
| volume = 52}}.</ref>

Implementations of certifying algorithms that also include a checker for the proof generated by the algorithm may be considered to be more reliable than non-certifying algorithms. For, whenever the algorithm is run, one of three things happens: it produces a correct output (the desired case), it detects a bug in the algorithm or its implication (undesired, but generally preferable to continuing without detecting the bug), or both the algorithm and the checker are faulty in a way that masks the bug and prevents it from being detected (undesired, but unlikely as it depends on the existence of two independent bugs).<ref name="mmns"/>

==Examples==
Many examples of problems with checkable algorithms come from [[graph theory]].
For instance, a classical algorithm for testing whether a graph is [[bipartite graph|bipartite]] would simply output a Boolean value: true if the graph is bipartite, false otherwise. In contrast, a certifying algorithm might output a 2-coloring of the graph in the case that it is bipartite, or a cycle of odd length if it is not. Any graph is bipartite if and only if it can be 2-colored, and non-bipartite if and only if it contains an odd cycle. Both checking whether a 2-coloring is valid and checking whether a given odd-length sequence of vertices is a cycle may be performed more simply than testing bipartiteness.<ref name="mmns"/>

Analogously, it is possible to test whether a given directed graph is [[directed acyclic graph|acyclic]] by a certifying algorithm that outputs either a [[topological sorting|topological order]] or a directed cycle. It is possible to test whether an undirected graph is a [[chordal graph]] by a certifying algorithm that outputs either an elimination ordering (an ordering of all vertices such that, for every vertex, the neighbors that are later in the ordering form a [[Clique (graph theory)|clique]]) or a chordless cycle. And it is possible to test whether a graph is [[planar graph|planar]] by a certifying algorithm that outputs either a planar embedding or a [[Kuratowski's theorem|Kuratowski subgraph]].<ref name="mmns"/>

The [[extended Euclidean algorithm]] for the [[greatest common divisor]] of two integers {{mvar|x}} and {{mvar|y}} is certifying: it outputs three integers {{mvar|g}} (the divisor), {{mvar|a}}, and {{mvar|b}}, such that {{math|''ax'' + ''by'' {{=}} ''g''}}. This equation can only be true of multiples of the greatest common divisor, so testing that {{mvar|g}} is the greatest common divisor may be performed by checking that {{mvar|g}} divides both {{mvar|x}} and {{mvar|y}} and that this equation is correct.<ref name="mmns"/>

==References==
{{reflist}}

[[Category:Algorithms]]

← Previous revision		Revision as of 00:04, 22 August 2016
Line 34:		Line 34:

	The [[extended Euclidean algorithm]] for the [[greatest common divisor]] of two integers {{mvar\|x}} and {{mvar\|y}} is certifying: it outputs three integers {{mvar\|g}} (the divisor), {{mvar\|a}}, and {{mvar\|b}}, such that {{math\|''ax'' + ''by'' {{=}} ''g''}}. This equation can only be true of multiples of the greatest common divisor, so testing that {{mvar\|g}} is the greatest common divisor may be performed by checking that {{mvar\|g}} divides both {{mvar\|x}} and {{mvar\|y}} and that this equation is correct.<ref name="mmns"/>		The [[extended Euclidean algorithm]] for the [[greatest common divisor]] of two integers {{mvar\|x}} and {{mvar\|y}} is certifying: it outputs three integers {{mvar\|g}} (the divisor), {{mvar\|a}}, and {{mvar\|b}}, such that {{math\|''ax'' + ''by'' {{=}} ''g''}}. This equation can only be true of multiples of the greatest common divisor, so testing that {{mvar\|g}} is the greatest common divisor may be performed by checking that {{mvar\|g}} divides both {{mvar\|x}} and {{mvar\|y}} and that this equation is correct.<ref name="mmns"/>

			==See also==
			*[[Sanity check]], a simple test of the correctness of an output or intermediate result that is not required to be a complete proof of correctness

	==References==		==References==
Line 39:		Line 42:

	[[Category:Algorithms]]		[[Category:Algorithms]]
			[[Category:Error detection and correction]]
			[[Category:Software testing]]