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

Originalsprog | Engelsk |
---|---|

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

Antal sider | 14 |

Publikationsdato | 2. aug. 2010 |

Sider | 71-84 |

ISBN (Trykt) | 3642141854, 9783642141850 |

DOI | |

Status | Udgivet - 2. aug. 2010 |

Begivenhed | 13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010 - Edinburgh, Storbritannien Varighed: 11. jul. 2010 → 14. jul. 2010 |

### Konference

Konference | 13th International Conference on Theory and Applications of Satisfiability Testing, SAT 2010 |
---|---|

Land | Storbritannien |

By | Edinburgh |

Periode | 11/07/2010 → 14/07/2010 |

Sponsor | EPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc. |

Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Vol/bind | 6175 LNCS |

ISSN | 0302-9743 |

### Fingeraftryk

### Citer dette

*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

}

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

Publikation: Bidrag til bog/antologi/rapport/konference-proceeding › Konferencebidrag i proceedings › Forskning › peer 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 -