nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

On the Usefulness of Linear Modular Arithmetic in Constraint Programming

verfasst von : Gilles Pesant, Kuldeep S. Meel, Mahshid Mohammadalitajrishi

Erschienen in: Integration of Constraint Programming, Artificial Intelligence, and Operations Research

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Linear modular constraints are a powerful class of constraints that arise naturally in cryptanalysis, checksums, hash functions, and the like. Given their importance, the past few years have witnessed the design of combinatorial solvers with native support for linear modular constraints, and the availability of such solvers has led to the emergence of new applications. While there exist global constraints in cp that consider congruence classes over domain values, linear modular arithmetic constraints have yet to appear in the global constraint catalogue despite their past investigation in the context of model counting for csps. In this work we seek to remedy the situation by advocating the integration of linear modular constraints in state-of-the-art cp solvers.

Contrary to previous belief, we conclude from an empirical investigation that Gauss-Jordan Elimination based techniques can provide an efficient and scalable way to handle linear modular constraints. On the theoretical side, we remark on the pairwise independence offered by hash functions based on linear modular constraints, and then discuss the design of hashing-based model counters for cp, supported by empirical results showing the accuracy and computational savings that can be achieved. We further demonstrate the usefulness of native support for linear modular constraints with applications to checksums and model counting.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Improving the Filtering of Branch-and-Bound MDD Solver

Nächstes Kapitel Injecting Domain Knowledge in Neural Networks: A Controlled Experiment on a Constrained Problem

One exception is the work on bit-vector domains, involving some modular arithmetic, with applications to software verification and cryptography [1, 8, 13].

Available at https://github.com/PesantGilles/MiniCPBP.

In practice we actually implement the compact table filtering algorithm and apply it directly instead of repeatedly posting and retracting Table constraints.

For example if p is chosen as the smallest prime number larger than the domain size, as one can always find a prime between d and 2d for any \(d>1\).

Bardin, S., Herrmann, P., Perroud, F.: An alternative to SAT-based approaches for bit-vectors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 84–98. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_7CrossRefMATH

Beldiceanu, N., Carlsson, M., Demassey, S., Petit, T.: Global constraint catalogue: past, present and future. Constraints Int. J. 12(1), 21–62 (2007). https://doi.org/10.1007/s10601-006-9010-8MathSciNetCrossRefMATH

Carter, J.L., Wegman, M.N.: Universal classes of hash functions. In: ACM Symposium on Theory of Computing, pp. 106–112. ACM (1977)

Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: Proceedings of AAAI (2016)

Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 200–216. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_18CrossRef

Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Proceedings of IJCAI (2016)

Chakraborty, S., Meel, K.S., Vardi, M.Y.: On the hardness of probabilistic inference relaxations. In: Proceedings of AAAI (2019)

Chihani, Z., Marre, B., Bobot, F., Bardin, S.: Sharpening constraint programming approaches for bit-vector theory. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 3–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59776-8_1CrossRefMATH

Demeulenaere, J., et al.: Compact-table: efficiently filtering table constraints with reversible sparse bit-sets. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 207–223. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44953-1_14CrossRef

10.

Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. Proc. AAAI 21, 54–61 (2006)MATH

11.

Gomes, C.P., van Hoeve, W.J., Sabharwal, A.Selman, B.: Counting CSP solutions using generalized XOR constraints. In: AAAI, pp. 204–209. AAAI Press (2007)

12.

Meel, K.S., Akshay, S.: Sparse hashing for scalable approximate model counting: theory and practice. In: Proceedings of Logic in Computer science (LICS), July 2020

13.

Michel, L.D., Van Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, pp. 527–543. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33558-7_39CrossRef

14.

Smith, C., Gomes, C., Fernández, C.: Streamlining local search for spatially balanced Latin squares. In: Kaelbling, L.P., Saffiotti, A. (eds.) IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, 30 July–5 August 2005, pp. 1539–1540. Professional Book Center (2005)

15.

Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 463–484. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_22CrossRef

16.

Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: Proceedings of AAAI Conference on Artificial Intelligence (AAAI), January 2019

17.

Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24CrossRef

18.

Trick, M.A.: A dynamic programming approach for consistency and propagation for knapsack constraints. Ann. OR 118(1–4), 73–84 (2003). https://doi.org/10.1023/A:1021801522545MathSciNetCrossRefMATH

19.

Vadhan, S.P., et al.: Pseudorandomness. Found. Trends® Theor. Comput. Sci. 7(1–3), 1–336 (2012)

20.

Valiant, L.G.: The complexity of enumeration and reliability problems. SIAM J. Comput. 8(3), 410–421 (1979)MathSciNetCrossRef

21.

Verhaeghe, H., Lecoutre, C., Deville, Y., Schaus, P.: Extending compact-table to basic smart tables. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 297–307. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_19CrossRef

Titel: On the Usefulness of Linear Modular Arithmetic in Constraint Programming
verfasst von: Gilles Pesant
Kuldeep S. Meel
Mahshid Mohammadalitajrishi
Verlag: Springer International Publishing
Buch: Integration of Constraint Programming, Artificial Intelligence, and Operations Research
Print ISBN: 978-3-030-78229-0

Electronic ISBN: 978-3-030-78230-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78230-6_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner