Synthesizing shortest linear straight-line programs over GF(2) using SAT

Carsten Fuhs*, Peter Schneider-Kamp

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Non-trivial linear straight-line programs over the Galois field of two elements occur frequently in applications such as encryption or high-performance computing. Finding the shortest linear straight-line program for a given set of linear forms is known to be MaxSNP-complete, i.e., there is no ε-approximation for the problem unless P = NP. This paper presents a non-approximative approach for finding the shortest linear straight-line program. In other words, we show how to search for a circuit of XOR gates with the minimal number of such gates. The approach is based on a reduction of the associated decision problem ("Is there a program of length k?") to satisfiability of propositional logic. Using modern SAT solvers, optimal solutions to interesting problem instances can be obtained.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings
Number of pages14
Publication date2. Aug 2010
Pages71-84
ISBN (Print)3642141854, 9783642141850
DOIs
Publication statusPublished - 2. Aug 2010
Event13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010 - Edinburgh, United Kingdom
Duration: 11. Jul 201014. Jul 2010

Conference

Conference13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010
Country/TerritoryUnited Kingdom
CityEdinburgh
Period11/07/201014/07/2010
SponsorEPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc.
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6175 LNCS
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Synthesizing shortest linear straight-line programs over GF(2) using SAT'. Together they form a unique fingerprint.

Cite this