paint-brush
Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Linksby@gitflow
153 reads

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Links

by What is GitFlow? The Collaborative Git Alternative
What is GitFlow? The Collaborative Git Alternative HackerNoon profile picture

What is GitFlow? The Collaborative Git Alternative

@gitflow

A branching model for Git, created by Vincent Driessen. ...

June 8th, 2024
Read on Terminal Reader
Read this story in a terminal
Print this story
Read this story w/o Javascript
Read this story w/o Javascript
tldt arrow

Too Long; Didn't Read

In this paper, researchers describe an implementation of the Dancing Links optimization in the Rust programming language.
featured image - Verification of a Rust Implementation of Knuth’s Dancing
Links using ACL2: Dancing Links
1x
Read by Dr. One voice-avatar

Listen to this story

What is GitFlow? The Collaborative Git Alternative HackerNoon profile picture
What is GitFlow? The Collaborative Git Alternative

What is GitFlow? The Collaborative Git Alternative

@gitflow

A branching model for Git, created by Vincent Driessen. #1 blog dedicated exclusively to forwarding the GitFlow agenda.

About @gitflow
LEARN MORE ABOUT @GITFLOW'S
EXPERTISE AND PLACE ON THE INTERNET.
0-item

STORY’S CREDIBILITY

Academic Research Paper

Academic Research Paper

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Author:

(1) David S. Hardin, Cedar Rapids, IA USA david.s.hardin@gmail.com.

The concept behind Dancing Links is quite simple: when a given element Y of a list is removed in an exact cover algorithm, it is very likely that this same element will later be restored. Thus, rather


Figure 1: Dancing Links in action. (a) Portion of a circular doubly-linked list prior to a remove operation; (b) After the remove operation on element Y; (c) After the restore operation for element Y.

Figure 1: Dancing Links in action. (a) Portion of a circular doubly-linked list prior to a remove operation; (b) After the remove operation on element Y; (c) After the restore operation for element Y.


than “zero out” the ‘previous’ and ‘next’ links associated with element Y, as good programming hygiene would normally dictate, in Dancing Links, the programmer leaves the link values in place for the removed element. The Dancing Links remove operator thus deletes element Y from the list, setting the ’next’ element of the preceding element X to the following element Z, and setting the ’previous’ element of Z to a link to X, but not touching the ’next’ and ’previous’ links of the removed element Y. Later on, if Y needs to be restored, it is simply hooked back in to the list using a simple restore operator. In Knuth’s words, if one monitors the list links as the DLX algorithm proceeds, the links appear to ‘dance’, hence the name. Knuth’s Dancing Links functionality is summarized in Fig. 1.


This paper is available on arxiv under CC 4.0 license.


L O A D I N G
. . . comments & more!

About Author

What is GitFlow? The Collaborative Git Alternative HackerNoon profile picture
What is GitFlow? The Collaborative Git Alternative@gitflow
A branching model for Git, created by Vincent Driessen. #1 blog dedicated exclusively to forwarding the GitFlow agenda.

TOPICS

THIS ARTICLE WAS FEATURED IN...

Permanent on Arweave
Read on Terminal Reader
Read this story in a terminal
 Terminal
Read this story w/o Javascript
Read this story w/o Javascript
 Lite
X REMOVE AD