Running into error when running with file containing XOR vales as x .. ..

[Aditya-2512-kumar]

Hi, below described is the error when I am trying to run a large file containing some XOR values

bool ArjunNS::Arjun::add_xor_clause(const std::vectorCMSat::Lit&, bool): Assertion `false && "Funnily enough this does NOT work. The XORs would generate a BVA variable, and that would then not be returned as part of the simplified CNF. We could calculate a smaller independent set, but that's all."' failed.

How can it work?

[msoos]

Hi,

The solution is to add the XORs as CNF. You can convert them using

https://github.com/msoos/cnf-utils/blob/master/xor_to_cnf.py

Just clone the repository and run it on your CNF. Or, you can blast your XORs into regular CNF too. As you wish 😀 So it works but you have to give it a regular CNF. Don't worry, the extra variables and clauses will make no difference to performance. It'll be fine.

Let me know how it goes,

Mate

[msoos]

I am closing because we don't support XORs this way. They need to be added via CNF as explained above.