This site presents a Java library dedicated to problem translation. The input problem has to be specified with Boolean variables and supported input constraints. The output problem is either a propositional or a peudo-Boolean satisfiability problem, which can be solved thanks to any suitable solver.
The workflow consists of two steps: specify a model using Boolean variables and input constraints, then use the available encoding resources to translate these constraints into the chosen output format (CNF or pseudo-Boolean).
Model m = new Model();
Whatever the chosen output format, Boolean variables are simply instances of the Variable class. For convenience, their references can be stocked into an array as follows:
Variable[] x = new Variable[4];
for(int i=0; i<4; i++) x[i] = new Variable();
Internally, each variable is related to a unique identifier that will be used in the output constraints resulting from the translation process. The only way to access to the identifier of a variable v is the v.toString() method.
New versionFriday, 24 October 2008The version 2.0 of BoolVar is online. A class Model were added in order to separate modelization and encoding. All the... + Full Story
Contact'us failure !Saturday, 29 March 2008As a newbie in content management systems, I have just discovered that the "contact us" section does not work ! This... + Full Story