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

Carsten Fuhs*, Peter Schneider-Kamp

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

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

Cryptography
Networks (circuits)

Citer dette

Fuhs, C., & Schneider-Kamp, P. (2010). Synthesizing shortest linear straight-line programs over GF(2) using SAT. I Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings (s. 71-84). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind. 6175 LNCS https://doi.org/10.1007/978-3-642-14186-7_8
Fuhs, Carsten ; Schneider-Kamp, Peter. / Synthesizing shortest linear straight-line programs over GF(2) using SAT. Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings. 2010. s. 71-84 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 6175 LNCS).
@inproceedings{80c6c80b3a694ca3a8269948efaf19e4,
title = "Synthesizing shortest linear straight-line programs over GF(2) using SAT",
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.",
author = "Carsten Fuhs and Peter Schneider-Kamp",
year = "2010",
month = "8",
day = "2",
doi = "10.1007/978-3-642-14186-7_8",
language = "English",
isbn = "3642141854",
pages = "71--84",
booktitle = "Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings",

}

Fuhs, C & Schneider-Kamp, P 2010, Synthesizing shortest linear straight-line programs over GF(2) using SAT. i Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 6175 LNCS, s. 71-84, 13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010, Edinburgh, Storbritannien, 11/07/2010. https://doi.org/10.1007/978-3-642-14186-7_8

Synthesizing shortest linear straight-line programs over GF(2) using SAT. / Fuhs, Carsten; Schneider-Kamp, Peter.

Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings. 2010. s. 71-84 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 6175 LNCS).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

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

AU - Fuhs, Carsten

AU - Schneider-Kamp, Peter

PY - 2010/8/2

Y1 - 2010/8/2

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77954969533&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14186-7_8

DO - 10.1007/978-3-642-14186-7_8

M3 - Article in proceedings

SN - 3642141854

SN - 9783642141850

SP - 71

EP - 84

BT - Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings

ER -

Fuhs C, Schneider-Kamp P. Synthesizing shortest linear straight-line programs over GF(2) using SAT. I Theory and Applications of Satisfiability Testing - 13th International Conference, SAT 2010, Proceedings. 2010. s. 71-84. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 6175 LNCS). https://doi.org/10.1007/978-3-642-14186-7_8