Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Using Constraint Logic Programming to Schedule Solar Array Operations on the International Space Station Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

The Picat-SAT Compiler

verfasst von : Neng-Fa Zhou, Håkan Kjellerstrand

Erschienen in: Practical Aspects of Declarative Languages

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

SAT has become the backbone of many software systems. In order to make full use of the power of SAT solvers, a SAT compiler must encode domain variables and constraints into an efficient SAT formula. Despite many proposals for SAT encodings, there are few working SAT compilers. This paper presents Picat-SAT, the SAT compiler in the Picat system. Picat-SAT employs the sign-and-magnitude log encoding for domain variables. Log-encoding for constraints resembles the binary representation of numbers used in computer hardware, and many algorithms and optimization opportunities have been exploited by hardware design systems. This paper gives the encoding algorithms for constraints, and attempts to experimentally justify the choices of the algorithms for the addition and multiplication constraints. This paper also presents preliminary, but quite encouraging, experimental results.

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 A GPU Implementation of the ASP Computation
Nächstes Kapitel Default Rules for Curry
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
The FznTini compiler is not maintained.
 
2
Picat supports the dot-notation for chaining function calls. The function call Board.vars() is the same as vars(Board).
 
3
The operators div and mod can be expressed by using the multiplication operator \(\times \). In the implemented version of Picat-SAT, Pseudo-Boolean constraints are treated in the same way as other linear constraints, except for the special case \(\varSigma _{i}^nB_i\ r\ c\) (c = 1 or 2).
 
4
Booth’s algorithm has not yet been implemented in Picat-SAT.
 
5
Efforts were also made to compare Picat-SAT with FznTini [15], a log-encoding based SAT compiler, and with meSAT [29], which supports the hybrid of order and sparse encodings. FznTini is for an old version of FlatZinc, and the default setting of meSAT did not perform better than Sugar on the benchmarks.
 
6
The CPU time does not include the compile time for any of the SAT compilers.
 
7
Picat-SAT scored 0 on project-planning because mzn2fzn failed to specialize the element constraint, which prevented Picat’s FlatZinc interpreter from functioning. It was understood that mzn2fzn would specialize generic global constraints into specific ones once the types of the arguments are known.
 
8
Note that the code size sometimes decreases with N because of the domain constraints.
 
Literatur
1.
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)MATH
2.
Bjork, M.: Successful SAT encoding techniques. JSAT Addendum (2009)
3.
4.
Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: a comparative survey. ACM Comput. Surv. 38(4), 1–54 (2006)CrossRef
5.
Brayton, R.K., Hachtel, G.D., McMullen, C.T., Sangiovanni-Vincentelli, A.L.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Boston (1984)CrossRefMATH
6.
Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Commun. ACM 54(12), 92–103 (2011)CrossRef
7.
Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceeding of the 9th International Workshop of Constraint Modeling and Reformulation (2010)
8.
Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: AAAI, pp. 1092–1097 (1994)
9.
Boulanger, J.L. (ed.): Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, New York (2014)
10.
11.
Gavanelli, M.: The log-support encoding of CSP into SAT. In: CP, pp. 815–822 (2007)
12.
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI, pp. 386–392 (2007)
13.
Ian Gent, P.: Arc consistency in SAT. In: ECAI, pp. 121–125 (2002)
14.
15.
Huang, J.: Universal Booleanization of constraint models. In: CP, pp. 144–158 (2008)
16.
Iwama, K., Miyazaki, S.: SAT-varible complexity of hard combinatorial problems. IFIP Congress 1, 253–258 (1994)MathSciNet
17.
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)
18.
Jackson, E.K.: A module system for domain-specific languages. Theory Pract. Logic Program. 14(4–5), 771–785 (2014)CrossRefMATH
19.
20.
Karatsuba, A., Ofman, Y.: Multiplication of many-digital numbers by automatic computers. In: Proceeding the USSR Academy of Sciences, vol. 145 pp. 293–294 (1962)
21.
Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359–363 (1992)
22.
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2004)
23.
Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)CrossRef
24.
25.
Metodi, A., Codish, M.: Compiling finite domain constraints to SAT with BEE. Theory Pract. Logic Program. 12(4–5), 465–483 (2012)CrossRefMATH
26.
Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.R.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007)CrossRef
27.
28.
Drechsler, R., Eggersglüß, S.: High Quality Test Pattern Generation and Boolean Satisfiability. Springer, New York (2012)MATH
29.
30.
31.
32.
Tanjo, T., Tamura, N., Banbara, M.: Azucar: a SAT-based CSP solver using compact order encoding. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 456–462. Springer, Heidelberg (2012)CrossRef
33.
Walsh, T.: SAT \(v\) CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, p. 441. Springer, Heidelberg (2000)CrossRef
34.
35.
Zhou, N.-F., Kjellerstrand, H., Fruhman, J.: Constraint Solving and Planning with Picat. Springer, Heidelberg (2015)CrossRef
Metadaten
Titel
The Picat-SAT Compiler
verfasst von
Neng-Fa Zhou
Håkan Kjellerstrand
Copyright-Jahr
2016
Buch
Practical Aspects of Declarative Languages

Print ISBN: 978-3-319-28227-5

Electronic ISBN: 978-3-319-28228-2

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-28228-2_4

Premium Partner

    Bildnachweise