Jay Hurley
Jay Hurley

Reputation: 1

Reversing the CNF conversion after MAXSAT solve

I have a boolean expression and wish to find valid values that maximize the number of true variables. Typical MAXSAT problem. The original expression is not in CNF form, so I used a converter. The conversion to CNF introduces many new variables. After solving the problem in CNF form, I need to get back to my original variable values to apply the solution.

I first generated the expression to be maximized. It's not relevant to this discussion but it comes from a geometry problem. The original input expression looks something like this:

( v3 & !v0 ) & ( v2 & !v0 ) & ( v1 & !v0 ) & ( v6 & v17 & !v0 ) ...

Where there are some number of variables denoted v0, v1, etc.

I used limboole to convert this expression into a cnf formated file.

limboole.exe -d expressionfilename.txt

The output of which looks like...

c 1 v3 c 2 v0 c 5 v2 c 8 v1 c 11 v6 c 12 v17 c 16 v5 c 20 v7 c 21 v13 c 28 v9 c 35 v15 c 36 v19 c 40 v11 c 41 v18 c 48 v10 c 49 v14 c 380 v4 c 388 v16 c 395 v12 c 402 v8 p cnf 1559 4598 3 2 0 -3 -2 0 -4 1 0 -4 3 0 4 -1 -3 0 ... ...

I then used sat4j to find an optimal solution for the cnf file, which looks like...

v -1 -2 3 -4 5 -6 -7 -8 -9 10 11 -12 -13 -14 ... ...

and has 1559 values, as it should.

My question is, now that I have a solution to the post-cnf conversion form, how do I relate those values back to my original v0,v1... variables? thanks for the help!

Upvotes: 0

Views: 68

Answers (0)

Related Questions