Fuhs, Carsten; Schneider-Kamp, Peter Synthesizing shortest linear straight-line programs over \(\mathrm{GF}(2)\) using SAT. (English) Zbl 1306.68156 Strichman, Ofer (ed.) et al., Theory and applications of satisfiability testing – SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14185-0/pbk). Lecture Notes in Computer Science 6175, 71-84 (2010). Summary: 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 \(\epsilon \)-approximation for the problem unless \(\text{P} = \text{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.For the entire collection see [Zbl 1196.68013]. Cited in 6 Documents MSC: 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) 03B05 Classical propositional logic 11Y16 Number-theoretic algorithms; complexity 68Q25 Analysis of algorithms and problem complexity 94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010) Software:AProVE PDFBibTeX XMLCite \textit{C. Fuhs} and \textit{P. Schneider-Kamp}, Lect. Notes Comput. Sci. 6175, 71--84 (2010; Zbl 1306.68156) Full Text: DOI