Enhancements to preprocessing - for dumpresult files and multiple solutions

[ajohnson1]

The preprocessing step 2 (--preproc 2) works with cryptominisat5 output, but not with results files (segfault).

Output format

s SATISFIABLE v 1 -2 v 3 0

Results files are given by --dumpresult and are of the format: SAT 1 -2 3 0

Other solvers also output files with just the variable values. 1 -2 3 0

Those file formats cause a segfault.

Also, preprocessing doesn't work with multiple solutions (--maxsol). That would be a nice enhancement. The preprocessed file might have multiple solutions, or extra multiple solutions might be generated from a single solution when postprocessing the intermediate result file.

[msoos]

--maxsol does not work indeed. That I think is OK and intended.

The other solvers' result file -- I' confused. Minisat is what all the other solvers are supposed to emulate in this regard, as that was the first one to emit these. It emits:

SAT
1 -2 0

Hence I'm following the golden setup. The fact that other solvers messed this up is beyond my control :( Most applications that were built on Minisat expect this output.

Actually, I have no trouble dumping the result to a file:

./cryptominisat5 --preproc 1 a.cnf --savedstate x simp
./cryptominisat5 simp > out
./cryptominisat5 --preproc 2 --savedstate x out --dumpres aaa
cat aaa

These work well for me. Do you have a CNF for which this doesn't work?

[ajohnson1]

Here are some commands

cryptominisat5 --preproc 1 a.cnf --savedstate x simp
cryptominisat5 simp --dumpres dump1 >out1
cryptominisat5 simp --dumpres dump2 --maxsol 2 >out2
cryptominisat5 simp --dumpres dump2a --maxsol 5 >out2a
glucose.exe -model simp >out3
glucose.exe -model simp dump4 >out4
cryptominisat5 --preproc 2 out1 --savedstate x
cryptominisat5 --preproc 2 out2 --savedstate x
cryptominisat5 --preproc 2 out2a --savedstate x
cryptominisat5 --preproc 2 out3 --savedstate x
cryptominisat5 --preproc 2 out4 --savedstate x
cryptominisat5 --preproc 2 dump1 --savedstate x
cryptominisat5 --preproc 2 dump2 --savedstate x
cryptominisat5 --preproc 2 dump2a --savedstate x
cryptominisat5 --preproc 2 dump4 --savedstate x

out1, has the form:

c comments
s SATISFIABLE
v -1 -2 3 4 -5 6 -7 8 -9 -10 -11 -12 13 14 15 -16 17 18 -19 20 -21 -22 23 24 25
v 26 27 28 -29 -30 31 -32 33 -34 35 -36 37 -38 39 40 -41 42 -43 -44 45 46 -47

out2 has the form with 2 solutions:

c comments
s SATISFIABLE
v -1 -2 3 4 -5 6 -7 8 -9 -10 -11 -12 13 14 15 -16 17 18 -19 20 -21 -22 23 24 25
v 26 27 28 -29 -30 31 -32 33 -34 35 -36 37 -38 39 40 -41 42 -43 -44 45 46 -47
c comments
s SATISFIABLE
v -1 2 3 -4 -5 6 7 8 -9 -10 -11 -12 -13 14 -15 16 17 18 19 20 -21 22 -23 -24 -25 
v -26 27 28 -29 30 31 -32 -33 34 35 36 -37 38 -39 -40 41 42 43 44 -45 -46 47 48

out2a has 2 solutions and a line

c comments
s SATISFIABLE
v -1 -2 3 4 -5 6 -7 8 -9 -10 -11 -12 13 14 15 -16 17 18 -19 20 -21 -22 23 24 25
v 26 27 28 -29 -30 31 -32 33 -34 35 -36 37 -38 39 40 -41 42 -43 -44 45 46 -47
c comments
s SATISFIABLE
v -1 2 3 -4 -5 6 7 8 -9 -10 -11 -12 -13 14 -15 16 17 18 19 20 -21 22 -23 -24 -25 
v -26 27 28 -29 30 31 -32 -33 34 35 36 -37 38 -39 -40 41 42 43 44 -45 -46 47 48
c comments
s UNSATISFIABLE

out3 has the form where the result v is all one line

c comments
s SATISFIABLE
v -1 -2 3 4 -5 6 -7 8 -9 -10 -11 -12 13 14 15 -16 17 18 -19 20 -21 -22 23 24 25 26 27 28 -29 -30 31 -32 33 -34 35 -36 37 -38 39 40 -41 42 -43 -44 45 46 -47

out4 doesn't have a variables line

c CPU time              : 26.754 s

s SATISFIABLE
SAT

dump1 has the form

SAT
-1 -2 3 4 -5 6 -7 8 -9 -10 -11

dump2 has the form with two solutions

SAT
-1 -2 3 4 -5 6 -7 8 -9 -10 -11
SAT
-1 2 3 -4 -5 6 7 8 -9 -10 -11 -12 -13 14 -15 16

dump2a has the form

SAT
-1 -2 3 4 -5 6 -7 8 -9 -10 -11
SAT
-1 2 3 -4 -5 6 7 8 -9 -10 -11 -12 -13 14 -15 16
UNSAT

dump4 has the form (no SAT line)

-1 -2 3 4 -5 6 -7 8 -9 -10 -11

The postprocessing gives a solution for out1 and out2 (possibly the second solution in the file). out2a gives

s UNSATISFIABLE

possibly because it takes the last solution found in the file. postprocessing out3 gives a solution postprocessing out4 which has no variable line gives

s SATISFIABLE
v -1 -4 -48 -60 -85 -86 -87 -88 89 -90 -103 104 -105 -106 -107 -108 -554 606 0
c NOTE: 1068 varables are NOT set

which is a bit odd.

dump1, dump2, dump2a, dump4 all give Segmentation fault (core dumped)

so preprocessing does work with stdout files but not dump result files. It would be nice, but not essential if it could also read dump result files.

For multiple solutions - this would be an enhancement. The --preproc 2 step could read multiple solutions from the file and generate a solution in the original form for each.

Can preprocessing break symmetries? E.g. if variable 1 and 2 were symmetric in usage but had to hold opposite values the preprocessor could make 1 true and 2 false. That would mean that one solution to the preprocessed file could expand back to multiple solutions in the original form.

[msoos]

Hi! First of all, I really appreciate you work here. Just to get some things out of the way:

glucose.exe -model simp >out3
glucose.exe -model simp dump4 >out4

Their output does not concern me. Yes, the authors decided not to output the solution. Yes, the authors decided to output the variables in one line. Good for them.

Again --maxsol does not work with preprocessing. It will segfault, give you wrong solutions, it might even cause a nuclear meltdown. I cannot vouch for what it will do. However, I will now write some code so that if you feed it an ouptut that you put above, it will simply exit(-1) with an error. That should fix some of the issues. If any more remain, please create a merge request so that all the issues above exit with a -1 code. Thank you!

You can always just cut the output:

s SATISFIABLE
v 1 2 0
s SATISFIABLE
v 1 -2 0
s UNSATISFIABLE

And feed it separately, in 3 parts, to --preprocess 2. That will always work.

By the way, CyrptoMiniSat of course preprocesses the problem when doing --maxsol, so I don't really understand why you want to use preprocessing when the main solver you will use is CryptoMiniSat :) If you want to use glucose, then --maxsol doesn't matter because glucose doesn't have that option anyway...