Skip to content

Instantly share code, notes, and snippets.

@Mr-Slippery
Last active November 19, 2020 15:09
Show Gist options
  • Save Mr-Slippery/9662c42c75f548180a0be952e949a174 to your computer and use it in GitHub Desktop.
Save Mr-Slippery/9662c42c75f548180a0be952e949a174 to your computer and use it in GitHub Desktop.
Hamiltonian cycle finder with KLEE
#include <klee/klee.h>
#include <assert.h>
typedef unsigned char byte;
#define N 5
byte a[N * N]=
{
/* A B C D E*/
/*A*/1,1,1,1,1,
/*B*/1,1,0,0,1,
/*C*/1,0,1,1,1,
/*D*/1,0,1,1,0,
/*E*/1,1,1,0,1
};
int ham_cycle(byte *path)
{
byte i;
byte visited[N + 1] = { 0 };
if (path[N] != path[0]) {
return 0;
}
for (i = 0; i < N; i++) {
if (path[i] >= N) {
return 0;
}
if (visited[path[i]]) {
return 0;
}
visited[path[i]]++;
}
for (i = 0; i < N; i++) {
byte x = path[i];
byte y = path[i + 1];
if (!a[x + y * N]) {
return 0;
}
}
return 1;
}
int main(int argc, char *argv[])
{
byte i;
byte cycle[N + 1];
klee_make_symbolic(&cycle[0], sizeof(byte) * (N + 1), "cycle");
klee_assert(!ham_cycle(cycle));
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment