Pith. sign in

REVIEW 2 major objections 4 minor 24 references

Design and Results of the Second International Competition on Computational Models of Argumentation

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper reports the design and results of the second International Competition on Computational Models of Argumentation, stating that under its scoring and verification procedure pyglaf won the complete, stable, and ideal semantics…

desk verdict A thorough, transparent ICCMA'17 report whose D3 prize call is one unchecked answer away from being wrong—worth refereeing, but the organizers should re-examine their own verification claim. read the letter →

arxiv 1909.00621 v1 pith:BWR3JLEB submitted 2019-09-02 cs.AI

Sarah A. Gaggl , Thomas Linsbichler , Marco Maratea , Stefan Woltran This is my paper · ORCID
classification cs.AI
keywords abstractargumentationsolvercompetitionICCMA'17semanticsbenchmarkselectionevaluationcomputationallogicDung'striathlon
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper reports on the second International Competition on Computational Models of Argumentation, a benchmark contest for solvers that compute with abstract argumentation frameworks. It establishes who won each track under the competition's own rules and argues that those results are meaningful because of three design features: a call for benchmarks, a hardness-based instance selection stage, and a scoring scheme that penalizes wrong answers. The winners are pyglaf for complete, stable, and ideal semantics; argmat-sat for semi-stable and stage semantics; ArgSemSAT for preferred; CoQuiAAS for grounded; and argmat-dvisat for Dung's Triathlon. The reason to care is that the competition is the main instrument for measuring progress in this area of AI, and the paper's comparison with the 2015 edition shows where solver technology has improved and where it has not.

What carries the argument

The central object is the abstract argumentation framework, a directed graph in which nodes are arguments and edges are attacks, together with the seven semantics under evaluation: complete, preferred, stable, semi-stable, stage, grounded, and ideal. The machinery that carries the argument is the competition protocol: 24 tasks grouped into five hardness classes (A to E), a benchmark suite of 3990 instances across 11 domains, a selection stage that classifies instances from very easy to too hard using reference solvers from the 2015 edition, a scoring rule of +1 per correct answer and -5 per wrong answer with ties broken by cumulative runtime, and an answer-verification pipeline based on ASPARTIX-D reference solutions, extension-checking encodings, and majority agreement.

What would settle it

Re-score the competition after replacing each unverifiable answer with 0 points instead of 1 point and independently checking the instances for which the reference solver produced no answer; if any track's top solver changes under either operation, the reported winner list is not robust to the verification rule.

Watch

Extended reading notes

Core claim

The central claim is that the second International Competition on Computational Models of Argumentation was run as designed and that its recorded winners are correct under that design. The paper describes the verification pipeline: reference solutions were generated with ASPARTIX-D, single extensions were checked with dedicated ASP encodings, and the few answers that could not be checked were resolved by majority agreement; only about 0.1% of the 105,350 submitted solutions could not be verified, and the paper states that these did not influence any track ranking. The reported winners are pyglaf for complete, stable, and ideal semantics; argmat-sat for semi-stable and stage semantics; ArgSemSAT for preferred; CoQuiAAS for grounded; and argmat-dvisat for Dung's Triathlon. On the competition's common tracks with 2015, the comparison shows mixed progress: some 2017 winners outperform their predecessors, while others remain comparable or even behind.

Load-bearing premise

The whole ranking depends on the assumption that how hard an instance is for the representative enumeration tasks (enumerating preferred extensions, enumerating stable extensions, and finding one grounded extension) predicts how hard it is for every other task in the same group, including the newly added semi-stable, stage, and ideal tasks that were assigned to the same benchmark set without their own difficulty classification.

Editorial extensions

