constraint-programmingsatchoco

Choco Sat Formulation


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?


Solution

  • 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.