A customizable timetabling software for educational institutions that encodes timetabling constraints as a SAT formula and solves them using a MaxSAT solver
Even if a constraint was disabled, the clauses for that constraint were being added to the formula, while the high level variable corresponding to the set of clauses was not being added.
The high level variable's value was hence free, which could sometimes lead to an incorrect output message that a constraint, that was disabled, could not be satisfied.
This PR fixes this by
not adding unnecessary clauses corresponding to disabled constraints
constraining high level vars of disabled constraints to always be true
Even if a constraint was disabled, the clauses for that constraint were being added to the formula, while the high level variable corresponding to the set of clauses was not being added.
The high level variable's value was hence free, which could sometimes lead to an incorrect output message that a constraint, that was disabled, could not be satisfied.
This PR fixes this by