If this is right

  • The winners become the reference points that future solvers must beat on their respective tracks.
  • The scoring scheme with a -5 penalty for wrong answers pushes unreliable solvers to the bottom of the rankings, so the rule can be retained to discourage guessing.
  • The hardness-based instance selection gives a reproducible way to build a balanced benchmark set, so future editions can apply the same classification procedure to new domains.
  • The common-track comparison shows that progress between 2015 and 2017 is uneven: some 2017 winners clearly outperform their predecessors, while others are comparable or slightly worse.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper's claims, the transferability of the benchmark classification can be tested directly by running a dedicated hardness classification for the semi-stable and stage tasks and comparing it with the group A classification; if the distributions differ, the rankings for the new semantics are shaped by the benchmark choice rather than by solver strength.
  • Beyond the paper's claims, the verification rule can be stress-tested by re-scoring all submitted answers with 0 points for the unverifiable cases instead of 1 point; a changed ordering in any track would show that the winner list is sensitive to the verification rule.
  • Beyond the paper's claims, the 2015-versus-2017 comparison can be extended to the new semantics by running the 2015 winners on the semi-stable, stage, and ideal benchmarks, yielding a complete two-year progress picture.
  • Beyond the paper's claims, the Dung's Triathlon idea can be generalized to other triples of semantics at different complexity levels, such as semi-stable, stage, and ideal, to see whether exploiting inter-semantics relationships transfers beyond the original trio.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. This paper reports the design and results of the Second International Competition on Computational Models of Argumentation (ICCMA'17), covering the task/track structure, the benchmark suite and call for benchmarks, the hardness-based instance selection, the scoring scheme with a -5 penalty for wrong answers, the answer verification procedure, the 16 participating solvers, and the per-track results and awards. The main claims are the listed winners: pyglaf for CO, ST, and ID; argmat-sat for SST and STG; ArgSemSAT for PR; CoQuiAAS for GR; and argmat-dvisat for the Dung's Triathlon (D3). The paper also compares the 2017 winners with the best ICCMA'15 solvers on common tasks.

Significance. If the reported results are accurate, this paper is a useful archival record for the argumentation-solver community and a methodological reference for future competitions. Its strengths are transparency and reproducibility: the verification chain is described in detail (ASPARTIX-D reference solutions, publicly available ASP encodings for checking SE/EE answers, and a majority-vote fallback for the small fraction of unverifiable cases), and the benchmark selection procedure is specified with enough detail to be re-run. The paper also reports per-solver correct/wrong/timeout/unverified counts, which is the right level of detail for a competition report. However, the archival value depends on the reliability of the awards; the D3 award is currently not supported by the verified data as presented, so the winners list needs correction before the paper can be accepted.

major comments (2)
  1. [Section 3.4 and Section 7.1 (D3 results, Figure 9)] Section 3.4 states that the approximately 0.1% of solutions that could not be verified were 'rated with 1 point' and that 'in none of the tracks these had an influence on the ranking of the solvers.' The D3 results in Figure 9 contradict this claim. argmat-dvisat is reported as the D3 winner with 276 points against pyglaf's 275, while the table lists 5 unchecked USC for argmat-dvisat and 1 unchecked USC for pyglaf. Because unverified solutions were counted as 1 point each, excluding them gives pyglaf 274 verified points and argmat-dvisat 271 verified points; if any single one of argmat-dvisat's five unverified answers were in fact wrong, the -5 penalty would reduce its score below pyglaf's. The reported D3 winner is therefore not robustly established by the data as presented. Please verify the five unchecked USC of argmat-dvisat, or withdraw/qualify the D3 award, and correct the Section 3.4 claim that no track was affected by unverified solutions.
  2. [Section 5.1-5.2 (benchmark selection for groups D and E)] The benchmark sets for the new SST, STG, and ID tasks are inherited from task group A, whose hardness classification was performed only for the representative enumeration task EE-PR. The paper asserts that enumeration tasks are representative because decision-task difficulty depends on the queried argument, but it provides no evidence that EE-PR hardness predicts difficulty for the newly introduced SST/STG/ID tasks, which have different complexity profiles and were not present in ICCMA'15. Since the reported winners for these semantics (argmat-sat in SST and STG, pyglaf in ID) are central claims, I ask the authors to either state explicitly and prominently that these rankings are conditional on benchmarks selected by EE-PR hardness, or provide a robustness check (for example, re-ranking the top solvers on benchmarks selected under an alternative classification).
minor comments (4)
  1. [Section 3.4 / 7.1] Please clarify whether the 'Correct' counts in the result tables include the unverified solutions that were 'rated with 1 point'; this ambiguity is what makes the D3 margin difficult to interpret from the tables alone.
  2. [Section 5.2 (No stable extensions)] The sentence 'for 22 instances no answer is provided by ASPARTIX-D' should be tied to the subsequent count: please state explicitly that these 22 instances are not included in the 114 instances classified as having no stable extensions, or explain how they were treated.
  3. [Acknowledgments] There is a typo: 'usefull comments' should be 'useful comments.'
  4. [Section 7.1] The phrase 'It is also worth to be noted' is ungrammatical; consider 'It is also worth noting.'

Circularity Check

0 steps flagged · score 1.0 of 10

No substantive circularity; the competition results come from actual solver runs, but the paper's own verification note conflicts with the D3 table.

full rationale

This paper is an empirical competition report, so there is no derivation chain whose outputs reduce to its inputs. The reported winners are sums of points obtained from actual solver executions under the Section 3 scoring rules; those scores are not fitted to the winner list. The benchmark selection does use ICCMA'15 solvers to classify instance hardness (Section 5.1), and the paper itself flags this as a possible bias ('With this choice, the risk is to have a selection biased toward the performance of such systems'), but that is a standard external-validity limitation, not circularity, because the 2017 participant rankings are generated by fresh runs on the selected instances. Self-citations (Gaggl et al. 2016, 2018; ASPARTIX-D references) are provenance or tool references rather than load-bearing evidence for the rankings; ASPARTIX-D is used only as a non-participating verifier. One manuscript-internal inconsistency should be flagged explicitly under the review rule, though it does not affect the circularity score: Section 3.4 states 'In none of the tracks these had an influence on the ranking of the solvers' about unverified solutions, but the D3 table in Figure 9 lists argmat-dvisat at 276 points against pyglaf's 275 while argmat-dvisat carries 5 unchecked USC and pyglaf carries 1; a single false-positive among those unverified answers would change the D3 winner. This is a verification robustness/correctness concern, not a circularity, so the overall circularity score remains minimal.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The central claim (competition winners) rests on the actual execution of the competition and the verification of answers. The listed free parameters are explicit design choices. The key ad hoc assumption is the representativeness of enumeration tasks for benchmark classification, which is load-bearing for the fairness of the selected benchmark set.

free parameters (4)
  • Scoring penalty for incorrect answers = -5 points
    Chosen by organizers to emphasize correctness; different penalties would change rankings.
  • Hardness classification time thresholds = 6s / 60s / 10min / 20min
    Hand-selected thresholds for very easy, easy, medium, hard, and too hard categories; directly determines benchmark selection.
  • Benchmark selection distribution = 50 very easy, 50 easy, 100 medium, 100 hard, 50 too hard per task group
    Fixed distribution over hardness categories for the 350 instances per group; affects the composition of the test set.
  • Time and memory limits = 10 min / 4 GB (30 min / 6.5 GB for D3)
    Limits affect timeouts and thus scores; chosen by organizers.
assumptions (4)
  • standard math Abstract argumentation framework definitions and semantics are as established in Dung (1995) and related literature.
    Background used throughout the paper without proof.
  • domain assumption Semi-stable, stage, and stable extensions coincide when a stable extension exists.
    Known result cited from Caminada et al. (2012); used in Section 5.2 to justify adding instances without stable extensions.
  • standard math Complexity results in Table 1 are correct.
    The paper relies on previously published complexity classifications.
  • ad hoc to paper Enumeration tasks are representative of task-group difficulty.
    Assumed in Section 5.1 to select representative tasks for benchmark classification; not independently validated.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Design and Results of the Second International Competition on Computational Models of Argumentation." pith.science (2026). https://pith.science/paper/BWR3JLEB

@misc{pith2026190900621,
  author       = {Pith},
  title        = {Pith review of: Design and Results of the Second International Competition on Computational Models of Argumentation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BWR3JLEB}},
  note         = {Machine review of arXiv:1909.00621}
}
read the original abstract

