An instance generator and multi-objective optimizer backend for Clafer using the Choco 6.0.2 constraint programming library. There are two ways to use the project: programmatically via the Java API or via the command-line interface (CLI).
The CLI is used by ClaferIDE, ClaferMooVisualizer, and ClaferConfigurator.
Note: the name "choco-solver" refers to the Java library for Constraint Programming, whereas "chocosolver" (without the "-") is the name of this project. We might change the name in the future to avoid confusion.
- Jimmy Liang, Ph.D. Candidate. Main developer.
- Michal Antkiewicz, Research Engineer. Release Management, development, testing.
- Alexandr Murashkin. CLI, stress testing.
- Jordan Ross. Stress testing.
Binary distributions of the release 0.5.4 of Clafer Tools can be downloaded from Clafer Tools - Binary Distributions.
- download the binaries and unpack
<target directory>of your choice - add the
<target directory>to your system path so that the executables can be found
- VS Code: clafer-vscode.
- Sublime Text 4: ClaferToolsST.
- Choco 6.0.2, v6.0.2.
- Java 21+, 64bit.
- Maven 3.2+. Required for building the project.
- Clafer compiler, v0.5.4.
- This backend provides an API for solving Clafer models. The Clafer compiler can compile a Clafer model down to the proper API calls.
- The API calls can also be written manually quite easily with a bit of extra typing (examples down below).
Follow the installation instructions in the README.md.
Install the API and the CLI.
git clone https://github.com/gsdlab/chocosolver.git
cd chocosolver
mvn install -DskipTestsInclude the following XML snippet in your POM to use the API in your Maven project.
<dependency>
<groupId>org.clafer</groupId>
<artifactId>chocosolver</artifactId>
<version>0.5.5</version>
</dependency>The CLI is installed to target/chocosolver-0.5.5-jar-with-dependencies.jar;
however, in the Clafer Tools binary distribution it is called chocosolver.jar.
You can deploy the files the same way as in Clafer Tools binary distribution by executing
make install to=<target path>All related projects are following the simultaneous release model.
The branch master contains releases, whereas the branch develop contains code under development.
When building the tools, the branches should match.
Releases from branches master are guaranteed to work well together.
Development versions from branches develop should work well together but this might not always be the case.
For usage instructions, start the CLI using the command
java -jar chocosolver.jar --help`
Option Description
------ -----------
--decimal-digits <Integer> Specify the number of fractional digits of decimals
(overrides the model's).
--file <File: Clafer model file (.cfr) Input file in .cfr or .js format.
or Clafer Javascript file (.js)>
--help Show help.
--import <Clafer file or URL> Compile the .cfr model together with the given Clafer
file or URL, relative to the current directory
(repeatable); a model also imports files with
--import in its //# OPTIONS directive.
--maxint <Integer> Specify maximum integer value.
--minint <Integer> Specify minimum integer value.
--moo Run in multi-objective optimization mode.
-n <Integer> Specify the maximum number of instances.
--output <File: text file> Output instances to the given file.
--prettify Use simple and pretty output format (not formal).
--repl Run in REPL (interactive) mode.
--scope <Integer> Override the default global scope value.
--scope-file <File: scope file> Read the scopes of clafers from the given .cfr-scope
file (by default, from the model's .cfr-scope file,
e.g., model.cfr-scope, if it exists).
--search <ClaferSearchStrategy> PreferSmallerInstances/PreferLargerInstances/Random.
-v Run in validation mode; checks all assertions.
--version Display the tool version.The CLI supports four modes of operation:
-v- validation mode,--repl- interactive mode,-moo- batch multi-objective optimization mode, and- (default) batch instance generation mode.
The last mode is selected when no -v and --repl are given and the model does not contain optimization objectives.
If the .cfr file is given, the CLI will first call the Clafer compiler using clafer -k -m choco model.cfr,
which will produce model.js.
A model can consist of several files (Clafer 0.5.4): the files that the model imports with --import in its //# OPTIONS directive are compiled with it, and --import=FILE on the command line adds a file (see Models in several files).
The compiler's errors give the file in which they are (Compile error at lib.cfr:3:11...).
The scopes come from the model: the compiler infers a scope for each clafer from the multiplicities.
A .cfr-scope file next to the model (model.cfr-scope for model.cfr or model.js), or the one given by --scope-file, sets the scopes of the clafers that it lists, e.g., smaller ones for a faster instance generation:
[
{"lpqName": "Component::Cfeatures", "scope": 132},
{"lpqName": "Flow::flowElements", "scope": 234}
]
A name is a clafer's UID (c0_Cfeatures) or a (partially) qualified name (Cfeatures, Component::Cfeatures or ::Component::Cfeatures), which sets the scopes of all the clafers whose names, with their parents', end with it.
This is the format that clafer --meta-data, claferIG's and the REPL's saveScopes write, and that claferIG reads.
The CLI prints Using the scopes from model.cfr-scope when it uses such a file; a name that is not of a clafer in the model is an error.
A scope that is too small excludes instances, so the instances with a smaller scope should be checked against those with the inferred one.
Certain features, such as transitive closure, are not yet supported by Clafer,
so they can only be used directly via API call in the .js file.
We recommend using the so called Choco escapes, as follows:
[choco|
<your code to be inserted verbatim at the end of the generated output>
|]
When running the interactive mode, the CLI automatically produces an instance and then is ready to accept commands. Here is an example session:
Type 'help' for the list of available REPL commands
=== Instance 1 Begin ===
Bob
owns -> car
car
transmission
manual
drivenBy -> Bob
--- Instance 1 End ---
ClaferChocoIG> h
'h'elp Print the REPL commands.
'n'ext Generate the next instance.
<enter> Generate the next instance.
'p'rettify Toggle prettify on/off.
'r'eload Reload the model from the same <file-name.js> file.
'u'nsatCore Compute the set of contradicting constraints if any.
min'U'nsat Compute the minimal UnSAT core and a near-miss example.
'S'etGlobalScope <value> Set the global scope to the <value> .
's'etScope <claferUID> <value> Set the scope of the given clafer to the <value>.
'I'ncGlobalScope <value?> Increase the global scope by <value> or 1 by default.
'i'ncScope <claferUID> <value?> Increase the scope of the given clafer by the <value> or 1 by default.
sa'v'eScopes Save the currect scopes to a .cfr-scope file.
'm'axInt <value> Set the largest allowed integer to <value>.
ma`x`imize <claferUID> Find a solution where <claferUID>.dref is maximal.
minimiz'e' <claferUID> Find a solution where <claferUID>.dref is minimal.
sta't's Display statistics about the current search.
'O'ptions Display the current solver options.
strate'g'y <smaller|larger|random> Set search strategy to prefer smaller, prefer larger, or random.
'o'ptimizations Toggle optimizations basic/full.
symmetry'B'reaking Toggle symmetry breaking basic/full.
'q'uit Exit the REPL sesssion.
ClaferChocoIG>
Each command can be invoked using a full name, e.g., IncGlobalScope, or using a shortcut, e.g., I, as indicated by 'I'.
The CLI is case sensitive, that is, i is for incScope command, whereas, I is for IncGlobalScope.
In general, the CLI classes are good examples of using the API:
- Main.java - this is the main class of the
chocosolver.jar. - Validate.java - checks assertions (run with
-v). - REPL.java - read, eval, print loop (interactive interface, run with
--repl). - Normal.java - runs batch instance generation or multi-objective optimization up to the given limit of instances (provided using
-n) or unlimited (by default). - Util.java - various shared utils.
Consider the following Clafer model.
Installation
xor Status
Ok
Bad
Time -> integer
[this > 2]
Below is an example of using the API to build the model above. AstModel represents the implicit "root" of the model. Every Clafer in the model is nested below it.
import org.clafer.ast.*;
import static org.clafer.ast.Asts.*;
public static void main(String[] args) {
AstModel model = newModel();
AstConcreteClafer installation = model.addChild("Installation").withCard(Mandatory);
// withCard(Mandatory) and withCard(1, 1) is the same. Pick the one you find more readable.
AstConcreteClafer status = installation.addChild("Status").withCard(1, 1).withGroupCard(1, 1);
AstConcreteClafer ok = status.addChild("Ok").withCard(Optional);
// withCard(Optional) and withCard(0, 1) is the same.
AstConcreteClafer bad = status.addChild("Bad").withCard(0, 1);
// Note that ok and bad have an explicit optional cardinality, whereas
// it was implicit in the oringal model.
AstConcreteClafer time = installation.addChild("Time").withCard(1, 1).refTo(IntType);
time.addConstraint(greaterThan(joinRef($this()), constant(2)));
// Note that joinRef is explicit whereas it was implicit in the original model.
}The Asts class provides all the functions required for building the model. See the previous link for a list of all the supported expressions. More examples of building models: structure, expressions, quantifiers, and attributed feature models.
The next step is to solve the model.
import org.clafer.compiler.*;
import org.clafer.scope.*;
public static void main(String[] args) {
...
ClaferSolver solver = ClaferCompiler.compile(model,
Scope.setScope(installation, 1).setScope(status, 1).setScope(ok, 1).setScope(bad, 1).setScope(time, 1)
// Set the scope of every Clafer to 1. The code above could be replaced with
// "Scope.defaultScope(1)".
.intLow(-16).intHigh(16));
// intLow is the "suggested" lowest integer for solving. intHigh is the "suggested"
// highest integer.
// find will return true when the solver finds another instance.
while (solver.find()) {
// Print the solution in a format similar to ClaferIG.
System.out.println(solver.instance());
}
}Optimizing on a single objective is supported. Suppose we wanted to optimize on the expression "sum time".
import org.clafer.objective.*;
...
ClaferOptimizer solver = ClaferCompiler.compile(model,
Scope.defaultScope(1).intLow(-16).intHigh(16),
Objective.maximize(sum(global(time))));
while (solver.find()) {
// The instances where time is maximal.
System.out.println(solver.instance());
}
solver = ClaferCompiler.compile(model,
Scope.defaultScope(1).intLow(-16).intHigh(16),
Objective.minimize(sum(global(time))));
while (solver.find()) {
// The instances where time is minimal.
System.out.println(solver.instance());
}The compiler can accept multiple objectives, in which case it will solve for all the Pareto-optimal solutions.
Consider the following Clafer model.
Mob
Duck ?
Witch ?
Floats ?
[Floats => Duck]
[Floats <=> Witch]
[!Duck]
[Witch]
The model is overconstrained and has no solutions. The solver can help here as well.
AstModel model = newModel();
AstConcreteClafer mob = model.addChild("Mob").withCard(0, 1);
AstConcreteClafer duck = model.addChild("Duck").withCard(0, 1);
AstConcreteClafer witch = model.addChild("Witch").withCard(0, 1);
AstConcreteClafer floats = model.addChild("Floats").withCard(0, 1);
model.addConstraint(some(mob));
model.addConstraint(implies(some(floats), some(duck)));
model.addConstraint(ifOnlyIf(some(floats), some(witch)));
model.addConstraint(none(duck));
model.addConstraint(some(witch));
ClaferUnsat unsat = ClaferCompiler.compileUnsat(model, Scope.defaultScope(1));
// Print the Min-Unsat and near-miss example.
System.out.println(unsat.minUnsat());The above code will print two things.
First it will print "#(Witch) >= 1" which is the constraint that is unsatisfiable in the model, i.e., the last constraint that enforces there to be some witch.
Next, it will print the near-miss example Mob#0.
It means that removing the some(Witch) constraint would make the model satisfiable and an example of a solution (after removing the constraint), is the instance with exactly one mob and nothing else.
For this example, the min-unsat is not unique, so it is possible that the library may report another set of constraints although the set of constraints is guaranteed to have a size of one.
The above example found that removing one constraint will fix the model but you may be wondering why the model cannot have a witch. In this case, it is more useful to compute the unsat-core instead.
ClaferUnsat unsat = ClaferCompiler.compileUnsat(model, Scope.defaultScope(1));
// Print the Unsat-Core.
System.out.println(unsat.unsatCore());The above code will print the last 4 constraints which are the constraints that are mutually unsatisfiable. What this means is that if you removed all constraints but these 4, the model is still unsatisfiable. The set of constraints is not guaranteed to be minimal but will likely be small.
If you prefer to use the Javascript API over the Java API:
import org.clafer.javascript.Javascript;
public static void main(String[] args) {
Javascript.readModel(
"scope({Installation:1, Status:1, Ok:1, Bad:1, Time:1});" +
"intRange(-16, 16);" +
"Installation = Clafer('Installation').withCard(1, 1);" +
...
}The configuration is done in the <host-tool-path>/Server/Backends/backends.json file, where <host-tool-path> is a path to the web-based tool (ClaferIDE, etc.) you want to configure to use chocosolver as a backend.
- An example configuration for ClaferIDE:
{
"backends": [
{
"id": "chocoIG",
"label": "Choco-based (IG + MOO)",
"tooltip": "An instance generator and multi-objective optimizer based on Choco3 solver library",
"accepted_format": "choco",
"tool": "java",
"tool_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--file=$filepath$", "--repl", "--prettify"],
"tool_version_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--version"],
"scope_options": {
"set_default_scope" : {"command": "SetGlobalScope $value$\n", "label": "Default:", "argument": "--scope=$value$", "default_value": 1},
"set_individual_scope": {"command": "setScope $clafer$ $value$\n"},
"inc_all_scopes" : {"command": "IncGlobalScope $value$\n", "label": "All:", "default_value": 1},
"inc_individual_scope": {"command": "incScope $clafer$ $value$\n"},
"produce_scope_file" : {"command": "saveScopes\n"},
"set_int_scope" : {"command": "maxInt $value$\n", "label": "Max. integer:", "argument": "--maxint=$value$", "default_value": 127}
},
"control_buttons": [
{"id": "next_instance", "command": "n\n", "label" : "Next", "tooltip": "Next Instance"},
{"id": "reload", "command": "r\n", "label" : "Reload", "tooltip": "Reload the model preserving scopes and other settings"},
{"id": "quit", "command": "q\n", "label" : "Quit", "tooltip": "Exit the IG safely"}
],
"presentation_specifics": {
"prompt_title": "ChocoIG> "
}
},
]
}
- An example configuration for ClaferMooVisualizer:
{
"backends": [
{
"id": "choco_moo",
"label": "Choco-based (MOO with magnifier)",
"tooltip": "A multi-objective optimizer based on Choco3 solver library",
"accepted_format": "choco",
"tool": "java",
"tool_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--file=$filepath$", "--moo"],
"tool_version_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--version"],
"optimization_options": {
"set_int_scope" : {"label": "Max. integer:", "argument": "--maxint=$value$", "default_value": 127},
"set_default_scope" : {"label": "Default scopes:", "argument": "--scope=$value$", "default_value": 25}
}
},
]
}- An example configuration for ClaferConfigurator:
{
"backends": [
{
"id": "chocoIG",
"label": "Choco-based (IG + MOO)",
"tooltip": "An instance generator based on Choco3 solver library",
"accepted_format": "choco",
"tool": "java",
"tool_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--file=$filepath$", "--repl"],
"tool_version_args": ["-jar", "/home/<user>/bin/chocosolver.jar", "--version"],
"scope_options": {
"set_default_scope" : {"command": "SetGlobalScope $value$\n"},
"set_individual_scope": {"command": "setScope $clafer$ $value$\n"},
"inc_all_scopes" : {"command": "IncGlobalScope $value$\n"},
"inc_individual_scope": {"command": "incScope $clafer$ $value$\n"},
"set_int_scope" : {"command": "maxInt $value$\n", "default_value": 127}
},
"control_buttons": [
{"id": "next_instance", "command": "n\n", "label" : "Next", "tooltip": "Next Instance"},
{"id": "reload", "command": "r\n", "label" : "Reset", "tooltip": "Reset instance generation, applied scopes and other settings"},
{"id": "quit", "command": "q\n", "label" : "Quit", "tooltip": "Exit the IG safely"}
],
"presentation_specifics": {
"prompt_title": "",
"no_more_instances": "No more instances found. Please consider increasing scopes"
}
},
]
}Notes:
- If you make any changes to the
backends.json, restart the web-tool completely to make the changes take effect. - If you done your configuration properly, the tool will restart successfully and the backend should be listed in the
Backendsdropdown list. If the tool does not start, the reason may be either a syntax error in thebackends.jsonfile, or the paths specified in it are not correct or lead to an inaccessiblejarfile. Also, check theeXecutepermission on thejarfile.
A decimal has a fixed number of fractional digits, the decimal scale of the model, and is solved as an integer: with 2 digits, 19.99 is 1999.
real (the mathematical reals) and double (IEEE 754 floating point) stay unsupported.
Clafer 0.5.5 compiles decimals to the Javascript format (clafer#102), so a .cfr model with decimals works with --file:
price -> decimal = 19.99
compiles to
defaultScope(1);
stringLength(16);
decimalScale(2);
c0_price = Clafer("c0_price").withCard(1, 1);
c0_price.refToUnique(Decimal);
Constraint(implies(some(global(c0_price)), equal(joinRef(global(c0_price)), decimal("19.99"))));
decimalScale(2) is the number of fractional digits: clafer's default is the most fractional digits of the literals, and --decimal-digits of either tool overrides it.
decimalRange("0", "1000") limits the decimals; without it, the range is the largest that fits.
+,-, comparisons,%,sum,min,max, the set operations andif then elseare exact. Integers mix with decimals:100 * priceis exact.decimal * decimaland divisions with a decimal round to the scale, half away from zero:19.99 * 0.13 = 2.5987is2.6, and20.0 / 3is6.67. A division of integers stays an integer division:2 / 3is0.- Equality is exact, after rounding, so a constraint holds only on the grid of the scale:
x * x = 2has no instance with 2 digits, since1.41 * 1.41is1.99and1.42 * 1.42is2.02. Either use more digits (with--decimal-digits=4,xis±1.4142), or allow a tolerance with two inequalities:[ x * x >= 1.98 && x * x <= 2.02 ]givesxis±1.41and±1.42. - The default range is the largest whose scaled values fit Choco's integers: about ±214748.35 with 2 digits, ±21474835 with 0. A decimal reference cannot be beyond it, so an instance whose total does not fit is excluded.
- Instances print decimals in their shortest form with at least one fractional digit:
199.0,12.5. - An optimization objective over decimals reports the scaled value in
ClaferOptimizer.optimalValues(), e.g.1449for14.49. - Not supported yet:
productof decimals, and a set of integers compared with a set of decimals (single values and constants are converted).
src/test/resources/optimization/decimal_bike.js is an attributed feature model with decimal costs, a rounded tax and an average weight, as compiled by clafer; the model is in its first lines.
Consider the following constraint.
[5 + 5 = -6]
For this backend, the constraint is always unsatisfiable. For the Alloy backend, the constraint can be satisfied, depending on the set bitwidth. Why? In the default bitwidth of 4, the number succeeding 7 is -8. Hence 5 + 5 is translated to 5 -> 6 -> 7 -> -8 -> -7 -> -6, hence the constraint is true. For any other bitwidth, the constraint is false. Overflow can be a problem for low bitwidths when dealing with arithmetic (in the new Alloy there's an option which prevents overflows). This backend can also suffer from overflow. It essentially, in regards to overflow, has a fixed bitwidth of 32.
- API for choosing branching strategy. Two reasons. The advantage of constraint programming is the ability to tune the solver to the specific problem. Choosing the right branching strategy can make a world of difference. Secondly, it allows the user to control the order of instances generated. For example, the user would like to see instances where Feature A is present and Feature B is absent before any other instances. This can be done by choosing the branching strategy.
- Reals
- Visit language's website.
- Report issues to issue tracker