markirch / sat-modulo-symmetries

MIT License
4 stars 4 forks source link

How to obtain graphs cleanly? #22

Closed lichengzhang1 closed 6 months ago

lichengzhang1 commented 1 year ago

Hello,

When I run the following command (or similar ones), I got a lot of output.

python ./graph_builder.py -v 6 --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 >output.txt

Arguments: Namespace(vertices=6, cnf_file=None, directed=False, multigraph=None, underlying_graph=False, static_partition=False, counter='sequential', DEBUG=1, all_graphs=True, hide_graphs=False, args_SMS='', num_edges_upp=12, num_edges_low=10, Delta_upp=None, delta_low=None, even_degrees=False, no_subsuming_neighborhoods=False, degree_partition=False, chi_upp=None, chi_low=None, Ck_free=None, mtf=False, girth=None, girth_compact=None, alpha_upp=None, omega_upp=None, ramsey=None, planar_kuratowski=False, connectivity_low=3, diam2_critical=False, forbidden_subgraphs=None, forbidden_induced_subgraphs=None)
running the command:  time smsg --vertices 6 --print-stats True --frequency 30 --all-graphs   --dimacs ./temp97.enc
Number of vertices: 6
Initial partition:0 0 0 0 0 0 
Clauses: 5841, Variables 1881
SAT Solver: Cadical
Start solving
Solution 1
[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)]
Solution 2
[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)]
Solution 3
[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)]
Solution 4
[(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)]
Solution 5
[(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)]
Solution 6
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(3,5),(4,5)]
Solution 7
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(4,5)]
Solution 8
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,5),(4,5)]
Solution 9
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)]
Solution 10
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5)]
Solution 11
[(0,2),(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,4),(2,5),(3,4),(3,5)]
Searched finished
Time in propagator: 0.000149
Time in check full graphs: 0.000006
Calls of check: 11
Calls propagator: 155
Number of models: 11
Statistics for MinimalityChecker:
    Calls: 37
    Time in seconds: 0.0006
    Added clauses: 26
Total time: 0.005533

However, sometimes I'm more interested in what the resulting graphs are. Indeed, I can write a script to select as follows. But I would like to ask if there are any built-in options.

python ./graph_builder.py -v 6    --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 > temp_output.txt
# Set a flag to indicate whether "Solution" is found
found_solution=false
# Read the output text line by line
while IFS= read -r line
do
    # If "Solution" is found, set the flag to true
    if [[ $line == *"Solution"* ]]; then
        found_solution=true
    # If the flag is true, print the current line and reset the flag to false
    elif [ "$found_solution" = true ]; then
        echo "$line"
        found_solution=false
    fi
done < temp_output.txt

# Delete the temporary file
rm temp_output.txt

Output:

[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)]
[(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)]
[(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5)]

The second thing is that I looked at the previously opened issue, and it seems there was an intention to convert it into the graph6 format (see https://github.com/markirch/sat-modulo-symmetries/issues/6). Has this work been completed? I'm thinking about seamless integration with software like nauty.

Best wishes, Licheng

manfredscheucher commented 1 year ago

If I understand, you only want one graph. So Just omit "--all-graphs"

lichengzhang1 @.***> schrieb am Fr., 6. Okt. 2023, 04:05:

When I run the following command (or similar ones), I get a lot of output.

python ./graph_builder.py -v 6 --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 >output.txt

Arguments: Namespace(vertices=6, cnf_file=None, directed=False, multigraph=None, underlying_graph=False, static_partition=False, counter='sequential', DEBUG=1, all_graphs=True, hide_graphs=False, args_SMS='', num_edges_upp=12, num_edges_low=10, Delta_upp=None, delta_low=None, even_degrees=False, no_subsuming_neighborhoods=False, degree_partition=False, chi_upp=None, chi_low=None, Ck_free=None, mtf=False, girth=None, girth_compact=None, alpha_upp=None, omega_upp=None, ramsey=None, planar_kuratowski=False, connectivity_low=3, diam2_critical=False, forbidden_subgraphs=None, forbidden_induced_subgraphs=None) running the command: time smsg --vertices 6 --print-stats True --frequency 30 --all-graphs --dimacs ./temp97.enc Number of vertices: 6 Initial partition:0 0 0 0 0 0 Clauses: 5841, Variables 1881 SAT Solver: Cadical Start solving Solution 1 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)] Solution 2 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)] Solution 3 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)] Solution 4 [(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)] Solution 5 [(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)] Solution 6 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(3,5),(4,5)] Solution 7 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(4,5)] Solution 8 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,5),(4,5)] Solution 9 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)] Solution 10 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5)] Solution 11 [(0,2),(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,4),(2,5),(3,4),(3,5)] Searched finished Time in propagator: 0.000149 Time in check full graphs: 0.000006 Calls of check: 11 Calls propagator: 155 Number of models: 11 Statistics for MinimalityChecker: Calls: 37 Time in seconds: 0.0006 Added clauses: 26 Total time: 0.005533

