This repository has been archived by the owner. It is now read-only.
Find the shortest SLP by transforming it to SAT
Switch branches/tags
Nothing to show
Clone or download
Latest commit 2b18161 Dec 11, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
src add unit test Mar 14, 2015
.gitignore Initial version of SLP SAT problem solver Feb 23, 2015
LICENCE Add README Apr 6, 2015 Add reference Dec 11, 2018
pom.xml Switch to junit4 Mar 3, 2015
program final tweaks, add input for Prøst Mar 3, 2015 Add new test Mar 3, 2015
test Add new test Mar 3, 2015

Find the shortest SLP by transforming it to SAT

Implements Fuhs and Schneider-Kamp's paper "Synthesizing Shortest Linear Straight-Line Programs over GF(2) using SAT".

Part of my Bachelor Thesis project. See


Thom Wiggers. Implementing CAESAR candidate Prøst on ARM11. Student Undergraduate Research E-Journal!, Volume 1, 2015.

  title = "Implementing CAESAR candidate Prøst on ARM11",
  author = "Thom Wiggers",
  date = "2015-11-20",
  journal = "Student Undergraduate Research E-Journal!",
  volume = 1,
  issn = "2468-0443",
  url = "",


Build dependencies

  • Maven
  • Java development environment

Getting started

  1. Compile with mvn package
  2. See for a convenient wrapper with some jvm options.


./ 6 < test     # Try input file test for k = 5
./ 10 5 < test  # Try it for 10 <= k <= 5


Copyright (C) 2015 Thom Wiggers

This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program. If not, see