Argumentation is a major topic in the study of Artificial Intelligence. Since the first edition in 2015, advancements in solving (abstract) argumentation frameworks are assessed in competition events, similar to other closely related problem solving technologies. In this paper, we report about the design and results of the Second International Competition on Computational Models of Argumentation, which has been jointly organized by TU Dresden (Germany), TU Wien (Austria), and the University of Genova (Italy), in affiliation with the 2017 International Workshop on Theory and Applications of Formal Argumentation. This second edition maintains some of the design choices made in the first event, e.g. the I/O formats, the basic reasoning problems, and the organization into tasks and tracks. At the same time, it introduces significant novelties, e.g. three additional prominent semantics, and an instance selection stage for classifying instances according to their empirical hardness.

Figures

Figures reproduced from arXiv: 1909.00621 by the authors.

Figure 1
Figure 1. An argumentation framework. F is depicted in [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. CO track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 31 [PITH_FULL_IMAGE:figures/full_fig_p031_2.png] view at source ↗
Figure 3
Figure 3. PR track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 33 [PITH_FULL_IMAGE:figures/full_fig_p033_3.png] view at source ↗
Figures from the paper (13 more)
Figure 4
Figure 4. Figure 4: ST track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 34 [PITH_FULL_IMAGE:figures/full_fig_p034_4.png]
Figure 5
Figure 5. Figure 5: SST track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 35 [PITH_FULL_IMAGE:figures/full_fig_p035_5.png]
Figure 6
Figure 6. Figure 6: STG track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 36 [PITH_FULL_IMAGE:figures/full_fig_p036_6.png]
Figure 7
Figure 7. Figure 7: GR track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 37 [PITH_FULL_IMAGE:figures/full_fig_p037_7.png]
Figure 8
Figure 8. Figure 8: ID track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 38 [PITH_FULL_IMAGE:figures/full_fig_p038_8.png]
Figure 9
Figure 9. Figure 9: D3 track: Ranking of solvers (top). Cactus plot of runtimes (bottom). 39 [PITH_FULL_IMAGE:figures/full_fig_p039_9.png]
Figure 10
Figure 10. Figure 10: CO track, DC and DS tasks: Comparison between ASPARTIX-D (2015) and pyglaf (2017). 8. Related Competitions This section discusses how the introduced novelties in this year competition are treated in related competitions. A paragraph is devoted to each of such novel￾ti…
Figure 11
Figure 11. Figure 11: CO track, SE and EE tasks: Comparison between ASPARTIX-D (2015) and pyglaf (2017.) tion, possibly having a more heterogeneous set. As we can note from Section 4.2, the response from the community was positive. Call for benchmarks are custom￾ary in other close competit…
Figure 12
Figure 12. Figure 12: PR track, DC and DS tasks: Comparison between ArgSemSAT (2015) and ArgSem￾SAT (2017). petitions (SAT-Comp; Jarvisalo et al., 2012; Balint et al., 2015; Gebser et al., ¨ 2017). The main differences in our benchmark selection, some of them due to the intrinsic character…
Figure 13
Figure 13. Figure 13: PR track, SE and EE tasks: Comparison between ArgSemSAT (2015) and ArgSemSAT (2017). and 5.3. As far as solvers employed for the classification of the instances are concerned, in the 2014 IPC competition (Vallati et al., 2015) actual participant systems have been empl…
Figure 14
Figure 14. Figure 14: ST track, DC and DS tasks: Comparison between ASPARTIX-D (2015) and pyglaf (2017). Scoring schema. This edition’s scoring schema put focus on correctness by giv￾ing a high penalty to incorrect solutions. In the following, we briefly overview the general scoring rules …
Figure 15
Figure 15. Figure 15: ST track, SE and EE tasks: Comparison between ASPARTIX-D (2015) and pyglaf (2017). and Query problems a solver can be disqualified for the same reasons, but the disqualification is applied to the domain the instance belongs. The score of each domain on such problems i…
Figure 16
Figure 16. Figure 16: GR track, DC and SE tasks: Comparison between CoQuiAAs (2015) and CoQuiAAs (2017). two main metrics for scoring planners are the solving times and the “quality” of returned plan. In the deterministic track of the 2014 IPC competition focus was put toward plan’s qualit…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 21 canonical work pages

  1. [6]

    doi: 10.1016/j.artint.2014.11.008. David R. Cok, David D ´eharbe, and Tjark Weber. The 2014 SMT competi- tion. Journal on Satisfiability, Boolean Modeling and Computation, 9:207–242,

    work page doi:10.1016/j.artint.2014.11.008 2014

  2. [8]

    An extensible SAT-solver

    55 Niklas E ´en and Niklas S ¨orensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Proceedings of the 6th Interna- tional Conference on Theory and Applications of Satisfiability Testing (SAT 2003). Selected Revised Papers , volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer,

    work page 2003

  3. [9]

    The DIAMOND system for comput- ing with abstract dialectical frameworks

    Stefan Ellmauthaler and Hannes Strass. The DIAMOND system for comput- ing with abstract dialectical frameworks. In Simon Parsons, Nir Oren, Chris Reed, and Federico Cerutti, editors, Proceedings of the 5th International Con- ference on Computational Models of Argument (COMMA 2014), volume 266 of Frontiers in Artificial Intelligence and Applications, pages ...

    work page 2014

  4. [11]

    CEUR- WS.org,

    co-located with the 6th International Conference on Computational Models of Argument (COMMA 2016)., volume 1672 of CEUR Workshop Proceedings , pages 4–9. CEUR- WS.org,

    work page 2016

  5. [13]

    Heureka: A general heuristic backtracking solver for abstract argumentation

    Nils Geilen and Matthias Thimm. Heureka: A general heuristic backtracking solver for abstract argumentation. In Elizabeth Black, Sanjay Modgil, and Nir Oren, editors, Proceedings of the 4th International Workshop on Theory and Applications of Formal Argumentation (TAFA 2017). Revised Selected Papers, volume 10757 ofLecture Notes in Computer Science, pages...

    work page 2017

  6. [15]

    http://www.argumentationcompetition.org/2017/ SolverRequirements.pdf.,

    ICCMA’17-Solreq. http://www.argumentationcompetition.org/2017/ SolverRequirements.pdf.,

    work page 2017

  7. [16]

    http://www

    Tomi Jahunen and Shahab Tasharrofi. http://www. argumentationcompetition.org/2017/gg-sts.pdf.,

    work page 2017

  8. [17]

    Jean-Marie Lagniez, Emmanuel Lonca, and Jean-Guy Mailly

    doi: 10.24963/ijcai.2017/159. Jean-Marie Lagniez, Emmanuel Lonca, and Jean-Guy Mailly. CoQuiAAS: A constraint-based quick abstract argumentation solver. In Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), pages 928–935. IEEE Computer Society,

    work page doi:10.24963/ijcai.2017/159 2017

