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

Carsten Fuhs*, Peter Schneider-Kamp

*Kontaktforfatter for dette arbejde

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.

OriginalsprogEngelsk
TitelTheory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings
Antal sider14
Publikationsdato2. aug. 2010
Sider71-84
ISBN (Trykt)3642141854, 9783642141850
DOI
StatusUdgivet - 2. aug. 2010
Begivenhed13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010 - Edinburgh, Storbritannien
Varighed: 11. jul. 201014. jul. 2010

Konference

Konference13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010
LandStorbritannien
ByEdinburgh
Periode11/07/201014/07/2010
SponsorEPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc.
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind6175 LNCS
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Synthesizing shortest linear straight-line programs over GF(2) using SAT'. Sammen danner de et unikt fingeraftryk.

Citationsformater