modify a preprocessed cnf

[max-waters]

Coprocessor stores undo information which allows a model of the preprocessed CNF to be translated back into a model of the original CNF. Is it possible to use this undo information to go the other way? Given a variable from the original CNF, can it be determined which variable it has been mapped to in the preprocessed CNF?

The reason I ask is that I would like to modify a CNF after it has been preprocessed, and avoid having to repeat the preprocessing. Let's say I have an input CNF which looks like:

1 2 3 0 
-1 -3 4 0
... 

Coprocessor produces an optimised version of the CNF and some undo information. I'd then like to add a new clause into the CNF:

1 2 3 0 
-1 -3 4 0 
... 
2 0

Currently, I have to add 2 into the original CNF, and then run Coprocessor again. But, if I knew which variable 2 is mapped to in the optimised CNF, then it could be added directly into the optimised CNF instead.

Is this possible? I have read this description of the undo info format but it seems to be outdated -- I'm currently using the version of Coprocessor found here. I've also looked through various versions of the source code but can't figure out how the undo information works.

[conp-solutions]

Hi,

the part of the undo info you are looking for is actually well hidden (sorry for the bad design). When you specify the -undo information with a file, it writes the actual specified file, as well as another file that contains the variable map. That file is called: .map. This mapping shows how variables are mapped, i.e. what happens to a variable "X" (which internally is represented as variable X-1). The file contains 2 arrays, the first is the mapping you are looking for. Variable Index, is mapped to variable array[Index] (again, the -1 offset has to be considered!).

In case you have variables that should not be touched by Coprocessor, you can use the parameter -whiteList to specify a file that contains the variables that should not be changed, so that the set of models for these variables does not change, i.e. you can safely add more clauses with those variable to the formula afterwards. Note, they might still be renamed, so that you need the detour via the tranlation map, or you do not use the "dense" parameter, then no renaming is performed.

Best,
Norbert

PS: I moved the source here: https://github.com/conp-solutions/riss and will likely remove this repository soonish.

[max-waters]

Thanks for this information. I see how the undo map works now. Next, I have a question about how the whitelist works!

Let's say the undo map looks like this:

3 5 12 18 ...

So variable 1 in the preprocessed formula maps to variable 2 in the original, 2 maps to 4, 3 to 11 and so on. But of course nothing in the preprocessed formula maps to 1, 3, 5, 6, 7, etc in the original. This means that the (original) clause 1 3 0 can't be added into the preprocessed formula as it can't be translated.

So I have added the argument -whiteList=whiteListFile, where whiteListFile looks like this:

1 3

But this makes no difference, the undo map remains the same. Am I doing something wrong?

Of course I can get around this by using the -dense arg, but I would rather make the formula smaller if possible.

[nmanthey]

It's been a while since i wrote that code. Could you give a full example of full (including the white file) input, undo info and map as well as simplified formula, and the clause that you would love to submit next. Furthermore, you should compile the tool in debug mode, as that gives you many ...-debug parameters tat show you what actually happens behind the scenes, including writing undo information, and simplification steps. Best, Norbert

[max-waters]

Actually, I still can't figure out the undo map! I have attached some files: undo-tests.zip. The files original.cnf and cp.cnf are the original and preprocessed CNFs. cp_model is a model of the preprocessed CNF, as found by minisat, and model is the result of postprocessing it with undoinfo and undoinfo.map.

There are a couple of mappings which don't make sense to me. For example, the 32nd entry in the undo map (i.e., index 31) is 220. This suggests that variable 32 in the preprocessed model maps to 219 in the postprocessed model. But the preprocessed model contains -32, and the postprocessed model contains 219. Shouldn't it contain -219?

Also, cp.cnf was generated with these flags: -dense -enabled_cp3 -cp3_stats -enabled_cp3 -cp3_stats -up -subsimp -bve -no-bve_gates -no-bve_strength -bve_red_lits=1 -cp3_bve_heap=1 -bve_heap_updates=1 -bve_totalG -bve_cgrow_t=1000 -bve_cgrow=10

[max-waters]

Also, I think I know why the whitelist was having no effect -- I was only using equivalence-preserving techniques. Which makes me wonder -- which equivalence-preserving techniques will remove variables? Equivalence elimination I suppose. Are there any others?

Ps thanks for your help with this. I know a bit about SAT solving/processing, but (as you can maybe tell) not enough yet!