I am trying to model a SAT formula using Choco 4.0.1. I read the docs , I am trying to understand from the javadoc, but unfortunately I am failing so far. This is my first time working on these type of problems and also choco. So, I may be asking something very obvious.
I need to add a number of constraints to the model like (each var is a BoolVar):
x <-> (a and -b)
I am trying to use ifOnlyIf method in Model, but I don't know how to negate a variable, or use and. Could someone provide me (ideally) some sample code or any ideas on how to model these types of constraints?
According to the Choco 4.0.1
online manual, it should be something like this:
SatFactory.addClauses(LogOp.ifOnlyIf(x, LogOp.and(a, LogOp.nor(b))), model);
// with static import of LogOp
SatFactory.addClauses(ifOnlyIf(x, and(a, nor(b))), model);
However, the manual seems to be outdated. Like suggested in the comment, I arrived at:
import static org.chocosolver.solver.constraints.nary.cnf.LogOp.and;
import static org.chocosolver.solver.constraints.nary.cnf.LogOp.ifOnlyIf;
import static org.chocosolver.solver.constraints.nary.cnf.LogOp.nor;
import org.chocosolver.solver.Model;
import org.chocosolver.solver.variables.BoolVar;
public class AkChocoSatDemo {
public static void main(String[] args) {
// 1. Create a Model
Model model = new Model("my first problem");
// 2. Create variables
BoolVar x = model.boolVar("X");
BoolVar a = model.boolVar("A");
BoolVar b = model.boolVar("B");
// 3. Post constraints
// LogOp omitted due to import static ...LogOp.*
model.addClauses(ifOnlyIf(x, and(a, nor(b))));
// 4. Solve the problem
model.getSolver().solve();
// 5. Print the solution
System.out.println(x); // X = 1
System.out.println(a); // A = 1
System.out.println(b); // B = 0
}
}
I have used nor()
with single parameter as not()
to negate an input.