Scippy

SCIP

Solving Constraint Integer Programs

compute_symmetry_sassy_nauty.cpp
Go to the documentation of this file.
1/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2/* */
3/* This file is part of the program and library */
4/* SCIP --- Solving Constraint Integer Programs */
5/* */
6/* Copyright (c) 2002-2025 Zuse Institute Berlin (ZIB) */
7/* */
8/* Licensed under the Apache License, Version 2.0 (the "License"); */
9/* you may not use this file except in compliance with the License. */
10/* You may obtain a copy of the License at */
11/* */
12/* http://www.apache.org/licenses/LICENSE-2.0 */
13/* */
14/* Unless required by applicable law or agreed to in writing, software */
15/* distributed under the License is distributed on an "AS IS" BASIS, */
16/* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
17/* See the License for the specific language governing permissions and */
18/* limitations under the License. */
19/* */
20/* You should have received a copy of the Apache-2.0 license */
21/* along with SCIP; see the file LICENSE. If not visit scipopt.org. */
22/* */
23/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
24
25/**@file compute_symmetry_sassy_nauty.cpp
26 * @brief interface for symmetry computations to sassy as a preprocessor to nauty
27 * @author Marc Pfetsch
28 * @author Gioni Mexi
29 * @author Christopher Hojny
30 */
31
32/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
33
34#include "compute_symmetry.h"
35
36/* the following determines whether nauty or traces is used: */
37#define NAUTY
38
39#ifdef NAUTY
40#include "nauty/nauty.h"
41#include "nauty/nausparse.h"
42#else
43#include "nauty/traces.h"
44#endif
45
46/* include sassy (as part of dejavu) */
47#include "build_dejavu_graph.h"
48#ifdef __GNUC__
49#pragma GCC diagnostic ignored "-Wshadow"
50#endif
51
52#ifdef _MSC_VER
53# pragma warning(push)
54# pragma warning(disable: 4456) // shadowed variable
55#endif
56
57#ifdef NAUTY
58#include "dejavu/tools/nauty_converter.h"
59#else
60#include "dejavu/tools/traces_converter.h"
61#endif
62
63#ifdef __GNUC__
64#pragma GCC diagnostic warning "-Wshadow"
65#endif
66
67#ifdef _MSC_VER
68# pragma warning(pop)
69#endif
70
71#include "scip/expr_var.h"
72#include "scip/expr_sum.h"
73#include "scip/expr_pow.h"
74#include "scip/expr.h"
75#include "scip/cons_nonlinear.h"
76#include "scip/cons_linear.h"
77#include "scip/scip_mem.h"
78#include "scip/symmetry_graph.h"
79#include "tinycthread/tinycthread.h"
80
81/** struct for symmetry callback */
82struct SYMMETRY_Data
83{
84 SCIP* scip; /**< SCIP pointer */
85 SYM_SYMTYPE symtype; /**< type of symmetries that need to be computed */
86 int npermvars; /**< number of variables for permutations */
87 int nperms; /**< number of permutations */
88 int** perms; /**< permutation generators as (nperms x npermvars) matrix */
89 int nmaxperms; /**< maximal number of permutations */
90 int maxgenerators; /**< maximal number of generators constructed (= 0 if unlimited) */
91 SCIP_Bool restricttovars; /**< whether permutations shall be restricted to variables */
92};
93
94#ifdef NAUTY
95/** struct for nauty callback */
96struct NAUTY_Data
97{
98 SCIP* scip; /**< SCIP pointer */
99 int maxlevel; /**< maximum depth level of nauty's search tree (-1: unlimited) */
100};
101
102/** static data for nauty callback */
103#if defined(_Thread_local)
104static _Thread_local struct NAUTY_Data nautydata_;
105#else
106static struct NAUTY_Data nautydata_;
107#endif
108
109#endif
110
111/* ------------------- hook functions ------------------- */
112
113/** callback function for sassy */ /*lint -e{715}*/
114static
116 void* user_param, /**< parameter supplied at call to sassy */
117 int n, /**< dimension of permutations */
118 const int* aut, /**< permutation */
119 int nsupp, /**< support size */
120 const int* suppa /**< support list */
121 )
122{
123 assert( aut != NULL );
124 assert( user_param != NULL );
125
126 SYMMETRY_Data* data = static_cast<SYMMETRY_Data*>(user_param);
127 assert( data->scip != NULL );
128 assert( data->maxgenerators >= 0 );
129
130 /* make sure we do not generate more that maxgenerators many permutations */
131 if ( data->maxgenerators != 0 && data->nperms >= data->maxgenerators )
132 return;
133
134 /* copy first part of automorphism */
135 bool isIdentity = true;
136 int* p = 0;
137 int permlen;
138 if ( data->restricttovars )
139 {
140 switch ( data->symtype )
141 {
142 case SYM_SYMTYPE_PERM:
143 permlen = data->npermvars;
144 break;
145 default:
146 assert( data->symtype == SYM_SYMTYPE_SIGNPERM );
147 permlen = 2 * data->npermvars;
148 }
149 }
150 else
151 permlen = n;
152
153 /* check whether permutation is identity */
154 for (int j = 0; j < permlen; ++j)
155 {
156 if ( (int) aut[j] != j )
157 isIdentity = false;
158 }
159
160 /* don't store identity permutations */
161 if ( isIdentity )
162 return;
163
164 if ( SCIPallocBlockMemoryArray(data->scip, &p, permlen) != SCIP_OKAY )
165 return;
166
167 /* store symmetry */
168 for (int j = 0; j < permlen; ++j)
169 p[j] = (int) aut[j];
170
171 /* check whether we should allocate space for perms */
172 if ( data->nmaxperms <= 0 )
173 {
174 if ( data->maxgenerators == 0 )
175 data->nmaxperms = 100; /* seems to cover many cases */
176 else
177 data->nmaxperms = data->maxgenerators;
178
179 if ( SCIPallocBlockMemoryArray(data->scip, &data->perms, data->nmaxperms) != SCIP_OKAY )
180 return;
181 }
182 else if ( data->nperms >= data->nmaxperms ) /* check whether we need to resize */
183 {
184 int newsize = SCIPcalcMemGrowSize(data->scip, data->nperms + 1);
185 assert( newsize >= data->nperms );
186 assert( data->maxgenerators == 0 );
187
188 if ( SCIPreallocBlockMemoryArray(data->scip, &data->perms, data->nmaxperms, newsize) != SCIP_OKAY )
189 return;
190
191 data->nmaxperms = newsize;
192 }
193
194 data->perms[data->nperms++] = p;
195}
196
197#ifdef NAUTY
198
199/** callback function for nauty to terminate early */ /*lint -e{715}*/
200static
202 graph* g, /**< sparse graph for nauty */
203 int* lab, /**< labels of node */
204 int* ptn, /**< array indicating change of set in node parition of graph */
205 int level, /**< level of current node in nauty's tree */
206 int numcells, /**< number of cells in current partition */
207 int tc, /**< index of target cells in lab if children need to be explored */
208 int code, /**< code produced by refinement and vertex-invariant procedures */
209 int m, /**< number of edges in the graph */
210 int n /**< number of nodes in the graph */
211 )
212{ /* lint --e{715} */
213 /* add level limit to work around call stack overflow in nauty */
214 if ( level > nautydata_.maxlevel && nautydata_.maxlevel >= 0 )
215 {
217 "symmetry computation terminated early because Nauty level limit %d is exceeded\n",
220 "for running full symmetry detection, increase value of parameter propagating/symmetry/nautymaxlevel\n");
221 nauty_kill_request = 1;
222 }
223}
224
225#endif
226
227/** return whether symmetry can be computed */
229{
230 return TRUE;
231}
232
233/** nauty/traces version string */
234#ifdef NAUTY
235static const char nautyname[] = {'N', 'a', 'u', 't', 'y', ' ', NAUTYVERSIONID/10000 + '0', '.', (NAUTYVERSIONID%10000)/1000 + '0', '.', (NAUTYVERSIONID%1000)/10 + '0', '\0'};
236#else
237static const char nautyname[] = {'T', 'r', 'a', 'c', 'e', 's', ' ', NAUTYVERSIONID/10000 + '0', '.', (NAUTYVERSIONID%10000)/1000 + '0', '.', (NAUTYVERSIONID%1000)/10 + '0', '\0'};
238#endif
239
240/** return name of external program used to compute generators */
241const char* SYMsymmetryGetName(void)
242{
243 return nautyname;
244}
245
246/** return description of external program used to compute generators */
247const char* SYMsymmetryGetDesc(void)
248{
249#ifdef NAUTY
250 return "Computing Graph Automorphism Groups by Brendan D. McKay (users.cecs.anu.edu.au/~bdm/nauty)";
251#else
252 return "Computing Graph Automorphism Groups by Adolfo Piperno (pallini.di.uniroma1.it)";
253#endif
254}
255
256#define STR(x) #x
257#define XSTR(x) STR(x)
258
259/** return name of additional external program used for computing symmetries */
260const char* SYMsymmetryGetAddName(void)
261{
262 return "sassy " XSTR(SASSY_VERSION_MAJOR) "." XSTR(SASSY_VERSION_MINOR);
263}
264
265/** return description of additional external program used to compute symmetries */
266const char* SYMsymmetryGetAddDesc(void)
267{
268 return "Symmetry preprocessor by Markus Anders (github.com/markusa4/sassy)";
269}
270
271/** computes autormorphisms of a graph */
272static
274 SCIP* scip, /**< SCIP pointer */
275 SYM_SYMTYPE symtype, /**< type of symmetries that need to be computed */
276 dejavu::static_graph* G, /**< pointer to graph for that automorphisms are computed */
277 int nsymvars, /**< number of variables encoded in graph */
278 int maxgenerators, /**< maximum number of generators to be constructed (=0 if unlimited) */
279 int*** perms, /**< pointer to store generators as (nperms x npermvars) matrix */
280 int* nperms, /**< pointer to store number of permutations */
281 int* nmaxperms, /**< pointer to store maximal number of permutations
282 * (needed for freeing storage) */
283 SCIP_Real* log10groupsize, /**< pointer to store log10 of size of group */
284 SCIP_Bool restricttovars, /**< whether permutations shall be restricted to variables */
285 SCIP_Real* symcodetime, /**< pointer to store the time for symmetry code */
286 SCIP_Bool canterminateearly /**< whether we allow to interrupt symmetry detection early
287 * (e.g., because of iteration limits) */
288 )
289{
290 SCIP_Real oldtime;
291
292 assert( scip != NULL );
293 assert( G != NULL );
294 assert( maxgenerators >= 0 );
295 assert( perms != NULL );
296 assert( nperms != NULL );
297 assert( nmaxperms != NULL );
298 assert( log10groupsize != NULL );
299 assert( symcodetime != NULL );
300
301 /* init */
302 *nperms = 0;
303 *nmaxperms = 0;
304 *perms = NULL;
305 *log10groupsize = 0.0;
306 *symcodetime = 0.0;
307
308 /* init data */
309 struct SYMMETRY_Data data;
310 data.scip = scip;
311 data.symtype = symtype;
312 data.npermvars = nsymvars;
313 data.nperms = 0;
314 data.nmaxperms = 0;
316 data.perms = NULL;
318
319#ifdef NAUTY
321 SCIP_CALL( SCIPgetIntParam(scip, "propagating/symmetry/nautymaxlevel", &nautydata_.maxlevel) );
322#endif
323
324 oldtime = SCIPgetSolvingTime(scip);
325
326 /* set up sassy preprocessor */
327 dejavu::preprocessor sassy;
328
329 /* lambda function to have access to data and pass it to sassyhook above */
330 dejavu_hook sassyglue = [&](int n, const int* p, int nsupp, const int* suppa) {
331 sassyhook((void*)&data, n, p, nsupp, suppa);
332 };
333
334 /* call sassy to reduce graph */
335 sassy.reduce(G, &sassyglue);
336
337 if( G->get_sgraph()->v_size == 0 )
338 {
339 dejavu::big_number grp_sz = sassy.grp_sz;
340 *log10groupsize = (SCIP_Real) log10l(grp_sz.mantissa * powl(10.0, (SCIP_Real) grp_sz.exponent));
341 }
342 else
343 {
344 /* first, convert the graph */
345 sparsegraph sg;
346 DYNALLSTAT(int, lab, lab_sz);
347 DYNALLSTAT(int, ptn, ptn_sz);
348
349#ifdef NAUTY
350 convert_dejavu_to_nauty(G, &sg, &lab, &lab_sz, &ptn, &ptn_sz);
351 assert( sg.nv > 0 );
352
353 statsblk stats;
354 DYNALLSTAT(int, orbits, orbits_sz);
355 DYNALLOC1(int, orbits, orbits_sz, sg.nv, "malloc");
356 DEFAULTOPTIONS_SPARSEGRAPH(options);
357 /* init callback functions for nauty (accumulate the group generators found by nauty) */
358 options.writeautoms = FALSE;
359 options.userautomproc = dejavu::preprocessor::nauty_hook;
360 options.defaultptn = FALSE; /* use color classes */
361 if ( canterminateearly )
362 options.usernodeproc = nautyterminationhook;
363 sparsenauty(&sg, lab, ptn, orbits, &options, &stats, NULL);
364 dejavu::big_number grp_sz = sassy.grp_sz;
365 *log10groupsize = log10(stats.grpsize1 * grp_sz.mantissa * pow(10.0, (SCIP_Real) (stats.grpsize2 + grp_sz.exponent)));
366#else
367 convert_dejavu_to_traces(&sassygraph, &sg, &lab, &lab_sz, &ptn, &ptn_sz);
368 TracesStats stats;
369 DYNALLSTAT(int, orbits, orbits_sz);
370 DYNALLOC1(int, orbits, orbits_sz, sg.nv, "malloc");
371 DEFAULTOPTIONS_TRACES(options);
372 /* init callback functions for traces (accumulate the group generators found by traces) */
373 options.writeautoms = FALSE;
374 options.userautomproc = dejavu::preprocessor::traces_hook;
375 options.defaultptn = FALSE; /* use color classes */
376 Traces(&sg, lab, ptn, orbits, &options, &stats, NULL);
377 dejavu::big_number grp_sz = sassy.grp_sz;
378 *log10groupsize = log10(stats.grpsize1 * grp_sz.mantissa * pow(10.0, (SCIP_Real) (stats.grpsize2 + grp_sz.exponent)));
379#endif
380
381 /* clean up */
382 DYNFREE(lab, lab_sz);
383 DYNFREE(ptn, ptn_sz);
384 SG_FREE(sg);
385 }
386
387 *symcodetime = SCIPgetSolvingTime(scip) - oldtime;
388
389 /* prepare return values */
390 if ( data.nperms > 0 )
391 {
392 *perms = data.perms;
393 *nperms = data.nperms;
394 *nmaxperms = data.nmaxperms;
395 }
396 else
397 {
398 assert( data.perms == NULL );
399 assert( data.nmaxperms == 0 );
400
401 *perms = NULL;
402 *nperms = 0;
403 *nmaxperms = 0;
404 }
405
406 return SCIP_OKAY;
407}
408
409/** compute generators of symmetry group */
411 SCIP* scip, /**< SCIP pointer */
412 int maxgenerators, /**< maximal number of generators constructed (= 0 if unlimited) */
413 SYM_GRAPH* symgraph, /**< symmetry detection graph */ /* cppcheck-suppress funcArgNamesDifferent */
414 int* nperms, /**< pointer to store number of permutations */
415 int* nmaxperms, /**< pointer to store maximal number of permutations (needed for freeing storage) */
416 int*** perms, /**< pointer to store permutation generators as (nperms x npermvars) matrix */
417 SCIP_Real* log10groupsize, /**< pointer to store log10 of size of group */
418 SCIP_Real* symcodetime /**< pointer to store the time for symmetry code */
419 )
420{
421 SCIP_Bool success = FALSE;
422
423 assert( scip != NULL );
424 assert( maxgenerators >= 0 );
425 assert( symgraph != NULL );
426 assert( nperms != NULL );
427 assert( nmaxperms != NULL );
428 assert( perms != NULL );
429 assert( log10groupsize != NULL );
430 assert( symcodetime != NULL );
431
432 /* init */
433 *nperms = 0;
434 *nmaxperms = 0;
435 *perms = NULL;
436 *log10groupsize = 0;
437 *symcodetime = 0.0;
438
439 /* create sassy graph */
440 dejavu::static_graph sassygraph;
441
442 SCIP_CALL( SYMbuildDejavuGraph(scip, &sassygraph, symgraph, &success) );
443
444 /* compute symmetries */
446 maxgenerators, perms, nperms, nmaxperms, log10groupsize, TRUE, symcodetime, TRUE) );
447
448 return SCIP_OKAY;
449}
450
451/** returns whether two given graphs are identical */
453 SCIP* scip, /**< SCIP pointer */
454 SYM_SYMTYPE symtype, /**< type of symmetries to be checked */
455 SYM_GRAPH* G1, /**< first graph */
456 SYM_GRAPH* G2 /**< second graph */
457 )
458{
459 int** perms;
460 int nnodes;
461 int nperms;
462 int nmaxperms;
463 int nnodesfromG1;
464 SCIP_Real symcodetime = 0.0;
465 SCIP_Real log10groupsize;
466 SCIP_Bool success;
467
468 /* create sassy graph */
469 dejavu::static_graph sassygraph;
470
471 SCIP_CALL( SYMbuildDejavuGraphCheck(scip, &sassygraph, G1, G2, &nnodes, &nnodesfromG1, &success) );
472
473 if ( ! success )
474 return FALSE;
475
476 /* compute symmetries */
478 &perms, &nperms, &nmaxperms, &log10groupsize, FALSE, &symcodetime, FALSE) );
479
480 /* since G1 and G2 are connected and disjoint, they are isomorphic iff there is a permutation
481 * mapping a node from G1 to a node of G2
482 */
483 success = FALSE;
484 for (int p = 0; p < nperms && ! success; ++p)
485 {
486 for (int i = 0; i < nnodesfromG1; ++i)
487 {
488 if ( perms[p][i] >= nnodesfromG1 )
489 {
490 success = TRUE;
491 break;
492 }
493 }
494 }
495
496 for (int p = 0; p < nperms; ++p)
497 {
499 }
501
502 return success;
503}
SCIP_RETCODE SYMbuildDejavuGraphCheck(SCIP *scip, dejavu::static_graph *dejavugraph, SYM_GRAPH *G1, SYM_GRAPH *G2, int *nnodes, int *nnodesfromG1, SCIP_Bool *success)
SCIP_RETCODE SYMbuildDejavuGraph(SCIP *scip, dejavu::static_graph *dejavugraph, SYM_GRAPH *graph, SCIP_Bool *success)
methods to build dejavu graph for symmetry detection
interface for symmetry computations
SCIP_Bool SYMcheckGraphsAreIdentical(SCIP *scip, SYM_SYMTYPE symtype, SYM_GRAPH *G1, SYM_GRAPH *G2)
const char * SYMsymmetryGetName(void)
static const char nautyname[]
const char * SYMsymmetryGetAddName(void)
static _Thread_local struct NAUTY_Data nautydata_
SCIP_Bool SYMcanComputeSymmetry(void)
const char * SYMsymmetryGetDesc(void)
static void sassyhook(void *user_param, int n, const int *aut, int nsupp, const int *suppa)
static SCIP_RETCODE computeAutomorphisms(SCIP *scip, SYM_SYMTYPE symtype, dejavu::static_graph *G, int nsymvars, int maxgenerators, int ***perms, int *nperms, int *nmaxperms, SCIP_Real *log10groupsize, SCIP_Bool restricttovars, SCIP_Real *symcodetime, SCIP_Bool canterminateearly)
#define XSTR(x)
static void nautyterminationhook(graph *g, int *lab, int *ptn, int level, int numcells, int tc, int code, int m, int n)
const char * SYMsymmetryGetAddDesc(void)
SCIP_RETCODE SYMcomputeSymmetryGenerators(SCIP *scip, int maxgenerators, SYM_GRAPH *symgraph, int *nperms, int *nmaxperms, int ***perms, SCIP_Real *log10groupsize, SCIP_Real *symcodetime)
Constraint handler for linear constraints in their most general form, .
constraint handler for nonlinear constraints specified by algebraic expressions
#define NULL
Definition: def.h:248
#define SCIP_Bool
Definition: def.h:91
#define SCIP_Real
Definition: def.h:156
#define TRUE
Definition: def.h:93
#define FALSE
Definition: def.h:94
#define SCIP_CALL_ABORT(x)
Definition: def.h:334
#define SCIP_CALL(x)
Definition: def.h:355
private functions to work with algebraic expressions
power and signed power expression handlers
sum expression handler
variable expression handler
#define nnodes
Definition: gastrans.c:74
void SCIPverbMessage(SCIP *scip, SCIP_VERBLEVEL msgverblevel, FILE *file, const char *formatstr,...)
Definition: scip_message.c:225
SCIP_RETCODE SCIPgetIntParam(SCIP *scip, const char *name, int *value)
Definition: scip_param.c:269
#define SCIPfreeBlockMemoryArray(scip, ptr, num)
Definition: scip_mem.h:110
int SCIPcalcMemGrowSize(SCIP *scip, int num)
Definition: scip_mem.c:139
#define SCIPallocBlockMemoryArray(scip, ptr, num)
Definition: scip_mem.h:93
#define SCIPreallocBlockMemoryArray(scip, ptr, oldnum, newnum)
Definition: scip_mem.h:99
#define SCIPfreeBlockMemoryArrayNull(scip, ptr, num)
Definition: scip_mem.h:111
SCIP_Real SCIPgetSolvingTime(SCIP *scip)
Definition: scip_timing.c:378
SYM_SYMTYPE SCIPgetSymgraphSymtype(SYM_GRAPH *graph)
int SCIPgetSymgraphNVars(SYM_GRAPH *graph)
public methods for memory management
SYM_SYMTYPE symtype
SCIP_Bool restricttovars
methods for dealing with symmetry detection graphs
@ SCIP_VERBLEVEL_MINIMAL
Definition: type_message.h:59
@ SCIP_OKAY
Definition: type_retcode.h:42
enum SCIP_Retcode SCIP_RETCODE
Definition: type_retcode.h:63
enum SYM_Symtype SYM_SYMTYPE
Definition: type_symmetry.h:64
@ SYM_SYMTYPE_SIGNPERM
Definition: type_symmetry.h:62
@ SYM_SYMTYPE_PERM
Definition: type_symmetry.h:61