nmanthey / riss-solver Goto Github PK

in the coprocessor-module, the given link
http://tools.computational-logic.org
points to nowhere.
the documentation here is not precise, whether this is Coprocessor 2 or an earlier version.
Is the Coprocessor 2 standalone sourcecode available somewhere ?

I have found that using the -dense flag with Coprocessor produces an invalid CNF. The problem is that a model of the preprocessed CNF, when translated back using the undo info, is not a valid model of the original CNF.

I have attached a small script to demonstrate the problem (undo-test.zip). It can be run with, for example, ./undo-test.sh example.cnf 10.

This hasn't been tested against the latest version of riss, as I haven't been able to get it to build. But, before I spend ages trying to compile the latest version, could you confirm whether or not this is a bug, and if so whether it exists in the latest version?

Sometimes the simplified CNF produced by coprocessor is empty. I don't know how to interpret this result.

For example, here's a very simple CNF:

p cnf 3 3
1 -2 -3 0
-1 2 -3 0
-1 -2 3 0

Run the command:

./coprocessor -dimacs=preprocessed -enabled_cp3 -ppOnly -rate input

The contents of the file preprocessed is simply:

p cnf 3 0

Is it an error? Or does it imply that input cannot be simplified?

When using dynamic linking against the IPASIR interface, two libraries would have to be used for Riss, as Coprocessor comes in its own library.

Similarly to the static library, add a rule to build a dynamic library, and build it when IPASIR is build.

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.

Mis-spelling a flag when running coprocessor results in the input file being deleted. For example:

./coprocessor -TYPO -dimacs=preprocessed -enabled_cp3 -bve input

Resuls in this output:

c ERROR! Could not open file: -TYPO

And the file input is now empty!

• simplify check for sharing clauses

• check better if LBD really has to be recomputed on success for all clauses (might be possible during checking next watched literal)