I have tried using minisat+, and now I am using cryptominisat, they support opb format and cnf format respectively. In the opb file, I can use x1 + x2 + x3 + x4 = 2 to represent two truth values out of four unknowns. How do I convert this constraint into a cnf file representation?
Simply speaking I want to be able to make the following constraints in the cnf file: x1 + x2 + x3 + x4 = 2, which shows that only two of the 4 unknowns are true, I don't know how to build the constraint clause.
I asked the cryptominisat developers, this is called, cardinality constraint, and cryptominisat doesn't support this natively, but it is possible to convert this constraint to cnf format via pblib.