Skip to content

chore(pumpkin-solver): Streamline the solver --help output and MiniZinc flag description #627

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.

Sign up for GitHub

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

Open
ImkoMarijnissen wants to merge 9 commits into
base: main
Choose a base branch
from
Open

chore(pumpkin-solver): Streamline the solver --help output and MiniZinc flag description #627

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
15b67c0
refactor: streamline the argument descriptions + MiniZinc flag descri…
ImkoMarijnissen Oct 22, 2026
bbdc725
refactor: clap-style defaults and possible values uses int
ImkoMarijnissen Oct 22, 2026
0b46544
refactor: give categories to the flags
ImkoMarijnissen Oct 22, 2026
51f5ae7
refactor: remove Max(SAT) flags from the .msc files
ImkoMarijnissen Oct 22, 2026
7f7745a
chore: args doc cleanup
ImkoMarijnissen Oct 22, 2026
51d3c4d
chore: update clearer value names
ImkoMarijnissen Oct 22, 2026
f47f6d0
chore: clean up docs
ImkoMarijnissen Oct 22, 2026
a37c276
chore: further cleanup for short help
ImkoMarijnissen Oct 22, 2026
a2ca3e9
chore: make requirements between flags explicit
ImkoMarijnissen Oct 22, 2026
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
154 changes: 68 additions & 86 deletions minizinc/pumpkin-for-proofs.msc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,185 +7,167 @@
"stdFlags": [
"-t",
"-r",
"-a",
"-v",
"-s",
"-f",
"-a"
"-f"
],
"extraFlags": [
[
"--proof-path",
"The output path for the proof file.\n\nWhen solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP\nproof is logged.\n\nIn case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be\nproduced.",
"The output path for the proof file. [possible values: string]",
"string",
""
],
[
"--proof-type",
"What type of proof to log.\n\nIf the `proof_path` option is not provided, this is ignored.",
"What type of proof to log. [default: scaffold] [possible values: scaffold, full]",
"opt:scaffold:full",
"scaffold"
],
[
"--optimisation-strategy",
"Determines what type of optimisation strategy is used by the solver. [default: linear-sat-unsat] [possible values: linear-sat-unsat, linear-unsat-sat]",
"opt:linear-sat-unsat:linear-unsat-sat",
"linear-sat-unsat"
],
[
"--conflict-resolver",
"Determines the conflict resolver. [default: one-uip] [possible values: no-learning, one-uip, all-decision, extended-cpip, bounds-extended-cpip]",
"opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip",
"one-uip"
],
[
"--recursive-minimisation",
"Enables recursive minimisation of learned nogoods.",
"bool",
"false"
],
[
"--no-iterative-minimisation",
"Disables semantic minimisation of learned nogoods during conflict analysis.",
"bool",
"false"
],
[
"--learning-max-num-high-lbd-nogoods",
"The number of high-lbd learned nogoods that are kept in the database.\n\nLearned nogoods are kept based on the tiered system introduced in \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\".\n\nPossible values: usize",
"The number of high-lbd learned nogoods that are kept in the database. [default: 20000] [possible values: int]",
"int:0:18446744073709551615",
"20000"
],
[
"--learning-max-num-mid-lbd-nogoods",
"The number of mid-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize",
"The number of mid-lbd learned nogoods that are kept in the database. [default: 7000] [possible values: int]",
"int:0:18446744073709551615",
"7000"
],
[
"--learning-max-num-low-lbd-nogoods",
"The number of low-lbd learned nogoods that are kept in the database.\n\nThis is based on the variation of the three-tiered system proposed in\n\"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: usize",
"The number of low-lbd learned nogoods that are kept in the database. [default: 100000] [possible values: int]",
"int:0:18446744073709551615",
"100000"
],
[
"--learning-low-lbd-threshold",
"The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"Low\" LBD nogood are kept around for longer since they are of better \"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32",
"The threshold determining whether a learned nogood is \"low\" LBD. [default: 3] [possible values: int]",
"int:0:4294967295",
"3"
],
[
"--learning-high-lbd-threshold",
"The treshold determining whether a learned nogood is \"low\" LBD.\n\n\"High\" LBD nogood are kept around for a shorter amount of time since they are of bad\n\"quality\".\n\nLearned nogoods are kept based on the tiered system introduced \"Improving\nSAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)\"\nwith the variation from \"Improving Implementation of SAT Competitions 2017–2019 Winners\".\n\nPossible values: u32",
"The threshold determining whether a learned nogood is \"high\" LBD. [default: 7] [possible values: int]",
"int:0:4294967295",
"7"
],
[
"--recursive-minimisation",
"Decides whether learned clauses are minimised as a post-processing step after computing the\n1-UIP Minimisation is done; according to the idea proposed in \"Generalized Conflict-Clause\nStrengthening for Satisfiability Solvers - Allen van Gelder (2011)\".\n\nPossible values: bool",
"bool",
"false"
"--memory-preallocated",
"The amount of memory (in MB) that is preallocated for storing nogoods. [default: 50] [possible values: int]",
"int:0:18446744073709551615",
"50"
],
[
"--no-iterative-minimisation",
"Decides whether to apply semantic minimisation during conflict analysis; according to the\nidea proposed in \"Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)\".\n\nIf this flag is present then the minimisation is turned on.\n\nPossible values: bool",
"--nogood-priority",
"The priority of the nogood propagator. [default: very-low] [possible values: high, medium, low, very-low, ultra-low, lowest]",
"opt:high:medium:low:very-low:ultra-low:lowest",
"very-low"
],
[
"--no-restarts",
"Determines that no restarts are allowed by the solver.",
"bool",
"false"
],
[
"--restart-sequence-generator-type",
"Decides the sequence based on which the restarts are performed.\n\n- The \"constant\" approach uses a constant number of conflicts before another restart is triggered - The \"geometric\" approach uses a geometrically increasing sequence - The \"luby\" approach uses a recursive sequence of the form 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2.... (see \"Optimal speedup of Las Vegas algorithms - Luby et al. (1993)\")\n\nTo be used in combination with \"--restarts-base-interval\".",
"Decides the sequence based on which the restarts are performed. [default: constant] [possible values: constant, geometric, luby]",
"opt:constant:geometric:luby",
"constant"
],
[
"--restart-base-interval",
"The base interval length is used as a multiplier to the restart sequence.\n- In the case of the \"constant\" restart sequence this argument indicates the constant which\n is used to determine when a restart occurs\n- For the \"geometric\" approach this argument indicates the starting value of the sequence\n- For the \"luby\" approach, the sequence is multiplied by this value\n\nFor example, constant restarts with base interval 50 means a restart is triggered every 50\nconflicts.\n\nPossible values: u64",
"The base interval length which is used as a multiplier to the restart sequence. [default: 50] [possible values: int]",
"int:0:18446744073709551615",
"50"
],
[
"--restart-geometric-coef",
"The coefficient of the geometric restart sequence. [possible values: float]",
"float",
""
],
[
"--restart-min-initial-conflicts",
"Indicates the minimum number of initial conflicts before the first restart can occur. This\nallows the solver to learn some things about the problem before a restart is allowed to\noccur.\n\nPossible values: u64",
"Indicates the minimum number of initial conflicts before the first restart can occur. [default: 10000] [possible values: int]",
"int:0:18446744073709551615",
"10000"
],
[
"--restart-lbd-coef",
"Used to determine if a restart should be forced (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe state is \"bad\" if the current LBD value is much greater than\nthe global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent\nrestart policy. If the long-term average LBD multiplied by this coefficient is lower\nthan the short-term average LBD then a restart is performed.\n\nPossible values: f64",
"The coefficient used to determine whether a restart should be forced. [default: 1.25] [possible values: float]",
"float",
"1.25"
],
[
"--restart-num-assigned-coef",
"Used to determine if a restart should be blocked (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nTo be used in combination with \"--restarts-num-assigned-window\".\n\nA restart is blocked if the number of assigned propositional variables is much greater than\nthe average number of assigned variables in the recent past. A greater (lower) value for\n\"--restart-num-assigned-coef\" means fewer (more) blocked restarts.\n\nPossible values: f64",
"The coefficient used to determine whether a restart should be blocked. [default: 1.4] [possible values: float]",
"float",
"1.4"
],
[
"--restart-num-assigned-window",
"Used to determine the length of the recent past that should be considered when deciding on\nblocking restarts (see \"Refining Restarts Strategies for SAT\nand UNSAT - Audemard and Simon (2012)\").\n\nThe solver considers the last \"--restart_num_assigned_window\" conflicts as the reference\npoint for the number of assigned variables.\n\nPossible values: u64",
"The length of the recent past that is considered when deciding whether to block a restart. [default: 5000] [possible values: int]",
"int:0:18446744073709551615",
"5000"
],
[
"--restart-geometric-coef",
"The coefficient in the geometric sequence `x_i = x_{i-1} * \"--restart-geometric-coef\"`\nwhere `x_1 = \"--restarts-base-interval\"`. Used only if \"--restarts-sequence-generator\"\nis assigned to \"geometric\".\n\nPossible values: f64 (Optional)",
"float",
""
],
[
"--omit-timestamp",
"If `--verbose` is enabled then this option removes the timestamp information from the log\nmessages. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool",
"bool",
"false"
],
[
"--omit-call-site",
"If `--verbose` is enabled then this option removes the call site information from the log\nmessages. The call site is the file and line from which the message\noriginated. Note that this option will only take affect in the case of a (W)CNF instance.\n\nPossible values: bool",
"bool",
"false"
],
[
"--upper-bound-encoding",
"The encoding to use for the upper bound constraint in a MaxSAT optimisation problem.\n\n- The \"generalised-totalizer\" value specifies that the solver should use the Generalized Totalizer Encoding (see \"Generalized totalizer encoding for pseudo-boolean constraints - Saurabh et al. (2015)\") - The \"cardinality-network\" value specifies that the solver should use the Cardinality Network Encoding (see \"Cardinality networks: a theoretical and empirical study - Asín et al. (2011)\").",
"opt:generalized-totalizer:cardinality-network",
"generalized-totalizer"
],
[
"--no-restarts",
"Determines that no restarts are allowed by the solver.\n\nPossible values: bool",
"bool",
"false"
],
[
"--conflict-resolver",
"Determines the conflict resolver",
"opt:no-learning:one-uip:all-decision:extended-cpip:bounds-extended-cpip",
"one-uip"
],
[
"--cumulative-allow-holes",
"Determines that the cumulative propagator(s) are allowed to create holes in the domain.\n\nPossible values: bool",
"bool",
"false"
"--cumulative-propagation-method",
"Determines the type of propagator which is used for the cumulative constraint. [default: time-table-over-interval-incremental] [possible values: time-table-per-point, time-table-per-point-incremental, time-table-per-point-incremental-synchronised, time-table-over-interval, time-table-over-interval-incremental, time-table-over-interval-incremental-synchronised]",
"opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised",
"time-table-over-interval-incremental"
],
[
"--cumulative-explanation-type",
"Determines the type of explanation used by the cumulative propagator(s) to explain propagations/conflicts",
"Determines the type of explanation used by the cumulative propagator(s). [default: pointwise] [possible values: naive, big-step, pointwise]",
"opt:naive:big-step:pointwise",
"pointwise"
],
[
"--cumulative-propagation-method",
"Determines the type of propagator which is used by the cumulative propagator(s) to propagate the constraint.\n\nCurrently, the solver only supports variations on time-tabling methods.",
"opt:time-table-per-point:time-table-per-point-incremental:time-table-per-point-incremental-synchronised:time-table-over-interval:time-table-over-interval-incremental:time-table-over-interval-incremental-synchronised",
"time-table-over-interval-incremental"
"--cumulative-allow-holes",
"Determines that the cumulative propagator(s) are allowed to create holes in the domain.",
"bool",
"false"
],
[
"--cumulative-single-profiles",
"Determines whether a single profiles are used generated when explaining a propagation for the cumulative constraint.\n\nPossible values: bool",
"Uses single profiles when explaining propagations of the cumulative constraint.",
"bool",
"false"
],
[
"--cumulative-incremental-backtracking",
"Determines whether incremental backtracking is applied or whether the cumulative propagators compute the time-table from scratch upon backtracking\n\nPossible values: bool",
"Enables incremental backtracking for the cumulative propagator(s).",
"bool",
"false"
],
[
"--optimisation-strategy",
"Determine what type of optimisation strategy is used by the solver",
"opt:linear-sat-unsat:linear-unsat-sat",
"linear-sat-unsat"
],
[
"--memory-preallocated",
"The amount of memory (in MB) that is preallocated for storing nogoods",
"int:0:18446744073709551615",
"50"
],
[
"--nogood-priority",
"The priority of the nogood propagator",
"opt:high:medium:low:very-low:ultra-low:lowest",
"very-low"
]
],
"tags": [
Expand Down
Loading
Loading