forked from chuffed/chuffed
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathchuffed.msc.in
55 lines (55 loc) · 4.15 KB
/
chuffed.msc.in
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
{
"id": "org.chuffed.chuffed",
"name": "Chuffed",
"description": "Chuffed FlatZinc executable",
"version": "${chuffed_VERSION_MAJOR}.${chuffed_VERSION_MINOR}.${chuffed_VERSION_PATCH}",
"mznlib": "../chuffed",
"executable": "${REL_INSTALL_BINARY}",
"tags": ["cp","lcg","int"],
"stdFlags": ["-a","-f","-n","-r","-s","-t","-v","--cp-profiler"],
"extraFlags": [
["--prop-fifo", "Use FIFO queues for propagation", "bool", "false"],
["--vsids", "Use activity-based search on the Boolean variables", "bool", "false"],
["--toggle-vsids", "Alternate search between user-specified and activity-based one", "bool", "false"],
["--restart", "Restart sequence type", "opt:chuffed:none:constant:linear:luby:geometric", "chuffed"],
["--restart-base", "Base for geometric restart sequence", "float", "1.5"],
["--restart-scale", "Scale factor for restart sequence", "int", "1000000000"],
["--switch-to-vsids-after", "Search starts with the user-specified one and switches to the activity-based one after a specified number of conflicts", "int", "1000000000"],
["--branch-random", "Use random variable selection for tie breaking instead of input order", "bool", "false"],
["--sat-polarity", "Selection of the polarity of Boolean variables (0 = default, 1 = same, 2 = anti, 3 = random)", "int", "0"],
["--lazy", "Allow clause generation for domain update", "bool:on:off", "true"],
["--finesse", "Try to generated stronger clauses", "bool:on:off", "true"],
["--learn", "Compute nogoods when a conflict is encountered", "bool:on:off", "true"],
["--eager-limit", "The maximal domain size of eager integer variables", "int", "1000"],
["--sat-var-limit", "The maximal number of Boolean variables", "int", "2000000"],
["--n-of-learnts", "The maximal number of learnt clauses", "int", "100000"],
["--learnts-mlimit", "The maximal memory limit for learnt clauses in Bytes", "int", "500000000"],
["--sort-learnt-level", "Sort literals in a learnt clause based on their decision level", "bool", "false"],
["--one-watch", "Watch only one literal in a learn clause", "bool:on:off", "true"],
["--bin-clause-opt", "Optimise learnt clauses of length 2", "bool:on:off", "true"],
["--assump-int", "Try and convert assumptions from the assumption interface back to integer domain expressions", "bool:on:off", "false"],
["--introduced-heuristic", "Decide if variable is introduced based on its name", "bool", "false"],
["--use-var-is-introduced", "Decide if variable is introduced based on var_is_introduced annotation", "bool", "false"],
["--exclude-introduced", "Exclude introduced variables from learnt clauses", "bool", "false"],
["--decide-introduced", "Allow search decisions on introduced variables and their derived internal variables", "bool:on:off", "true"],
["--fd-simplify", "Remove FD propagators that are satisfied globally", "bool:on:off", "true"],
["--sat-simplify", "Remove of clauses that are satisfied globally", "bool:on:off", "true"],
["--cumu-global", "Use the global cumulative propagator if possible", "bool:on:off", "true"],
["--disj-edge-find", "Use the edge-finding propagator for disjunctive constraints", "bool:on:off", "true"],
["--disj-set-bp", "Use the set bounds propagator for disjunctive constraints", "bool:on:off", "true"],
["--mdd", "Use the MDD propagator if possible", "bool", "false"],
["--mip", "Use the MIP propagator if possible", "bool", "false"],
["--mip-branch", "Use MIP branching as the branching strategy", "bool", "false"],
["--sym-static", "Use static symmetry breaking constraints", "bool", "false"],
["--ldsb", "Use lightweight dynamic symmetry breaking constraints '1UIP crippled'", "bool", "false"],
["--ldsbta", "Use lightweight dynamic symmetry breaking constraints '1UIP'", "bool", "false"],
["--ldsbad", "Use lightweight dynamic symmetry breaking constraints 'all decision clause'", "bool", "false"],
["--sbps", "Use Solution-based phase saving (SBPS) value selection heuristic", "bool", "false"],
],
"supportsMzn": false,
"supportsFzn": true,
"needsSolns2Out": true,
"needsMznExecutable": false,
"needsStdlibDir": false,
"isGUIApplication": false
}