Hard XOR constraints violated

[cenyunuo]

Hi!

I try to use GaussMaxHS to solve a problem with 1600 variables, including 80 exactly-one constraint (hard), 30400 clauses (hard) and 1600 XOR constraints (soft). The XOR constraints are harden using the approach mentioned in "Gaussian Elimination Meets Maximum Satisfiability", section 4.1. At the end, it is encoded as:

p wcnf 3200 96080 1601
x 1601 3 4 6 8 10 13 14 16 17 21 22 25 28 29 30 31 32 33 ...
x 1601 1 5 6 8 10 11 12 17 21 22 23 24 27 28 29 30 31 34 ...
...
c hard clauses
1601 -16 -48 0
1601 -8 -56 0
...
c soft clauses due to harden XOR
1 -1601 0
1 -1602 0
...

Then GaussMaxHS seems to give the solution very fast. However, the solution seems not to be correct.

0.54/0.65   c Wcnf Space Required: 5MB
0.54/0.65   c ================================
0.54/0.65   c Using IBM CPLEX version 22.1.1.0 under IBM's Academic Initiative licencing program
0.54/0.65   o 0
0.54/0.65   c Solved by Init Bnds.
0.54/0.65   o 0
0.54/0.65   s OPTIMUM FOUND
0.54/0.65   v -1 -2 -3 -4 -5 ...

When the size of the problem is smaller (900 XOR hard constraint, length is 451), GaussMaxHS can give the correct solution. In this problem, is it because the XOR constraints are too large (1600 XOR hard constraint, length is 801)?

[msoos]

Hi,

Sorry for the slow answer and thanks for the bug report! Are you sure it's not correct? Do you have the CNF that you used? Can you attach it here? I want to debug.

Thanks,

Mate

[cenyunuo]

Hi,

Sorry for the slow answer and thanks for the bug report! Are you sure it's not correct? Do you have the CNF that you used? Can you attach it here? I want to debug.

Thanks,

Mate

Hi Mate,

Thanks for your response. Please see the attached files I used. cycle_reg_n10_d5_x100_0.txt cycle_reg_n40_d20_x1600_0.txt

n10_d5_x100 is a smaller size instance that gaussmaxhs can generate upper bound and CPLEX can generate lower bound. The output is like

Greedy Solution # 18
c Computing Greedy Solution
c GREEDY: += 6 Clauses. Average size =12.5
c Greedy: soln cost = 13
c Greedy Solution yielded 6 conflicts
c CPLEX returns incumbent with cost 8 and lower bound of 8 time = 0.137944
c CPLEX solution cost = 8 lower bound = 8
c CPLEX found optimal solution to its current model
c after CPLEX bnds: LB = 8 UB = 36
c CPLEX solution yielded 6 conflicts

While for the larger size instance n40_d20_x1600, gaussmaxhs gave result immediately. Except for the output I put above, after printing the model at v line, it was like:

c Solved: Number of falsified softs = 0
c CPLEX: #constraints 0
c CPLEX: Avg constraint size -nan
c CPLEX: #non-core constraints 0
c CPLEX: Ave non-core size -nan
c SAT: #calls 1
c SAT: Total time 0.11827
c SAT: #muser calls 0 (-nan % successful)
c SAT: Minimize time 0 (0%)
c SAT: Avg constraint minimization -nan
c CPLEX: #calls 0
c CPLEX: Total time 0
c GREEDY: #calls 0
c GREEDY: Total time 0
c LP-Bounds: Hardened 0 softs 0 because not in cplex
c LP-Bounds: Relaxed 0 softs
c LP-Bounds: Total time 0
c LP-Bounds: #calls 0
c CPLEX: #calls 0
c CPLEX: Total time 0
c MEM MB: 238
c CPU: 0.503178

Best, Yunuo

[msoos]

Hi,

I'm sorry. Can you please tell me what is the correct solution? You say that the solution does not seem to be correct. But do you have an optimal solution that is better? Or are you only suspecting it to be incorrect? Can you please edit the title to say "is incorrect" instead of "seems incorrect"? I am afraid I can't fix it if I don't know if it's incorrect or not. Sorry,but I need an example where the there is a solution that is definitely better than what GaussMaxHS gives. I just want to be 100% sure this is indeed a bug. Have you got a solution that if you substitute into the formula you get a better optimum than what GaussMaxHS found?

Sorry this is taking so long for me. I am under a lot of deadlines lately :S

Mate

[cenyunuo]

Hi Mate,

Sorry for the confusion. But what I intend to show is that, gaussmaxhs does not generate valid result that satisfies the XOR constraints when solving the cycle_reg_n40_d20_x1600_0.txt instance I put above.

I use the below code to verify.

# verify_xor.py

with open('gaussmaxhs_log.txt', 'r') as f:
    for line in f:
        split = line.split()
        if split[0] == "v":
            res = [int(val) for val in split[1:-1]]

xors = []
with open('cycle_reg_n40_d20_x1600_0.txt', 'r') as f:
    for line in f:
        split = line.split()
        if split[0] == "x":
            lits = [int(val) for val in split[2:-1]]
            xors.append(lits)

sgn = lambda x: (x > 0) - (x < 0)

for xor in xors:
    num_of_true = 0
    for x in xor:
        if sgn(x) * res[abs(x)-1] > 0:
            num_of_true += 1
    print(num_of_true)

And then the output will be:

40
18
24
20
16
16
20
19
20
19
21
21
22
17
20
...

Based on my knowledge, the number of literals to be true should be an odd number such that the XOR constraint can be satisfied. So the results the v line violated the XOR constraints. This be may related to issues #1 and issue #2.

Best, Yunuo