diff --git a/minizinc/pumpkin-for-proofs.msc b/minizinc/pumpkin-for-proofs.msc index eec3a7eca..9128b513c 100644 --- a/minizinc/pumpkin-for-proofs.msc +++ b/minizinc/pumpkin-for-proofs.msc @@ -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": [ diff --git a/minizinc/pumpkin.msc b/minizinc/pumpkin.msc index ec1de9bed..b9d40a3c1 100644 --- a/minizinc/pumpkin.msc +++ b/minizinc/pumpkin.msc @@ -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": [ diff --git a/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs b/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs index 1a60a4cd5..11127dc7f 100644 --- a/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs +++ b/pumpkin-crates/core/src/basic_types/sequence_generators/sequence_generator_type.rs @@ -16,9 +16,9 @@ pub enum SequenceGeneratorType { /// When `multiplicative_factor` is not an integer, then the above formula is **not** the same /// as the formula `f(i) = a * m^i` since intermediate values are founded down. Geometric, - /// Indicates that the restart strategy should use Luby restarts \[1\]. + /// Indicates that the restart strategy should use Luby restarts. /// - /// The Luby sequence is a recursive sequence of the form: + /// The Luby sequence \[1\] is a recursive sequence of the form: /// 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2.... /// /// # Bibliography diff --git a/pumpkin-crates/core/src/optimisation/mod.rs b/pumpkin-crates/core/src/optimisation/mod.rs index 5b581e336..9fdb540f3 100644 --- a/pumpkin-crates/core/src/optimisation/mod.rs +++ b/pumpkin-crates/core/src/optimisation/mod.rs @@ -28,11 +28,15 @@ pub trait OptimisationProcedure). @@ -80,6 +83,65 @@ struct Args { #[arg(long, hide = true, exclusive = true)] generate_msc: Option, + /// The time budget for the solver, given in milliseconds. + #[arg( + short = 't', + long = "time-limit", + verbatim_doc_comment, + value_name = "MS" + )] + time_limit: Option, + + /// The random seed to use for the Pseudo Random Number Generator. + /// + /// Randomisation can be used for aspects such as the variable/value generator or initial + /// ordering of variables. + #[arg( + short = 'r', + long = "random-seed", + default_value_t = 42, + verbatim_doc_comment, + value_name = "u64" + )] + random_seed: u64, + + /// Reports all solutions (satisfaction) or all intermediate solutions (optimisation). + /// + /// For satisfaction problems, every solution is reported. For optimisation problems, solutions + /// of increasing quality are reported as they are found. + /// + /// See the MiniZinc specification () + /// for more information. + #[arg( + help_heading = "Output", + short = 'a', + long = "all-solutions", + verbatim_doc_comment + )] + all_solutions: bool, + + /// Enables log message output from the solver. + /// + /// For printing statistics see the option "--log-statistics", and for printing all solutions + /// (in case of a satisfaction problem) or printing solutions of increasing quality (in case of + /// an optimization problem) see the option "--all-solutions". + #[arg( + help_heading = "Output", + short = 'v', + long = "verbose", + verbatim_doc_comment + )] + verbose: bool, + + /// Enables logging of statistics from the solver. + #[arg( + help_heading = "Output", + short = 's', + long = "log-statistics", + verbatim_doc_comment + )] + log_statistics: bool, + /// The output path for the proof file. /// /// When solving a DIMACS instance, a DRAT proof is logged. In case of a FlatZinc model, a DRCP @@ -87,25 +149,95 @@ struct Args { /// /// In case of a DRCP proof, if the file extension ends with `.gz`, a gzipped proof will be /// produced. - #[arg(long, verbatim_doc_comment)] + #[arg( + help_heading = "Proof Logging", + long, + verbatim_doc_comment, + value_name = "PATH" + )] proof_path: Option, /// What type of proof to log. /// - /// If the `proof_path` option is not provided, this is ignored. - #[arg(long, value_enum, default_value_t)] + /// Requires "--proof-path" to be provided. + #[arg( + help_heading = "Proof Logging", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "TYPE", + requires = "proof_path" + )] proof_type: ProofType, + /// Determines what type of optimisation strategy is used by the solver. + #[arg( + help_heading = "Search", + long = "optimisation-strategy", + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "STRATEGY" + )] + optimisation_strategy: OptimisationStrategy, + + /// Allows the solver to ignore the search annotations specified in a MiniZinc model. + /// + /// See the MiniZinc specification () + /// for more information. + #[arg( + help_heading = "Search", + short = 'f', + long = "free-search", + verbatim_doc_comment + )] + free_search: bool, + + /// Determines the conflict resolver. + #[arg( + help_heading = "Conflict Analysis", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "RESOLVER" + )] + conflict_resolver: ConflictResolverType, + + /// Enables recursive minimisation of learned nogoods. + /// + /// The minimisation is applied as a post-processing step after conflict analysis; according to + /// the idea proposed in "Generalized Conflict-Clause Strengthening for Satisfiability Solvers + /// - Allen van Gelder (2011)". + #[arg( + help_heading = "Conflict Analysis", + long = "recursive-minimisation", + verbatim_doc_comment + )] + recursive_minimisation: bool, + + /// Disables semantic minimisation of learned nogoods during conflict analysis. + /// + /// By default, semantic minimisation is applied during conflict analysis; according to the + /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". + #[arg( + help_heading = "Conflict Analysis", + long = "no-iterative-minimisation", + verbatim_doc_comment + )] + no_iterative_minimisation: bool, + /// The number of high-lbd learned nogoods that are kept in the database. /// /// Learned nogoods are kept based on the tiered system introduced in "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)". - /// - /// Possible values: usize #[arg( + help_heading = "Nogood Database", long = "learning-max-num-high-lbd-nogoods", default_value_t = 20_000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_high_lbd_nogoods: usize, @@ -113,12 +245,12 @@ struct Args { /// /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: usize #[arg( + help_heading = "Nogood Database", long = "learning-max-num-mid-lbd-nogoods", default_value_t = 7000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_mid_lbd_nogoods: usize, @@ -126,32 +258,32 @@ struct Args { /// /// This is based on the variation of the three-tiered system proposed in /// "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: usize #[arg( + help_heading = "Nogood Database", long = "learning-max-num-low-lbd-nogoods", default_value_t = 100_000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "usize" )] learning_max_num_low_lbd_nogoods: usize, - /// The treshold determining whether a learned nogood is "low" LBD. + /// The threshold determining whether a learned nogood is "low" LBD. /// /// "Low" LBD nogood are kept around for longer since they are of better "quality". /// /// Learned nogoods are kept based on the tiered system introduced "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: u32 #[arg( + help_heading = "Nogood Database", long = "learning-low-lbd-threshold", default_value_t = 3, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u32" )] learning_low_lbd_threshold: u32, - /// The treshold determining whether a learned nogood is "low" LBD. + /// The threshold determining whether a learned nogood is "high" LBD. /// /// "High" LBD nogood are kept around for a shorter amount of time since they are of bad /// "quality". @@ -159,31 +291,52 @@ struct Args { /// Learned nogoods are kept based on the tiered system introduced "Improving /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)" /// with the variation from "Improving Implementation of SAT Competitions 2017–2019 Winners". - /// - /// Possible values: u32 #[arg( + help_heading = "Nogood Database", long = "learning-high-lbd-threshold", default_value_t = 7, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u32" )] learning_high_lbd_threshold: u32, - /// Decides whether learned clauses are minimised as a post-processing step after computing the - /// 1-UIP Minimisation is done; according to the idea proposed in "Generalized Conflict-Clause - /// Strengthening for Satisfiability Solvers - Allen van Gelder (2011)". - /// - /// Possible values: bool - #[arg(long = "recursive-minimisation", verbatim_doc_comment)] - recursive_minimisation: bool, + /// The amount of memory (in MB) that is preallocated for storing nogoods. + #[arg( + help_heading = "Nogood Database", + long = "memory-preallocated", + default_value_t = 50, + verbatim_doc_comment, + value_name = "MB" + )] + memory_preallocated: usize, - /// Decides whether to apply semantic minimisation during conflict analysis; according to the - /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". - /// - /// If this flag is present then the minimisation is turned on. - /// - /// Possible values: bool - #[arg(long = "no-iterative-minimisation", verbatim_doc_comment)] - no_iterative_minimisation: bool, + /// The priority of the nogood propagator. + #[arg( + help_heading = "Nogood Database", + long = "nogood-priority", + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "PRIORITY" + )] + nogood_propagator_priority: Priority, + + /// Determines that no restarts are allowed by the solver. + #[arg( + help_heading = "Restarts", + long = "no-restarts", + verbatim_doc_comment, + conflicts_with_all = [ + "restart_sequence_generator_type", + "restart_base_interval", + "restart_geometric_coef", + "restart_min_num_conflicts_before_first_restart", + "restart_lbd_coef", + "restart_num_assigned_coef", + "restart_num_assigned_window", + ] + )] + no_restarts: bool, /// Decides the sequence based on which the restarts are performed. /// @@ -194,11 +347,19 @@ struct Args { /// 1, 1, 2, 4, 8, 1, 1, 2.... (see "Optimal speedup of Las Vegas algorithms - Luby et al. /// (1993)") /// - /// To be used in combination with "--restarts-base-interval". - #[arg(long, value_enum, default_value_t)] + /// To be used in combination with "--restart-base-interval". + #[arg( + help_heading = "Restarts", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "SEQUENCE_GENERATOR" + )] restart_sequence_generator_type: SequenceGeneratorType, - /// The base interval length is used as a multiplier to the restart sequence. + /// The base interval length which is used as a multiplier to the restart sequence. + /// /// - In the case of the "constant" restart sequence this argument indicates the constant which /// is used to determine when a restart occurs /// - For the "geometric" approach this argument indicates the starting value of the sequence @@ -206,219 +367,183 @@ struct Args { /// /// For example, constant restarts with base interval 50 means a restart is triggered every 50 /// conflicts. - /// - /// Possible values: u64 #[arg( + help_heading = "Restarts", long = "restart-base-interval", default_value_t = 50, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_base_interval: u64, - /// Indicates the minimum number of initial conflicts before the first restart can occur. This - /// allows the solver to learn some things about the problem before a restart is allowed to - /// occur. + /// The coefficient of the geometric restart sequence. /// - /// Possible values: u64 + /// The sequence is defined as `x_i = x_{i-1} * "--restart-geometric-coef"` where + /// `x_1 = "--restart-base-interval"`. Required if "--restart-sequence-generator-type" is + /// assigned to "geometric". #[arg( + help_heading = "Restarts", + long = "restart-geometric-coef", + verbatim_doc_comment, + value_name = "f64", + required_if_eq("restart_sequence_generator_type", "geometric") + )] + restart_geometric_coef: Option, + + /// Indicates the minimum number of initial conflicts before the first restart can occur. + /// + /// This allows the solver to learn some things about the problem before a restart is allowed + /// to occur. + #[arg( + help_heading = "Restarts", long = "restart-min-initial-conflicts", default_value_t = 10000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_min_num_conflicts_before_first_restart: u64, - /// Used to determine if a restart should be forced (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The coefficient used to determine whether a restart should be forced. + /// + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// /// The state is "bad" if the current LBD value is much greater than /// the global LBD average. A greater (lower) value for lbd-coef means a less (more) frequent /// restart policy. If the long-term average LBD multiplied by this coefficient is lower /// than the short-term average LBD then a restart is performed. - /// - /// Possible values: f64 #[arg( + help_heading = "Restarts", long = "restart-lbd-coef", default_value_t = 1.25, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "f64" )] restart_lbd_coef: f64, - /// Used to determine if a restart should be blocked (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The coefficient used to determine whether a restart should be blocked. + /// + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// - /// To be used in combination with "--restarts-num-assigned-window". + /// To be used in combination with "--restart-num-assigned-window". /// /// A restart is blocked if the number of assigned propositional variables is much greater than /// the average number of assigned variables in the recent past. A greater (lower) value for /// "--restart-num-assigned-coef" means fewer (more) blocked restarts. - /// - /// Possible values: f64 #[arg( + help_heading = "Restarts", long = "restart-num-assigned-coef", default_value_t = 1.4, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "f64" )] restart_num_assigned_coef: f64, - /// Used to determine the length of the recent past that should be considered when deciding on - /// blocking restarts (see "Refining Restarts Strategies for SAT - /// and UNSAT - Audemard and Simon (2012)"). + /// The length of the recent past that is considered when deciding whether to block a restart. /// - /// The solver considers the last "--restart_num_assigned_window" conflicts as the reference - /// point for the number of assigned variables. + /// See "Refining Restarts Strategies for SAT and UNSAT - Audemard and Simon (2012)". /// - /// Possible values: u64 + /// The solver considers the last "--restart-num-assigned-window" conflicts as the reference + /// point for the number of assigned variables. #[arg( + help_heading = "Restarts", long = "restart-num-assigned-window", default_value_t = 5000, - verbatim_doc_comment + verbatim_doc_comment, + value_name = "u64" )] restart_num_assigned_window: u64, - /// The coefficient in the geometric sequence `x_i = x_{i-1} * "--restart-geometric-coef"` - /// where `x_1 = "--restarts-base-interval"`. Used only if "--restarts-sequence-generator" - /// is assigned to "geometric". + /// Determines the type of propagator which is used for the cumulative constraint. /// - /// Possible values: f64 (Optional) - #[arg(long = "restart-geometric-coef", verbatim_doc_comment)] - restart_geometric_coef: Option, + /// Currently, the solver only supports variations on time-tabling methods. + #[arg( + help_heading = "Cumulative", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "PROPAGATION" + )] + cumulative_propagation_method: CumulativePropagationMethod, - /// The time budget for the solver, given in milliseconds. - /// - /// Possible values: u64 (Optional) - #[arg(short = 't', long = "time-limit", verbatim_doc_comment)] - time_limit: Option, + /// Determines the type of explanation used by the cumulative propagator(s). + #[arg( + help_heading = "Cumulative", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "EXPLANATION" + )] + cumulative_explanation_type: CumulativeExplanationType, - /// The random seed to use for the Pseudo Random Number Generator. - /// - /// Randomisation can be used for aspects such as the variable/value generator or initial - /// ordering of variables. - /// - /// Possible values: u64 + /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. #[arg( - short = 'r', - long = "random-seed", - default_value_t = 42, + help_heading = "Cumulative", + long = "cumulative-allow-holes", verbatim_doc_comment )] - random_seed: u64, - - /// Enables log message output from the solver. - /// - /// For printing statistics see the option "--log-statistics", and for printing all solutions - /// (in case of a satisfaction problem) or printing solutions of increasing quality (in case of - /// an optimization problem) see the option "--all-solutions". - /// - /// Possible values: bool - #[arg(short = 'v', long = "verbose", verbatim_doc_comment)] - verbose: bool, - - /// Enables logging of statistics from the solver. - /// - /// Possible values: bool - #[arg(short = 's', long = "log-statistics", verbatim_doc_comment)] - log_statistics: bool, - - /// Instructs the solver to perform free search when solving a MiniZinc model; this flag - /// indicates that it is allowed to ignore the search annotations specified in the model. - /// - /// See the MiniZinc specification () - /// for more information. - /// - /// Possible values: bool - #[arg(short = 'f', long = "free-search", verbatim_doc_comment)] - free_search: bool, - - /// Instructs the solver to report all solutions in the case of satisfaction problems, - /// or print intermediate solutions of increasing quality in the case of optimisation - /// problems. - /// - /// See the MiniZinc specification () - /// for more information. - /// - /// Possible values: bool - #[arg(short = 'a', long = "all-solutions", verbatim_doc_comment)] - all_solutions: bool, + cumulative_allow_holes: bool, - /// If `--verbose` is enabled then this option removes the timestamp information from the log - /// messages. Note that this option will only take affect in the case of a (W)CNF instance. - /// - /// Possible values: bool - #[arg(long = "omit-timestamp", verbatim_doc_comment)] - omit_timestamp: bool, + /// Uses single profiles when explaining propagations of the cumulative constraint. + #[arg( + help_heading = "Cumulative", + long = "cumulative-single-profiles", + verbatim_doc_comment + )] + cumulative_single_profiles: bool, - /// If `--verbose` is enabled then this option removes the call site information from the log - /// messages. The call site is the file and line from which the message - /// originated. Note that this option will only take affect in the case of a (W)CNF instance. + /// Enables incremental backtracking for the cumulative propagator(s). /// - /// Possible values: bool - #[arg(long = "omit-call-site", default_value_t = false, verbatim_doc_comment)] - omit_call_site: bool, + /// Otherwise, the cumulative propagator(s) compute the time-table from scratch upon + /// backtracking. + #[arg( + help_heading = "Cumulative", + long = "cumulative-incremental-backtracking", + verbatim_doc_comment + )] + cumulative_incremental_backtracking: bool, /// The encoding to use for the upper bound constraint in a MaxSAT optimisation problem. /// - /// - The "generalised-totalizer" value specifies that the solver should use the Generalized + /// - The "generalized-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)"). - #[arg(long, value_enum, default_value_t)] + #[arg( + help_heading = "Max(SAT)", + long, + value_enum, + default_value_t, + verbatim_doc_comment, + value_name = "ENCODING" + )] upper_bound_encoding: PseudoBooleanEncoding, - /// Determines that no restarts are allowed by the solver. - /// - /// Possible values: bool - #[arg(long = "no-restarts", verbatim_doc_comment)] - no_restarts: bool, - - /// Determines the conflict resolver. - #[arg(long, value_enum, default_value_t)] - conflict_resolver: ConflictResolverType, - - /// Determines that the cumulative propagator(s) are allowed to create holes in the domain. + /// Removes the timestamp information from the log messages. /// - /// Possible values: bool - #[arg(long = "cumulative-allow-holes", verbatim_doc_comment)] - cumulative_allow_holes: bool, - - /// Determines the type of explanation used by the cumulative propagator(s) to explain - /// propagations/conflicts. - #[arg(long, value_enum, default_value_t)] - cumulative_explanation_type: CumulativeExplanationType, - - /// Determines the type of propagator which is used by the cumulative propagator(s) to - /// propagate the constraint. - /// - /// Currently, the solver only supports variations on time-tabling methods. - #[arg(long, value_enum, default_value_t)] - cumulative_propagation_method: CumulativePropagationMethod, + /// Only applicable if `--verbose` is enabled, and only for (W)CNF instances. + #[arg( + help_heading = "Max(SAT)", + long = "omit-timestamp", + verbatim_doc_comment + )] + omit_timestamp: bool, - /// Determines whether a single profiles are used generated when explaining a propagation for - /// the cumulative constraint. + /// Removes the call site information from the log messages. /// - /// Possible values: bool - #[arg(long = "cumulative-single-profiles")] - cumulative_single_profiles: bool, - - /// Determines whether incremental backtracking is applied or whether the cumulative - /// propagators compute the time-table from scratch upon backtracking + /// Only applicable if `--verbose` is enabled, and only for (W)CNF instances. /// - /// Possible values: bool - #[arg(long = "cumulative-incremental-backtracking")] - cumulative_incremental_backtracking: bool, - - /// Determine what type of optimisation strategy is used by the solver - #[arg(long = "optimisation-strategy", value_enum, default_value_t)] - optimisation_strategy: OptimisationStrategy, - - /// The amount of memory (in MB) that is preallocated for storing nogoods. - #[arg(long = "memory-preallocated", default_value_t = 50)] - memory_preallocated: usize, - - /// The priority of the nogood propagator. - #[arg(long = "nogood-priority", value_enum, default_value_t)] - nogood_propagator_priority: Priority, + /// The call site is the file and line from which the message originated. + #[arg( + help_heading = "Max(SAT)", + long = "omit-call-site", + default_value_t = false, + verbatim_doc_comment + )] + omit_call_site: bool, } fn configure_logging( diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs index 547aa0a2b..d6b1cf3dc 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs @@ -69,17 +69,20 @@ pub(crate) trait PseudoBooleanConstraintEncoderInterface { /// [`PseudoBooleanConstraintEncoder`]. #[derive(Default, Clone, Copy, Debug, ValueEnum)] pub(crate) enum PseudoBooleanEncoding { - /// Specifies the usage of the generalized totalizer encoding for pseudo-boolean constraints - /// \[1\]. + /// Specifies the usage of the generalized totalizer encoding for pseudo-boolean constraints. + /// + /// See \[1\] for more information. /// /// # Bibliography /// \[1] "Generalized totalizer encoding for pseudo-boolean constraints.", Joshi Saurabh, Ruben /// Martins, Vasco Manquinho; CP '15 #[default] GeneralizedTotalizer, - /// Specifies the usage of the cardinality network \[1\] encoding for unweighted cardinality - /// constraints in the form `x1 + ... + xn <= k`. The encoding is arc-consistent and - /// supports incremental strengthening of the upper bound. + /// Specifies the usage of the cardinality network encoding for unweighted cardinality + /// constraints in the form `x1 + ... + xn <= k`. + /// + /// The encoding \[1\] is arc-consistent and supports incremental strengthening of the upper + /// bound. /// /// # Bibliography /// \[1\] R. Asín, R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-Carbonell, ‘Cardinality diff --git a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs index 6f3b704ef..bb2cc4070 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/msc.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/msc.rs @@ -39,12 +39,20 @@ const CONFIGURATIONS: [(&str, &str, &str, &str); 2] = [ /// ). const MINIZINC_STD_FLAGS: [char; 9] = ['a', 'f', 'i', 'n', 'p', 'r', 's', 't', 'v']; +/// The help headings of arguments which are not applicable to MiniZinc models, and are therefore +/// not exposed. +const EXCLUDED_HEADINGS: [&str; 1] = ["Max(SAT)"]; + fn generate_msc(name: &str, id: &str, mznlib: &str) -> String { let command = Args::command(); let arguments = command .get_arguments() .filter(|arg| !arg.is_positional() && !arg.is_hide_set()) - .filter(|arg| !matches!(arg.get_action(), ArgAction::Help | ArgAction::Version)); + .filter(|arg| !matches!(arg.get_action(), ArgAction::Help | ArgAction::Version)) + .filter(|arg| { + arg.get_help_heading() + .is_none_or(|heading| !EXCLUDED_HEADINGS.contains(&heading)) + }); // Arguments whose short flag is a standard flag of MiniZinc (e.g. `-a`) are exposed as such; // all other arguments are exposed as extra flags. @@ -82,10 +90,10 @@ fn extra_flag(arg: &Arg) -> Value { (None, Some(short)) => format!("-{short}"), (None, None) => unreachable!("non-positional arguments have a long or short flag"), }; - let description = arg + let summary = arg .get_long_help() .or(arg.get_help()) - .map(|help| help.to_string()) + .map(|help| summary(&help.to_string())) .unwrap_or_default(); let default = arg @@ -95,8 +103,8 @@ fn extra_flag(arg: &Arg) -> Value { .collect::>() .join(","); - let (flag_type, default) = if matches!(arg.get_action(), ArgAction::SetTrue) { - ("bool".to_owned(), "false".to_owned()) + let (flag_type, default, description) = if matches!(arg.get_action(), ArgAction::SetTrue) { + ("bool".to_owned(), "false".to_owned(), summary) } else if !arg.get_possible_values().is_empty() { let values = arg .get_possible_values() @@ -104,14 +112,41 @@ fn extra_flag(arg: &Arg) -> Value { .filter(|value| !value.is_hide_set()) .map(|value| value.get_name().to_owned()) .collect::>(); - (format!("opt:{}", values.join(":")), default) + let description = format!( + "{summary} [default: {default}] [possible values: {}]", + values.join(", ") + ); + (format!("opt:{}", values.join(":")), default, description) } else { - (value_type(arg), default) + let flag_type = value_type(arg); + // Strip the bounds from the type, e.g. `int:0:4294967295` is shown as `int`. + let type_name = flag_type + .split(':') + .next() + .expect("split yields at least one item"); + let description = if default.is_empty() { + format!("{summary} [possible values: {type_name}]") + } else { + format!("{summary} [default: {default}] [possible values: {type_name}]") + }; + (flag_type, default, description) }; json!([flag, description, flag_type, default]) } +/// Condenses the help of an argument into a single line, such that it is displayed nicely by +/// `minizinc --help`, which does not indent the continuation lines of a description. +/// +/// The summary is the first paragraph of the help, up to the start of any list. +fn summary(help: &str) -> String { + help.lines() + .map(str::trim) + .take_while(|line| !line.is_empty() && !line.starts_with("- ")) + .collect::>() + .join(" ") +} + /// Returns the MiniZinc type corresponding to the type of value which is parsed for `arg`. fn value_type(arg: &Arg) -> String { let type_id = arg.get_value_parser().type_id();