iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/978-3-642-14186-7_8
Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT | SpringerLink
Skip to main content
Springer Nature Link
Log in

Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2010 (SAT 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6175))

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.

Supported by the G.I.F. grant 966-116.6 and the Danish Natural Science Research Council.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167–180. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Boyar, J., Matthews, P., Peralta, R.: On the shortest linear straight-line program for computing linear forms. In: Ochmański, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol. 5162, pp. 168–179. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Boyar, J., Peralta, R.: A new technique for combinational circuit optimization and a new circuit for the S-Box for AES. In: Patent Application Number 61089998 filed with the U.S. Patent and Trademark Office (2009)

    Google Scholar 

  4. Boyar, J., Peralta, R.: A new combinational logic minimization technique with applications to cryptology. In: Festa, P. (ed.) SEA 2010. LNCS, vol. 6049, pp. 178–189. Springer, Heidelberg (2010)

    Google Scholar 

  5. Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 5, 193–215 (2008)

    MathSciNet  MATH  Google Scholar 

  6. Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modelling and Computation (JSAT) 2(1-4), 1–26 (2006)

    MATH  Google Scholar 

  7. Fuhs, C., Giesl, J., Middeldorp, A., Thiemann, R., Schneider-Kamp, P., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483–497. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Hong, H., Jakuš, D.: Testing positiveness of polynomials. Journal of Automated Reasoning (JAR) 21(1), 23–38 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  11. Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 32–44. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Le Berre, D., Parrain, A.: SAT4J, http://www.sat4j.org

  13. Federal Information Processing Standard 197. The advanced encryption standard. Technical report, National Institute of Standards and Technology (2001)

    Google Scholar 

  14. Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125 (1968); Reprinted in Automation of Reasoning 2, 466–483 (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Germany

    Carsten Fuhs

  2. IMADA, University of Southern Denmark, Denmark

    Peter Schneider-Kamp

Authors
  1. Carsten Fuhs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technion, Technion City, 32000, Haifa, Israel

    Ofer Strichman

  2. Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Stefan Szeider

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fuhs, C., Schneider-Kamp, P. (2010). Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14186-7_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14185-0

  • Online ISBN: 978-3-642-14186-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation