CNF conversion

[markus hecher]

Hi all,

So I am converting a fzn file into a cnf file using fzn_picat_sat.pi.

Unfortunately, I am not able to figure out which variables in the translated cnf file belong to the output variables of the fzn file. Is there a possibility to somehow see or mark/highlight the variables in the cnf file that are present in the output_array of the fzn file to make them distinguishable from the newly introduced variables when converting to cnf? The conversion to the cnf file is done using an option argument in the bp.sat_solve call, which also gets the list of variables, so I am guessing that I have to somehow tell this call or intervene in order to mark the variables, if this is possible.

Thank you for your help!

Kind regards,

Markus Hecher

[Neng-Fa Zhou]

Hi,

May I ask why you need to know the correspondence between the problem variables and the CNF variables? If you'd like to use a separate SAT solver, you could replace the default solver (kissat) with yours through the C interface. Once CNF code is dumped, there is no way to know the original problem variable of the CNF variables.

Cheers,

NF

[markus hecher]

Hi,

Thanks for the quick response. So we were just wondering regarding relationships between solutions / satisfying assignments. But I guess this answers the question negatively :/.

Best,

Markus