Reputation: 1
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