Code review of pb optimization branch

[Bart Bogaerts]

PB optimization branch needs code review and merge into master (since people are starting to use it in different projects)

[Ignace Bleukx]

One issue I found with the pb_optimization branch is that sometimes a constraint is added twice as symmetry breaking constraint:

For this input file:

* #variable= 5 #constraint= 6
min:
+1 x1 +1 x2 +1 x3  >= +1
+1 x1 +1 x2 +1 x3 +1 x4 +1 x5  >= +1

I get the following output:

$ BreakID -f /tmp/test.opb -pb 10
...
* #variable= 5 #constraint= 6
min:
+1 x1 +1 x2 +1 x3  >= +1
+1 x1 +1 x2 +1 x3 +1 x4 +1 x5  >= +1
+1 x4 -1 x5  >= 0
-1 x1 +1 x3  >= 0
+1 x1 -1 x2  >= 0
+1 x4 -1 x5  >= 0

Where the last constraint is a duplicate of the first symmetry breaking constraint

[Bart Bogaerts]

I would not consider this an issue. It is possible that two symmetry breaking clauses/constraints generated from different symmetries happen to be the same.

[Ignace Bleukx]

I see, possibly related is the following, for this theory:

p cnf 6 3
1 2 0
3 4 0
5 6 0

I get these generators (same on master branch):

$ cat sym.txt
( 3 4 ) ( -3 -4 ) 
( 3 4 ) ( -3 -4 ) 
rows 3 columns 4
1 -1 2 -2 
6 -6 5 -5 
3 -3 4 -4 

Now, if I try to generate the symmetry breaking constraints for this, I use the following command:

$ BreakID -addsym sym.txt
p cnf 6 0%

This works fine, but as soon as I remove th e duplicate permutation, BreakID segfaults on the pb_optimization branch, on master it runs fine. It seems the pb branch tries to read two lines at once.

$ BreakID -addsym sym                                                                                                                                      ignace@ignace-x299
*** Reading instance from input stream.
p cnf 6 0
*** Creating first graph...
*** Detecting symmetry group...
**** total symmetry generators detected: 0
**** strong symmetry generators detected: 0
*** Reading input symmetry from: sym
( 3 4 ) ( -3 -4 ) 
*** Detecting subgroups...
**** subgroups detected: 1
[1]    15894 segmentation fault (core dumped)  BreakID -addsym sym

‌

[Bart Bogaerts]

Ignace’s parsing issue is resolved in commit 6c60366