Show all 24 references
  1. [19]

    CEUR- WS.org,

    co-located with 19th Inter- national Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 1719 of CEUR Workshop Proceedings , pages 1–13. CEUR- WS.org,

    2016

  2. [20]

    http://www.satcompetition.org/ 2009/.,

    2009

  3. [21]

    Constraint propagation in propositional planning

    Andreas Sideris and Yannis Dimopoulos. Constraint propagation in propositional planning. In Ronen I. Brafman, Hector Geffner, J ¨org Hoffmann, and Henry A. Kautz, editors, Proceedings of the 20th International Conference on Automated Planning and Scheduling (ICAPS 2010), pages...

    2010

  4. [23]

    Matthias Thimm and Serena Villata

    URL http://arxiv.org/abs/1510.05373. Matthias Thimm and Serena Villata. The first international competition on compu- tational models of argumentation: Results and analysis. Artificial Intelligence, 252:267–294,

    arXiv

  5. [24]

    Mauro Vallati, Luk ´as Chrpa, Marek Grzes, Thomas Leo McCluskey, Mark Roberts, and Scott Sanner

    doi: 10.1080/19462166.2013.869878. Mauro Vallati, Luk ´as Chrpa, Marek Grzes, Thomas Leo McCluskey, Mark Roberts, and Scott Sanner. The 2014 international planning competition: Progress and trends. AI Magazine, 36(3):90–98,

    2013

  6. [25]

    On the combina- tion of argumentation solvers into parallel portfolios

    Mauro Vallati, Federico Cerutti, and Massimiliano Giacomin. On the combina- tion of argumentation solvers into parallel portfolios. In Wei Peng, Damminda 59 Alahakoon, and Xiaodong Li, editors, Advances in Artificial Intelligence - Pro- ceedings of the 30th Australasian Joint C...

    2017

  7. [26]

    URL https://doi.org/10.1007/s11225-009-9210-5

    doi: 10.1007/s11225-009-9210-5. URL https://doi.org/10.1007/s11225-009-9210-5 . Adam Z. Wyner, Trevor J. M. Bench-Capon, Paul E. Dunne, and Federico Cerutti. Senses of ’argument’ in instantiated argumentation frameworks. Argument & Computation, 6(1):50–72,

    doi

  8. [1959]

    Solving set optimization problems by cardinality optimization with an applica- tion to argumentation

    Wolfgang Faber, Mauro Vallati, Federico Cerutti, and Massimiliano Giacomin. Solving set optimization problems by cardinality optimization with an applica- tion to argumentation. In Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke H¨ullermeier, Virginia Dignum, Frank Dignum, and ...

    2016

  9. [2006]

    http://www.argumentationcompetition.org/2017/ submissions.html.,

    ICCMA’17-Soldes. http://www.argumentationcompetition.org/2017/ submissions.html.,

    2017

  10. [2009]

    Overview and analysis of the SAT challenge 2012 solver competition

    Adrian Balint, Anton Belov, Matti J ¨arvisalo, and Carsten Sinz. Overview and analysis of the SAT challenge 2012 solver competition. Artificial Intelligence, 223:120–155,

    2012

  11. [2010]

    Federico Cerutti, Massimiliano Giacomin, and Mauro Vallati

    Available at http://bnaic2010.uni.lu/proceedings.html. Federico Cerutti, Massimiliano Giacomin, and Mauro Vallati. ArgSemSAT: Solv- ing argumentation problems using SAT. In Simon Parsons, Nir Oren, Chris Reed, and Federico Cerutti, editors, Proceedings of the 5th International...

  12. [2013]

    2013.06.004

    doi: 10.1016/j.artint. 2013.06.004. Wolfgang Dvoˇr´ak, Matti J ¨arvisalo, Johannes Peter Wallner, and Stefan Woltran. Complexity-sensitive decision procedures for abstract argumentation. Artificial Intelligence, 206:53–78,

    2013 doi

  13. [2015]

    Stefano Bistarelli, Fabio Rossi, and Francesco Santini

    doi: 10.3233/FI-2015-1254. Stefano Bistarelli, Fabio Rossi, and Francesco Santini. Not only size, but also shape counts: abstract argumentation solvers are benchmark-sensitive. Journal of Logic and Computation, 28(1):85–117,

    2015 doi

  14. [2016]

    CEUR-WS.org,

    co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016),, volume 1719 of CEUR Workshop Proceed- ings, pages 49–54. CEUR-WS.org,

    2016

  15. [2017]

    Predicting learnt clauses quality in modern SAT solvers

    51 Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pages 399–404,

    2009

  16. [2018]

    Clingo = ASP + control: Preliminary report

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Clingo = ASP + control: Preliminary report. CoRR, abs/1405.3694,

    arXiv

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.