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