-
Notifications
You must be signed in to change notification settings - Fork 21
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #3419 from openjournals/joss.04591
Merging automatically
- Loading branch information
Showing
3 changed files
with
944 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,380 @@ | ||
<?xml version="1.0" encoding="UTF-8"?> | ||
<doi_batch xmlns="http://www.crossref.org/schema/5.3.1" | ||
xmlns:ai="http://www.crossref.org/AccessIndicators.xsd" | ||
xmlns:rel="http://www.crossref.org/relations.xsd" | ||
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
version="5.3.1" | ||
xsi:schemaLocation="http://www.crossref.org/schema/5.3.1 http://www.crossref.org/schemas/crossref5.3.1.xsd"> | ||
<head> | ||
<doi_batch_id>20220809T140906-42e026020d483a3ce60fad4255da9f06896f3a35</doi_batch_id> | ||
<timestamp>20220809140906</timestamp> | ||
<depositor> | ||
<depositor_name>JOSS Admin</depositor_name> | ||
<email_address>[email protected]</email_address> | ||
</depositor> | ||
<registrant>The Open Journal</registrant> | ||
</head> | ||
<body> | ||
<journal> | ||
<journal_metadata> | ||
<full_title>Journal of Open Source Software</full_title> | ||
<abbrev_title>JOSS</abbrev_title> | ||
<issn media_type="electronic">2475-9066</issn> | ||
<doi_data> | ||
<doi>10.21105/joss</doi> | ||
<resource>https://joss.theoj.org/</resource> | ||
</doi_data> | ||
</journal_metadata> | ||
<journal_issue> | ||
<publication_date media_type="online"> | ||
<month>08</month> | ||
<year>2022</year> | ||
</publication_date> | ||
<journal_volume> | ||
<volume>7</volume> | ||
</journal_volume> | ||
<issue>76</issue> | ||
</journal_issue> | ||
<journal_article publication_type="full_text"> | ||
<titles> | ||
<title>Mallob: Scalable SAT Solving On Demand With | ||
Decentralized Job Scheduling</title> | ||
</titles> | ||
<contributors> | ||
<person_name sequence="first" contributor_role="author"> | ||
<given_name>Peter</given_name> | ||
<surname>Sanders</surname> | ||
<ORCID>https://orcid.org/0000-0003-3330-9349</ORCID> | ||
</person_name> | ||
<person_name sequence="additional" | ||
contributor_role="author"> | ||
<given_name>Dominik</given_name> | ||
<surname>Schreiber</surname> | ||
<ORCID>https://orcid.org/0000-0002-4185-1851</ORCID> | ||
</person_name> | ||
</contributors> | ||
<publication_date> | ||
<month>08</month> | ||
<day>09</day> | ||
<year>2022</year> | ||
</publication_date> | ||
<pages> | ||
<first_page>4591</first_page> | ||
</pages> | ||
<publisher_item> | ||
<identifier id_type="doi">10.21105/joss.04591</identifier> | ||
</publisher_item> | ||
<ai:program name="AccessIndicators"> | ||
<ai:license_ref applies_to="vor">http://creativecommons.org/licenses/by/4.0/</ai:license_ref> | ||
<ai:license_ref applies_to="am">http://creativecommons.org/licenses/by/4.0/</ai:license_ref> | ||
<ai:license_ref applies_to="tdm">http://creativecommons.org/licenses/by/4.0/</ai:license_ref> | ||
</ai:program> | ||
<rel:program> | ||
<rel:related_item> | ||
<rel:description>Software archive</rel:description> | ||
<rel:inter_work_relation relationship-type="references" identifier-type="doi">v1.1.0</rel:inter_work_relation> | ||
</rel:related_item> | ||
<rel:related_item> | ||
<rel:description>GitHub review issue</rel:description> | ||
<rel:inter_work_relation relationship-type="hasReview" identifier-type="uri">https://github.com/openjournals/joss-reviews/issues/4591</rel:inter_work_relation> | ||
</rel:related_item> | ||
</rel:program> | ||
<doi_data> | ||
<doi>10.21105/joss.04591</doi> | ||
<resource>https://joss.theoj.org/papers/10.21105/joss.04591</resource> | ||
<collection property="text-mining"> | ||
<item> | ||
<resource mime_type="application/pdf">https://joss.theoj.org/papers/10.21105/joss.04591.pdf</resource> | ||
</item> | ||
</collection> | ||
</doi_data> | ||
<citation_list> | ||
<citation key="audemard2009predicting"> | ||
<article_title>Predicting learnt clauses quality in modern | ||
SAT solvers</article_title> | ||
<author>Audemard</author> | ||
<journal_title>International joint conference on artificial | ||
intelligence</journal_title> | ||
<cYear>2009</cYear> | ||
<unstructured_citation>Audemard, G., & Simon, L. (2009). | ||
Predicting learnt clauses quality in modern SAT solvers. International | ||
Joint Conference on Artificial Intelligence, | ||
399–404.</unstructured_citation> | ||
</citation> | ||
<citation key="biere2020cadical"> | ||
<article_title>CaDiCaL, kissat, paracooba, plingeling and | ||
treengeling entering the SAT competition 2020</article_title> | ||
<author>Biere</author> | ||
<journal_title>SAT Competition 2020</journal_title> | ||
<cYear>2020</cYear> | ||
<unstructured_citation>Biere, A., Fazekas, K., Fleury, M., | ||
& Heisinger, M. (2020). CaDiCaL, kissat, paracooba, plingeling and | ||
treengeling entering the SAT competition 2020. SAT Competition 2020, | ||
50.</unstructured_citation> | ||
</citation> | ||
<citation key="biere2017cadical"> | ||
<article_title>Cadical, lingeling, plingeling, treengeling | ||
and yalsat entering the SAT competition 2018</article_title> | ||
<author>Biere</author> | ||
<journal_title>SAT Competition</journal_title> | ||
<cYear>2017</cYear> | ||
<unstructured_citation>Biere, A. (2017). Cadical, lingeling, | ||
plingeling, treengeling and yalsat entering the SAT competition 2018. | ||
SAT Competition, 14–15.</unstructured_citation> | ||
</citation> | ||
<citation key="cook1971complexity"> | ||
<article_title>The complexity of theorem-proving | ||
procedures</article_title> | ||
<author>Cook</author> | ||
<journal_title>ACM symposium on theory of | ||
computing</journal_title> | ||
<doi>10.7551/mitpress/12274.003.0036</doi> | ||
<cYear>1971</cYear> | ||
<unstructured_citation>Cook, S. A. (1971). The complexity of | ||
theorem-proving procedures. ACM Symposium on Theory of Computing, | ||
151–158. | ||
https://doi.org/10.7551/mitpress/12274.003.0036</unstructured_citation> | ||
</citation> | ||
<citation key="feitelson1997job"> | ||
<article_title>Job scheduling in multiprogrammed parallel | ||
systems</article_title> | ||
<author>Feitelson</author> | ||
<cYear>1997</cYear> | ||
<unstructured_citation>Feitelson, D. G. (1997). Job | ||
scheduling in multiprogrammed parallel systems.</unstructured_citation> | ||
</citation> | ||
<citation key="goldberg2001using"> | ||
<article_title>Using SAT for combinational equivalence | ||
checking</article_title> | ||
<author>Goldberg</author> | ||
<journal_title>Proceedings design, automation and test in | ||
europe. Conference and exhibition 2001</journal_title> | ||
<doi>10.1109/date.2001.915010</doi> | ||
<cYear>2001</cYear> | ||
<unstructured_citation>Goldberg, E. I., Prasad, M. R., & | ||
Brayton, R. K. (2001). Using SAT for combinational equivalence checking. | ||
Proceedings Design, Automation and Test in Europe. Conference and | ||
Exhibition 2001, 114–121. | ||
https://doi.org/10.1109/date.2001.915010</unstructured_citation> | ||
</citation> | ||
<citation key="hamadi2012seven"> | ||
<article_title>Seven challenges in parallel SAT | ||
solving</article_title> | ||
<author>Hamadi</author> | ||
<journal_title>Proceedings of the AAAI conference on | ||
artificial intelligence</journal_title> | ||
<volume>26</volume> | ||
<doi>10.1609/aimag.v34i2.2450</doi> | ||
<cYear>2012</cYear> | ||
<unstructured_citation>Hamadi, Y., & Wintersteiger, C. | ||
(2012). Seven challenges in parallel SAT solving. Proceedings of the | ||
AAAI Conference on Artificial Intelligence, 26, 2120–2125. | ||
https://doi.org/10.1609/aimag.v34i2.2450</unstructured_citation> | ||
</citation> | ||
<citation key="heule2016solving"> | ||
<article_title>Solving and verifying the boolean pythagorean | ||
triples problem via cube-and-conquer</article_title> | ||
<author>Heule</author> | ||
<journal_title>International conference on theory and | ||
applications of satisfiability testing</journal_title> | ||
<doi>10.1007/978-3-319-40970-2_15</doi> | ||
<cYear>2016</cYear> | ||
<unstructured_citation>Heule, M. J., Kullmann, O., & | ||
Marek, V. W. (2016). Solving and verifying the boolean pythagorean | ||
triples problem via cube-and-conquer. International Conference on Theory | ||
and Applications of Satisfiability Testing, 228–245. | ||
https://doi.org/10.1007/978-3-319-40970-2_15</unstructured_citation> | ||
</citation> | ||
<citation key="buning2019using"> | ||
<article_title>Using DimSpec for bounded and unbounded | ||
software model checking</article_title> | ||
<author>Kleine-Büning</author> | ||
<journal_title>International conference on formal | ||
engineering methods</journal_title> | ||
<doi>10.1007/978-3-030-32409-4_2</doi> | ||
<cYear>2019</cYear> | ||
<unstructured_citation>Kleine-Büning, M., Balyo, T., & | ||
Sinz, C. (2019). Using DimSpec for bounded and unbounded software model | ||
checking. International Conference on Formal Engineering Methods, 19–35. | ||
https://doi.org/10.1007/978-3-030-32409-4_2</unstructured_citation> | ||
</citation> | ||
<citation key="froleyks2021sat"> | ||
<article_title>SAT competition 2020</article_title> | ||
<author>Froleyks</author> | ||
<journal_title>Artificial Intelligence</journal_title> | ||
<volume>301</volume> | ||
<doi>10.1016/j.artint.2021.103572</doi> | ||
<cYear>2021</cYear> | ||
<unstructured_citation>Froleyks, N., Heule, M., Iser, M., | ||
Järvisalo, M., & Suda, M. (2021). SAT competition 2020. Artificial | ||
Intelligence, 301, 103572. | ||
https://doi.org/10.1016/j.artint.2021.103572</unstructured_citation> | ||
</citation> | ||
<citation key="balyo2021results"> | ||
<article_title>The results of SAT competition | ||
2021</article_title> | ||
<author>Balyo</author> | ||
<cYear>2021</cYear> | ||
<unstructured_citation>Balyo, T., Froleyks, N., Heule, M. | ||
J., Iser, M., Järvisalo, M., & Suda, M. (2021). The results of SAT | ||
competition 2021. | ||
https://satcompetition.github.io/2021/slides/ISC2021-fixed.pdf</unstructured_citation> | ||
</citation> | ||
<citation key="massacci2000logical"> | ||
<article_title>Logical cryptanalysis as a SAT | ||
problem</article_title> | ||
<author>Massacci</author> | ||
<journal_title>Journal of Automated | ||
Reasoning</journal_title> | ||
<issue>1</issue> | ||
<volume>24</volume> | ||
<cYear>2000</cYear> | ||
<unstructured_citation>Massacci, F., & Marraro, L. | ||
(2000). Logical cryptanalysis as a SAT problem. Journal of Automated | ||
Reasoning, 24(1), 165–203.</unstructured_citation> | ||
</citation> | ||
<citation key="sanders2022artifact"> | ||
<article_title>Artifact and instructions to generate | ||
experimental results for the Euro-Par 2022 paper: “Decentralized Online | ||
Scheduling of Malleable NP-hard Jobs”</article_title> | ||
<author>Sanders</author> | ||
<doi>10.6084/m9.figshare.20000642</doi> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Sanders, P., & Schreiber, D. | ||
(2022). Artifact and instructions to generate experimental results for | ||
the Euro-Par 2022 paper: “Decentralized Online Scheduling of Malleable | ||
NP-hard Jobs”. | ||
https://doi.org/10.6084/m9.figshare.20000642</unstructured_citation> | ||
</citation> | ||
<citation key="sanders2022decentralized"> | ||
<article_title>Decentralized online scheduling of malleable | ||
NP-hard jobs</article_title> | ||
<author>Sanders</author> | ||
<journal_title>European international conference on parallel | ||
processing</journal_title> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Sanders, P., & Schreiber, D. | ||
(2022). Decentralized online scheduling of malleable NP-hard jobs. | ||
European International Conference on Parallel | ||
Processing.</unstructured_citation> | ||
</citation> | ||
<citation key="schreiber2021lilotane"> | ||
<article_title>Lilotane: A lifted SAT-based approach to | ||
hierarchical planning</article_title> | ||
<author>Schreiber</author> | ||
<journal_title>Journal of Artificial Intelligence | ||
Research</journal_title> | ||
<volume>70</volume> | ||
<doi>10.1613/jair.1.12520</doi> | ||
<cYear>2021</cYear> | ||
<unstructured_citation>Schreiber, D. (2021). Lilotane: A | ||
lifted SAT-based approach to hierarchical planning. Journal of | ||
Artificial Intelligence Research, 70, 1117–1181. | ||
https://doi.org/10.1613/jair.1.12520</unstructured_citation> | ||
</citation> | ||
<citation key="schreiber2021scalable"> | ||
<article_title>Scalable SAT solving in the | ||
cloud</article_title> | ||
<author>Schreiber</author> | ||
<journal_title>International conference on theory and | ||
applications of satisfiability testing</journal_title> | ||
<doi>10.1007/978-3-030-80223-3_35</doi> | ||
<cYear>2021</cYear> | ||
<unstructured_citation>Schreiber, D., & Sanders, P. | ||
(2021). Scalable SAT solving in the cloud. International Conference on | ||
Theory and Applications of Satisfiability Testing, 518–534. | ||
https://doi.org/10.1007/978-3-030-80223-3_35</unstructured_citation> | ||
</citation> | ||
<citation key="cook2022automated"> | ||
<article_title>Automated reasoning’s scientific | ||
frontiers</article_title> | ||
<author>Cook</author> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Cook, B. (2022). Automated | ||
reasoning’s scientific frontiers. Amazon Science. | ||
https://www.amazon.science/blog/automated-reasonings-scientific-frontiers</unstructured_citation> | ||
</citation> | ||
<citation key="dusikova2022compile"> | ||
<article_title>Compile time regular | ||
expressions</article_title> | ||
<author>Dusíková</author> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Dusíková, H. (2022). Compile time | ||
regular expressions. | ||
https://github.com/hanickadot/compile-time-regular-expressions</unstructured_citation> | ||
</citation> | ||
<citation key="ankerl2022robin"> | ||
<article_title>robin_hood unordered map & | ||
set</article_title> | ||
<author>Ankerl</author> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Ankerl, M. (2022). robin_hood | ||
unordered map & set. | ||
https://github.com/martinus/robin-hood-hashing</unstructured_citation> | ||
</citation> | ||
<citation key="goetghebuer2022implementation"> | ||
<article_title>A C++ implementation of a fast hash map and | ||
hash set using robin hood hashing</article_title> | ||
<author>Goetghebuer-Planchon</author> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Goetghebuer-Planchon, T. (2022). A | ||
C++ implementation of a fast hash map and hash set using robin hood | ||
hashing. https://github.com/Tessil/robin-map</unstructured_citation> | ||
</citation> | ||
<citation key="lohmann2022json"> | ||
<article_title>JSON for modern C++</article_title> | ||
<author>Lohmann</author> | ||
<cYear>2022</cYear> | ||
<unstructured_citation>Lohmann, N. (2022). JSON for modern | ||
C++. https://github.com/nlohmann/json</unstructured_citation> | ||
</citation> | ||
<citation key="balyo2015hordesat"> | ||
<article_title>Hordesat: A massively parallel portfolio SAT | ||
solver</article_title> | ||
<author>Balyo</author> | ||
<journal_title>International conference on theory and | ||
applications of satisfiability testing</journal_title> | ||
<doi>10.1007/978-3-319-24318-4_12</doi> | ||
<cYear>2015</cYear> | ||
<unstructured_citation>Balyo, T., Sanders, P., & Sinz, | ||
C. (2015). Hordesat: A massively parallel portfolio SAT solver. | ||
International Conference on Theory and Applications of Satisfiability | ||
Testing, 156–172. | ||
https://doi.org/10.1007/978-3-319-24318-4_12</unstructured_citation> | ||
</citation> | ||
<citation key="een2003extensible"> | ||
<article_title>An extensible SAT-solver</article_title> | ||
<author>Eén</author> | ||
<journal_title>International conference on theory and | ||
applications of satisfiability testing</journal_title> | ||
<doi>10.1007/978-3-540-24605-3_37</doi> | ||
<cYear>2003</cYear> | ||
<unstructured_citation>Eén, N., & Sörensson, N. (2003). | ||
An extensible SAT-solver. International Conference on Theory and | ||
Applications of Satisfiability Testing, 502–518. | ||
https://doi.org/10.1007/978-3-540-24605-3_37</unstructured_citation> | ||
</citation> | ||
<citation key="schreiber2020engineering"> | ||
<article_title>Engineering HordeSat towards malleability: | ||
Mallob-mono in the SAT 2020 cloud track</article_title> | ||
<author>Schreiber</author> | ||
<journal_title>SAT Competition 2020</journal_title> | ||
<cYear>2020</cYear> | ||
<unstructured_citation>Schreiber, D. (2020). Engineering | ||
HordeSat towards malleability: Mallob-mono in the SAT 2020 cloud track. | ||
SAT Competition 2020, 45.</unstructured_citation> | ||
</citation> | ||
<citation key="schreiber2021mallob"> | ||
<article_title>Mallob in the SAT competition | ||
2021</article_title> | ||
<author>Schreiber</author> | ||
<journal_title>SAT Competition 2021</journal_title> | ||
<cYear>2021</cYear> | ||
<unstructured_citation>Schreiber, D. (2021). Mallob in the | ||
SAT competition 2021. SAT Competition 2021, 38.</unstructured_citation> | ||
</citation> | ||
</citation_list> | ||
</journal_article> | ||
</journal> | ||
</body> | ||
</doi_batch> |
Oops, something went wrong.