However, sometimes I'm more interested in what the resulting graph is.

Indeed, I can write a script to select as follows. But I would like to ask if there are any built-in options.

python ./graph_builder.py -v 6 --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 > temp_output.txt Set a flag to indicate whether "Solution" is found

found_solution=false

Read the output text line by line

while IFS= read -r line do

If "Solution" is found, set the flag to true

if [[ $line == *"Solution"* ]]; then
    found_solution=true
# If the flag is true, print the current line and reset the flag to false
elif [ "$found_solution" = true ]; then
    echo "$line"
    found_solution=false
fi

done < temp_output.txt

Delete the temporary file

rm temp_output.txt

The second thing is that I looked at the previously opened issue, and it seems there was an intention to convert it into the graph6 format (see

6 https://github.com/markirch/sat-modulo-symmetries/issues/6). Has

this work been completed? I'm thinking about seamless integration with software like nauty.

— Reply to this email directly, view it on GitHub https://github.com/markirch/sat-modulo-symmetries/issues/22, or unsubscribe https://github.com/notifications/unsubscribe-auth/A6OXSLIQSOEY5RV4WANBSFLX55RPRAVCNFSM6AAAAAA5VD7EPCVHI2DSMVQWIX3LMV43ASLTON2WKOZRHEZDSMZRHA3TONA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

manfredscheucher commented 1 year ago

Currently our python program just calls the smsg, so the graphs are not parsed in python. It is of course possible to parse the smsg output, but we are planning to make this interface nicer since there is a nice python-C++ interface. If you just want to convert and investigate one or a few graph, you can use sagemath or python+networks to convert an edge list as it is printed by smsg to graph6. If you are not yet familiar with sagemath I highly recommend you to have a look at sagemath since it is very user-friendly computer algebra system, providing easy to use functionality for most areas of mathematics plus tons of documentation. E.g. you can run both, G=Graph([(1,2),(2,3)]) and G=Graph(graph6string) as input. Export with G.edges(labels=False) and G.graph6_string(). https://doc.sagemath.org/html/en/reference/graphs/index.html

Manfred Scheucher @.***> schrieb am Fr., 6. Okt. 2023, 08:21:

If I understand, you only want one graph. So Just omit "--all-graphs"

lichengzhang1 @.***> schrieb am Fr., 6. Okt. 2023, 04:05:

When I run the following command (or similar ones), I get a lot of output.

python ./graph_builder.py -v 6 --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 >output.txt

Arguments: Namespace(vertices=6, cnf_file=None, directed=False, multigraph=None, underlying_graph=False, static_partition=False, counter='sequential', DEBUG=1, all_graphs=True, hide_graphs=False, args_SMS='', num_edges_upp=12, num_edges_low=10, Delta_upp=None, delta_low=None, even_degrees=False, no_subsuming_neighborhoods=False, degree_partition=False, chi_upp=None, chi_low=None, Ck_free=None, mtf=False, girth=None, girth_compact=None, alpha_upp=None, omega_upp=None, ramsey=None, planar_kuratowski=False, connectivity_low=3, diam2_critical=False, forbidden_subgraphs=None, forbidden_induced_subgraphs=None) running the command: time smsg --vertices 6 --print-stats True --frequency 30 --all-graphs --dimacs ./temp97.enc Number of vertices: 6 Initial partition:0 0 0 0 0 0 Clauses: 5841, Variables 1881 SAT Solver: Cadical Start solving Solution 1 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)] Solution 2 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)] Solution 3 [(0,3),(0,4),(0,5),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)] Solution 4 [(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,5),(4,5)] Solution 5 [(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(4,5)] Solution 6 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(3,5),(4,5)] Solution 7 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,4),(4,5)] Solution 8 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,5),(3,5),(4,5)] Solution 9 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5),(4,5)] Solution 10 [(0,3),(0,4),(0,5),(1,2),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5)] Solution 11 [(0,2),(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,4),(2,5),(3,4),(3,5)] Searched finished Time in propagator: 0.000149 Time in check full graphs: 0.000006 Calls of check: 11 Calls propagator: 155 Number of models: 11 Statistics for MinimalityChecker: Calls: 37 Time in seconds: 0.0006 Added clauses: 26 Total time: 0.005533

However, sometimes I'm more interested in what the resulting graph is.

