Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Creating pull request for 10.21105.joss.04591 #3419

Merged
merged 3 commits into from
Aug 9, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
380 changes: 380 additions & 0 deletions joss.04591/10.21105.joss.04591.crossref.xml
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., &amp; 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.,
&amp; 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., &amp;
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., &amp; 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., &amp;
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., &amp;
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., &amp; 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., &amp; 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., &amp; 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., &amp; 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., &amp; 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., &amp; 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 &amp;
set</article_title>
<author>Ankerl</author>
<cYear>2022</cYear>
<unstructured_citation>Ankerl, M. (2022). robin_hood
unordered map &amp; 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., &amp; 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., &amp; 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>
Loading