Indeed, I can write a script to select as follows. But I would like to ask if there are any built-in options.

python ./graph_builder.py -v 6 --num-edges-low 10 --num-edges-upp 12 --all-graphs --connectivity-low 3 > temp_output.txt Set a flag to indicate whether "Solution" is found

found_solution=false

Read the output text line by line

while IFS= read -r line do

If "Solution" is found, set the flag to true

if [[ $line == *"Solution"* ]]; then
    found_solution=true
# If the flag is true, print the current line and reset the flag to false
elif [ "$found_solution" = true ]; then
    echo "$line"
    found_solution=false
fi

done < temp_output.txt

Delete the temporary file

rm temp_output.txt

The second thing is that I looked at the previously opened issue, and it seems there was an intention to convert it into the graph6 format (see

6 https://github.com/markirch/sat-modulo-symmetries/issues/6). Has

this work been completed? I'm thinking about seamless integration with software like nauty.

— Reply to this email directly, view it on GitHub https://github.com/markirch/sat-modulo-symmetries/issues/22, or unsubscribe https://github.com/notifications/unsubscribe-auth/A6OXSLIQSOEY5RV4WANBSFLX55RPRAVCNFSM6AAAAAA5VD7EPCVHI2DSMVQWIX3LMV43ASLTON2WKOZRHEZDSMZRHA3TONA . You are receiving this because you are subscribed to this thread.Message ID: @.***>

lichengzhang1 commented 1 year ago

@manfredscheucher I don't just want one graph; I want all of them. I updated my question. It feels like these graphs could be output more concisely from the solver's settings. Thank you, I'm familiar with SageMath or networkx, and indeed, it can be achieved by writing some scripts.

manfredscheucher commented 1 year ago

(sorry I started writing this before your post appeared, I will leave it in case someone else is interested) here is a short example, which i ran in the commandline, but you may also use the notebook option in the browser:

manfred@mscheuch:~$ sage
┌────────────────────────────────────────────────────────────────────┐
│ SageMath version 9.8, Release Date: 2023-02-11                     │
│ Using Python 3.11.5. Type "help()" for help.                       │
└────────────────────────────────────────────────────────────────────┘
sage: graphs.PetersenGraph().plot()
Launched png viewer for Graphics object consisting of 26 graphics primitives
sage: for G in graphs.nauty_geng("4 -c"):
....:     print(G.edges(labels=0),G.graph6_string())
....:     
<ipython-input-2-6738621c58e4>:2: DeprecationWarning: parameter 'sort' will be set to False by default in the future
See https://trac.sagemath.org/27408 for details.
  print(G.edges(labels=Integer(0)),G.graph6_string())
[(0, 3), (1, 3), (2, 3)] CF
[(0, 2), (0, 3), (1, 3)] CU
[(0, 2), (0, 3), (1, 3), (2, 3)] CV
[(0, 2), (0, 3), (1, 2), (1, 3)] C]
[(0, 2), (0, 3), (1, 2), (1, 3), (2, 3)] C^
[(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)] C~
sage: G = graphs.CompleteGraph(5)

moreover, besides the web-documentation, there is also a PDF with hundrets of pages, or you can simply type "G." and hit tabulator, then it provides all possible features:

sage: G.   <<tabulator pressed here>>
  G.add_clique                            G.all_cliques                           G.antisymmetric                          
  G.add_cycle                             G.all_paths                             G.apex_vertices                          
  G.add_edge                              G.allow_loops                           G.arboricity                             
  G.add_edges                             G.allow_multiple_edges                  G.atoms_and_clique_separators            
  G.add_path                              G.allows_loops                          G.automorphism_group                    >
  G.add_vertex                            G.allows_multiple_edges                 G.average_degree                         
  G.add_vertices                          G.am                                    G.average_distance                       
  G.adjacency_matrix                      G.antipodal_graph                       G.bipartite_color  

To see documentation (the same as on the website) for one functionality type "G.is_planar?"

manfredscheucher commented 1 year ago

@lichengzhang1 I now implemented what I wrote above (parsing the C++ output in python) as parameter --graph-format graph6 so that the python layer now supports output in graph6 format. you may now use --DEBUG 0 to only print the graph strings to stdout

lichengzhang1 commented 1 year ago

Great job! I just try, but I feel that the speed has been significantly slowed down. Perhaps there's room for improvement.

manfredscheucher commented 1 year ago

yes i also noticed that slow-down. firstly, the string-parsing in python is slow and secondly i currently use the network.to_graph6_bytes in the python layer to compute the graph6 string. I am sure there are more efficient implementations available in C, so it would be more efficient to pass the "--graph-format" to smsg so that this is done in C. another good reason to refactor the python-C interface