### Build and Install SMS from Source

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

This script compiles and installs the SAT Modulo Symmetries framework. It requires execute permissions and will prompt for administrative privileges for system-wide installation. Use the -l flag for local installation without root.

```bash
chmod +x build-and-install.sh
./build-and-install.sh
```

--------------------------------

### Executable Definition and Installation

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/src/CMakeLists.txt

Defines the main executable 'smsg' and links it against the static 'sms' library. It also specifies installation rules for the executable, shared library, static library, and header files.

```cmake
# targets must be added *after* all calls to link_libraries()
add_executable(smsg "main.cpp")
target_link_libraries(smsg PRIVATE sms_static)

install(TARGETS
	smsg
	sms
	sms_static
)
install(FILES ${CADICAL_LIBRARY} DESTINATION lib RENAME libsmscadical.a)
install(FILES "sms.hpp" "cadical.hpp" "useful.h" "graphChecker.hpp" "minimalityCheck.hpp" DESTINATION include/sms)
```

--------------------------------

### Example: Generate all graphs on 7 vertices

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Demonstrates how to use the `smsg` command to generate all possible graphs on 7 vertices, irrespective of isomorphism.

```bash
smsg -v 7 --all-graphs
```

--------------------------------

### CMakeLists.txt Project Setup and Configuration

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/CMakeLists.txt

This CMakeLists.txt file sets up the C++ project, defining the minimum required CMake version and project details. It configures C++ standards to C++20, manages the build type, and conditionally links external libraries such as Boost and the Glasgow Subgraph Solver based on the GLASGOW variable. It also includes subdirectories for source code modules.

```CMake
cmake_minimum_required(VERSION 3.12)

project(SMS VERSION "1.0" LANGUAGES C CXX)

# set(CMAKE_EXE_LINKER_FLAGS "-static")
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
list(APPEND CMAKE_MODULE_PATH "${PROJECT_SOURCE_DIR}/cmake")

if (CMAKE_BUILD_TYPE)
  message("Build type set to ${CMAKE_BUILD_TYPE}.")
else()
  set(CMAKE_BUILD_TYPE Release)
endif ()


# find_package(Z3 4.12.0 REQUIRED)

if (DEFINED GLASGOW)
	set(CMAKE_CXX_STANDARD 20)
	add_compile_definitions(GLASGOW)
	include_directories(glasgow-subgraph-solver)
	#link_libraries("${PROJECT_SOURCE_DIR}/glasgow-subgraph-solver/libcommon.a")
	link_libraries("${PROJECT_SOURCE_DIR}/glasgow-subgraph-solver/build/gss/libglasgow_subgraphs.a")
	link_libraries("pthread")
	link_libraries("stdc++fs")
	find_package(Boost REQUIRED COMPONENTS container thread iostreams)
	include_directories(${Boost_INCLUDE_DIRS})
	link_libraries(${Boost_LIBRARIES})
	# link_libraries("boost_container")
	# link_libraries("boost_thread")
	# link_libraries("boost_iostreams")
	message("-- Linking with the Glasgow Subgraph Solver")
	unset(GLASGOW) # to suppress the warning about an unused variable in src/CMakeLists.txt
else ()
	message("-- Building without the Glasgow Subgraph Solver")
endif()

add_subdirectory(src)
# add_subdirectory(src_directed)
# add_subdirectory(src_hypher_graph)
# add_subdirectory(src_hypher_graph_incidence)

# -DZ3_INCLUDE_DIR=[path][/src/api
# -DZ3_LIBRARIES=[path]/debug/libz3.so

# cmake . -B./build -DZ3_INCLUDE_DIR=./z3-master/src/api -DZ3_LIBRARIES=./z3-master/build/libz3.so

```

--------------------------------

### Example: Generate non-bipartite graphs with chromatic number >= 3

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Shows how to generate graphs on 7 vertices that are non-bipartite (chromatic number at least 3) and display detailed timing statistics for minimality checks and coloring propagators.

```bash
smsg -v 7 --all-graphs --min-chromatic-number 3
```

--------------------------------

### Troubleshoot PySMS Installation

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

If the installation of the Python SMS library (PySMS) fails, this command can help by updating the pip package installer to its latest version. This often resolves dependency or compatibility issues.

```bash
python3 -m pip install --update pip
```

--------------------------------

### Test biplanarity of C5[4,4,4,4,3]

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Tests if the graph C5[4,4,4,4,3] is biplanar using the planarity encoding script. This command is a specific test case for the Earth-Moon problem setup.

```bash
python ./encodings/planarity.py -v 19 --directed --earthmoon_candidate1
```

--------------------------------

### Forbidden Subgraph File Format Example (Plaintext)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/advanced.md

Provides an example of the file format used to specify forbidden subgraphs for the SMS solver. Each line defines a graph with vertices and edges, enabling the generation of graphs that exclude these patterns.

```Plaintext
3 0 1 1 2 0 2
3 0 1 1 2 2 3 0 3
```

--------------------------------

### Z3 Integration (Commented Out)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/src/CMakeLists.txt

Contains commented-out CMake commands demonstrating how to integrate the Z3 solver, including setting include directories, linking libraries, and adding compile options for a target named 'graphgen'.

```cmake
# commands for adding Z3
# target_include_directories(graphgen PRIVATE ${Z3_CXX_INCLUDE_DIRS})
# target_link_libraries(graphgen PRIVATE ${Z3_LIBRARIES})
# target_compile_options(graphgen PRIVATE ${Z3_COMPONENT_CXX_FLAGS})

# target_include_directories(graphgendirected PRIVATE ${Z3_CXX_INCLUDE_DIRS})
# target_link_libraries(graphgendirected PRIVATE ${Z3_LIBRARIES})
# target_compile_options(graphgendirected PRIVATE ${Z3_COMPONENT_CXX_FLAGS})

# add_executable(graphgenBoth "main.cpp" "minimalityCheck.cpp"  "solveCadical.cpp" "useful.cpp" "arguments.cpp" "path.cpp" "connectedComponents.cpp" "coloring.cpp" "solveGeneral.cpp")
# target_link_libraries(graphgenBoth PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/../cadical-internal-theory-propagation/build/libcadical.a")
# target_compile_options(graphgenBoth PRIVATE "-Wall" "-Wextra" "-pedantic" "-O3")
```

--------------------------------

### Project Configuration and Dependencies

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/src/CMakeLists.txt

Configures the build environment, sets compiler flags, and finds necessary external libraries such as Boost, CaDiCaL, and Clingo. It includes conditional compilation based on the GLASGOW flag and handles cross-platform compiler warnings.

```cmake
set(Boost_USE_STATIC_LIBS OFF)

# set(Boost_USE_MULTITHREADED ON)
# set(Boost_USE_STATIC_RUNTIME OFF)
find_package(Boost 1.74.0 REQUIRED COMPONENTS program_options graph)
include_directories(${Boost_INCLUDE_DIRS})
link_libraries(${Boost_LIBRARIES})

# cross-platform way to elevate the warning level
# -O3 not needed, because it is implied by CMAKE_BUILD_TYPE=Release (which is the default)
if (MSVC)
    # warning level 4
    add_compile_options(/W4)
else()
    # additional warnings
    add_compile_options(-Wall -Wextra -Wpedantic)
endif()

if (DEFINED CLINGO)
	find_package(Clingo)
	if (Clingo_FOUND) # only build with Clingo if the library was explicitly requested and is available
		list(APPEND sources "${clingo_wrapper}")
		add_compile_definitions(INCLUDE_CLINGO)
		link_libraries(libclingo)
		message("Linking with Clingo")
	else()
		message("Could not find Clingo, continuing without it")
	endif()
endif()
```

--------------------------------

### Generate Kochen-Specker Graphs (22 vertices) with Cubing Args

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates Kochen-Specker candidate graphs with 22 vertices, including specific arguments for cubing. It sets a prerun time cutoff and a minimum edge variable assignment cutoff for cube generation, passed via `--args-SMS`.

```bash
python ./encodings/kochen_specker.py -v 22 --all-graphs --args-SMS "--assignment-cutoff-prerun-time 5 --assignment-cutoff 110"
```

--------------------------------

### BibTeX Entry: Searching for Smallest Universal Graphs and Tournaments with SAT

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'Searching for Smallest Universal Graphs and Tournaments with SAT' by Zhang and Szeider, presented at CP 2023.

```bibtex
@inproceedings{ZhangS23,
  author       = {Tianwei Zhang and
                  Stefan Szeider},
  title        = {Searching for Smallest Universal Graphs and Tournaments with {SAT}},
  booktitle    = {29th International Conference on Principles and Practice of Constraint
                  Programming, {CP} 2023, August 27-31, 2023, Toronto, Canada},
  series       = {LIPIcs},
  volume       = {280},
  pages        = {39:1--39:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  doi          = {10.4230/LIPICS.CP.2023.39},
}
```

--------------------------------

### Project Dependencies

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/requirements.txt

This snippet details the Python packages and their versions required for the project, as specified by pip-compile. It includes package names, version specifiers, and comments indicating their usage or origin.

```pip-compile
click==8.1.3
    # via mkdocs
```

```pip-compile
colorama==0.4.6
    # via griffe
```

```pip-compile
ghp-import==2.1.0
    # via mkdocs
```

```pip-compile
griffe==0.29.0
    # via mkdocstrings-python
```

```pip-compile
importlib-metadata==6.6.0
    # via
    #   markdown
    #   mkdocs
    #   mkdocstrings
```

```pip-compile
jinja2==3.1.2
    # via
    #   mkdocs
    #   mkdocstrings
```

```pip-compile
markdown==3.3.7
    # via
    #   markdown-include
    #   mkdocs
    #   mkdocs-autorefs
    #   mkdocstrings
    #   pymdown-extensions
```

```pip-compile
markdown-include==0.8.1
    # via -r docs/requirements.in
```

```pip-compile
markupsafe==2.1.3
    # via
    #   jinja2
    #   mkdocstrings
```

```pip-compile
mergedeep==1.3.4
    # via mkdocs
```

```pip-compile
mkdocs==1.4.3
    # via
    #   -r docs/requirements.in
    #   mkdocs-autorefs
    #   mkdocstrings
```

```pip-compile
mkdocs-autorefs==0.4.1
    # via mkdocstrings
```

```pip-compile
mkdocstrings[python]==0.22.0
    # via
    #   -r docs/requirements.in
    #   mkdocstrings-python
```

```pip-compile
mkdocstrings-python==1.1.2
    # via mkdocstrings
```

```pip-compile
packaging==23.1
    # via mkdocs
```

```pip-compile
pymdown-extensions==10.0.1
    # via mkdocstrings
```

```pip-compile
python-dateutil==2.8.2
    # via ghp-import
```

```pip-compile
pyyaml==6.0
    # via
    #   mkdocs
    #   pymdown-extensions
    #   pyyaml-env-tag
```

```pip-compile
pyyaml-env-tag==0.1
    # via mkdocs
```

```pip-compile
six==1.16.0
    # via python-dateutil
```

```pip-compile
typing-extensions==4.6.3
    # via mkdocstrings
```

```pip-compile
watchdog==3.0.0
    # via mkdocs
```

```pip-compile
zipp==3.15.0
    # via importlib-metadata
```

--------------------------------

### BibTeX Entry: Computing small Rainbow Cycle Numbers with SAT modulo Symmetries

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'Computing small Rainbow Cycle Numbers with SAT modulo Symmetries' by Kirchweger and Szeider, presented at CP 2024.

```bibtex
@InProceedings{KirchwegerSzeider24,
	author       = {Markus Kirchweger and Stefan Szeider},
	title        = {Computing small Rainbow Cycle Numbers with SAT modulo Symmetries},
	booktitle    = {30th International Conference on Principles and Practice of Constraint
                  Programming, {CP} 2024, September 2-6, 2024, Girona, Spain},
	series       = {LIPIcs},
	volume       = {307},
	pages        = {37:1--37:11},
	publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
	year         = {2024},
	doi      = {10.4230/LIPICS.CP.2024.37},
}
```

--------------------------------

### BibTeX Entry: Co-Certificate Learning with SAT Modulo Symmetries

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'Co-Certificate Learning with SAT Modulo Symmetries' by Kirchweger, Peitl, and Szeider, presented at IJCAI 2023.

```bibtex
@inproceedings{KirchwegerPeitlSzeider23,
	title = {Co-Certificate Learning with {SAT} Modulo Symmetries},
	author= {Kirchweger, Markus and Peitl, Tom{\'a}s and Szeider, Stefan},
	year  = {2023},
	booktitle = {Proceedings of the 34th International Joint Conference on Artificial Intelligence, IJCAI 2023},
	publisher = {AAAI Press/IJCAI},
	doi = {10.24963/IJCAI.2023/216},
}
```

--------------------------------

### Generate Triangle-Free Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Commands to generate QCIR encodings for triangle-free graphs with specified chromatic numbers (chi-low). These commands utilize the pysms.qcir_graph_builder module to create graph instances for QBF solvers.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --chi-low 4 --Ck-free 3 --no-subsuming-neighborhoods --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --chi-low 5 --mtf --no-subsuming-neighborhoods --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### Generate Planar Graphs (Universal Set Encoding)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates planar graphs using a universal set-based encoding. This command employs the `planarity.py` script to construct graph representations for planarity analysis.

```bash
python ./encodings/planarity.py -v $n --all-graphs --planar_universal
```

--------------------------------

### Clone SAT Modulo Symmetries Repository

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

This command clones the main project repository for SAT Modulo Symmetries from GitHub. It is the initial step to obtain the source code for building the framework.

```bash
git clone https://github.com/markirch/sat-modulo-symmetries
cd sat-modulo-symmetries
```

--------------------------------

### BibTeX Entry: SAT-Based Generation of Planar Graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'SAT-Based Generation of Planar Graphs' by Kirchweger, Scheucher, and Szeider, presented at SAT 2023.

```bibtex
@InProceedings{KirchwegerScheucherSzeider23,
	author       = {Markus Kirchweger and Manfred Scheucher and Stefan Szeider},
	title        = {{SAT}-Based Generation of Planar Graphs},
	booktitle = {The 26th International Conference on Theory and
	Applications of Satisfiability Testing (SAT 2023),
	July 04-08, 2023, Alghero, Italy},
	year      = {2023},
	editor    = {Meena Mahajan and Friedrich Slivovsky},
	series    = {LIPIcs},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
	doi          = {10.4230/LIPICS.SAT.2023.14},
}
```

--------------------------------

### PySMS Graph Builder Command Line Usage

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Demonstrates how to use the PySMS graph_builder module from the command line to generate graphs with specific properties. It shows common options for defining graph characteristics and controlling the solving process.

```bash
python -m pysms.graph_builder --vertices 6 --delta-low 3 --num-edges-upp 10 --all-graphs
```

```bash
python -m pysms.graph_builder --help
```

```bash
smsg --help
```

--------------------------------

### Generate Domination Conjecture Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Commands to generate QCIR encodings related to the domination conjecture in cubic and general graphs. These use the pysms.qcir_graph_builder module with parameters like --domination-conjecture, --connected-static, --bipartite, and --min-girth-compact.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --domination-conjecture --connected-static --print-qcir "$QCIR_OUTPUT_FILE"
```

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --domination-conjecture --bipartite --print-qcir "$QCIR_OUTPUT_FILE"
```

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --min-girth-compact 6 --domination-conjecture --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### Generate k-connected n-vertex graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates k-connected graphs with n vertices. This command is used to explore OEIS sequences related to graph connectivity.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --connectivity-low $k
```

--------------------------------

### Generate Kochen-Specker Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Command to generate QCIR encodings for Kochen-Specker graphs. This utilizes the pysms.qcir_graph_builder module to produce graphs with the Kochen-Specker property, suitable for QBF analysis.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --kochen-specker --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### Source File Collection and Library Definitions

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/src/CMakeLists.txt

Collects C++ source files, including dynamically found graph propagators, and defines shared and static libraries named 'sms'. It also imports and links the CaDiCaL library.

```cmake
set(sources "minimalityCheckCommon.cpp" "sms.cpp" "graph.cpp" "useful.cpp" "options.cpp" "minimalityCheck.cpp" "minimalityCheck_dir.cpp" "cubing.cpp" "qbf/universal.cpp" "qbf/universal2.cpp" "qbf/qcirParser.cpp" )
if(GLASGOW)
	list(APPEND sources "other/forbiddenSubgraph.cpp")
endif()

# append graph propagators
file(GLOB prop_resources "graphPropagators/*.cpp")
message("Graph propagators: ${prop_resources}")

list(APPEND sources ${prop_resources})


set(glasgow_wrapper "glasgow_wrapper.cpp")

find_library(CADICAL_LIBRARY
NAMES cadical
HINTS "${CMAKE_CURRENT_SOURCE_DIR}/../cadical_sms/build/"
)
if (NOT CADICAL_LIBRARY)
	message(FATAL_ERROR "CaDiCaL not found (")
else()
	message("CaDiCaL found at ${CADICAL_LIBRARY}")
endif()
add_library(cadical STATIC IMPORTED GLOBAL)
set_target_properties(cadical PROPERTIES IMPORTED_LOCATION ${CADICAL_LIBRARY})
link_libraries(cadical)


#set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "time")

add_library(sms SHARED ${sources})
add_library(sms_static STATIC ${sources})

set_target_properties(sms_static PROPERTIES OUTPUT_NAME sms)
```

--------------------------------

### Generate Treewidth Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Commands to generate QCIR encodings for graphs with specific treewidth constraints. These commands use the pysms.qcir_graph_builder module to create graphs with low treewidth, specified by versioned parameters.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --tree-width-low-version2 4 --tree-width-upp-version1 4 --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --tree-width-low-version2 5 --tree-width-upp-version1 5 --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### BibTeX Entry: SAT Modulo Symmetries for Graph Generation

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'SAT Modulo Symmetries for Graph Generation and Enumeration' by Markus Kirchweger and Stefan Szeider, published in ACM Transactions on Computational Logic in 2024.

```bibtex
@article{KirchwegerS24,
  author    = {Markus Kirchweger and
               Stefan Szeider},
  title = {SAT Modulo Symmetries for Graph Generation and Enumeration},
  year = {2024},
  journal   = {{ACM} Trans. Comput. Log.},
  publisher = {Association for Computing Machinery},
  volume = {25},
  number = {3},
  issn = {1529-3785},
  doi = {10.1145/3670405},
}
```

--------------------------------

### Generate Folkman Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Commands to generate QCIR encodings for Folkman graphs of specified sizes (k=4 and k=5). These commands leverage the pysms.qcir_graph_builder module for creating these particular graph properties.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --folkmann 4 --no-subsuming-neighborhoods --print-qcir "$QCIR_OUTPUT_FILE"
```

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --folkmann 5 --no-subsuming-neighborhoods --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### Generate Kochen-Specker Graphs (19 vertices)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates Kochen-Specker candidate graphs with 19 vertices using the `kochen_specker.py` script. This command is used to reproduce results from a specific paper on co-certificate learning with SAT modulo symmetries.

```bash
python ./encodings/kochen_specker.py -v 19 --all-graphs
```

--------------------------------

### Generate k-connected n-vertex planar graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates k-connected planar graphs with n vertices. This command is used for OEIS sequences focusing on planar graph properties.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --connectivity-low $k --planar
```

--------------------------------

### Generate k-connected directed n-vertex planar graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates k-connected directed planar graphs with n vertices, focusing on the underlying graph. Essential for certain OEIS sequence investigations.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --connectivity-low $k --planar --directed --underlying-graph
```

--------------------------------

### Generate Planar Graphs (Schnyder Order Encoding)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates planar graphs using a Schnyder order-based encoding. This command utilizes the `planarity.py` script to create graph encodings for planarity testing.

```bash
python ./encodings/planarity.py -v $n --all-graphs --planar_schnyder
```

--------------------------------

### Generate 2-connected 3-regular n-vertex planar graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates 2-connected, 3-regular planar graphs with n vertices. This command is used for OEIS sequences like A58378.

```bash
python ./pysms/graph_builder.py -v $((2*$n)) --all-graphs --planar --delta-low 3 --Delta-upp 3 --connectivity-low 2
```

--------------------------------

### Generate k-connected n-vertex triangulations

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates k-connected triangulations with n vertices. This command is specific to OEIS sequences involving triangulated planar graphs.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --connectivity-low $k --planar --num-edges-low $((3*$n-6))
```

--------------------------------

### smsg/smsd Command-Line Arguments

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Details the primary command-line arguments for the smsg and smsd SAT solvers. These arguments control graph properties, search behavior, parallelization, and input/output formats.

```APIDOC
smsg/smsd Command-Line Arguments:

-v VERTICES
  - Number of vertices (order) of the graph.

-b n m
  - Searches for a bipartite graph with n+m vertices.
  - Partitions are {0, ..., n-1} and {n, ..., n+m-1}.

--all-graphs
  - Computes all graphs instead of stopping at the first solution.

--cutoff CUTOFF
  - Limits the number of recursive calls in the minimality check.
  - Helps avoid exponential behavior but may render symmetry breaking incomplete.

--frequency FREQUENCY
  - Balances time spent in minimality check and the solver.
  - If frequency is 5, minimality check is called every 5th time on average.

--dimacs FILE
  - Specifies the file name providing the SAT encoding in DIMACS format.

--print-stats
  - Prints statistics of the run at the end, including time spent in propagators.

--simple-assignment-cutoff ACUTOFF
  - Cubing parameter for parallelization.
  - If at least ACUTOFF edge variables are assigned and propagate is called, a cube is generated.

--assignment-cutoff ACUTOFF
  - Uses lookahead for picking branching variables during the cubing phase.

--prerun TIME
  - Runs the solver for TIME seconds before starting cubing (applying assignment cutoff).

--cube-file FILE
  - Loads cubes from FILE for the second phase of cube-and-conquer.

--cube-line LINENR
  - Solves the cube specified by line number LINENR from the cube file.
  - Line numbers start with 1.

For a complete list, call `smsg --help`.
```

--------------------------------

### Update Git Submodules for SMS

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

After cloning the repository, this command initializes and updates all necessary Git submodules, which include dependencies like the CaDiCaL SAT solver. This ensures all required components are present.

```bash
git submodule update --init --recursive
```

--------------------------------

### Solve Kochen-Specker Problem with Cubes

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Solves the Kochen-Specker problem for 22 vertices using pre-generated cubes from a specified file. It indicates the cubes to be used and the range of cube IDs to solve, passed as arguments to the SAT Modulo Symmetries solver.

```bash
python ./encodings/kochen_specker.py -v 22 --all-graphs --args-SMS " --cubes cubeFile --cube2solve 2390 2392 "
```

--------------------------------

### Generate k-connected directed n-vertex graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates k-connected directed graphs with n vertices, considering their underlying undirected graph structure. Used for specific OEIS sequences.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --connectivity-low $k --directed --underlying-graph
```

--------------------------------

### BibTeX Entry: Small Unsatisfiable k-CNFs with Bounded Literal Occurrence

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/publications.md

BibTeX entry for the publication 'Small Unsatisfiable k-CNFs with Bounded Literal Occurrence' by Zhang, Peitl, and Szeider, presented at SAT 2024.

```bibtex
@inproceedings{ZhangPS24,
  author       = {Tianwei Zhang and
                  Tom{\'a}s Peitl and
                  Stefan Szeider},
  title        = {Small Unsatisfiable k-CNFs with Bounded Literal Occurrence},
  booktitle    = {27th International Conference on Theory and Applications of Satisfiability
                  Testing, {SAT} 2024, August 21-24, 2024, Pune, India},
  series       = {LIPIcs},
  volume       = {305},
  pages        = {31:1--31:22},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2024},
  doi          = {10.4230/LIPICS.SAT.2024.31},
}
```

--------------------------------

### Generate Planar Graphs (Kuratowski Encoding)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates planar graphs using a Kuratowski-based encoding. Planarity is not part of the encoding itself but is forwarded to the SMS solver and checked with a frequency of 1/5.

```bash
python -m pysms.graph_builder.py -v $n --all-graphs --planar
```

--------------------------------

### Generate connected triangle-free 3-regular 2n-vertex planar graphs

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates connected, triangle-free, 3-regular planar graphs with 2n vertices. This command is specific for OEIS sequences like A255600.

```bash
python ./pysms/graph_builder.py -v $((2*$n)) --all-graphs --connectivity-low 1 --planar --Ck-free 3 --delta-low 3 --Delta-upp 3
```

--------------------------------

### Generate connected n-vertex planar graphs with even degrees

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates connected planar graphs with n vertices and even degrees. This command targets OEIS sequences requiring both connectivity and even degree properties.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --planar --even-degrees --connectivity-low 1
```

--------------------------------

### Compute rainbow cycle number with permutation restriction

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Computes an encoding for the rainbow cycle number problem, restricting the search to permutations. This is an advanced option for the efx.py script.

```bash
python ./encodings/efx.py --directed --partition-size 3 -v 12 --permutation
```

--------------------------------

### Generate Snark Graph Encodings (PySMS)

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Command to generate QCIR encodings for snarks, specifically graphs that are non-3-edge-colorable and cubic. This uses the pysms.qcir_graph_builder module to create these specific graph structures.

```bash
python3 -m pysms.qcir_graph_builder -v "$VERTICES" --cubic --non-3-edge-colorable --Ck-free 3 --Ck-free 4 --two-connected --all-graphs --print-qcir "$QCIR_OUTPUT_FILE"
```

--------------------------------

### Compute rainbow cycle number with propagator

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Computes an encoding for the rainbow cycle number problem using a propagator for absence of rainbow cycles, instead of static encoding. This is an advanced option for the efx.py script.

```bash
python ./encodings/efx.py --directed --partition-size 3 -v 12 --efx-propagator
```

--------------------------------

### Generate n-vertex planar graphs with minimum degree at least k

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates planar graphs with n vertices where the minimum degree is at least k. This is for OEIS sequences related to minimum degree constraints.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --planar --delta-low $k
```

--------------------------------

### PySMS Graph Builder Options

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Details the primary command-line options available for the pysms.graph_builder module, used for specifying graph properties and controlling the generation and solving process. These options define search parameters and output formats.

```APIDOC
PySMS Graph Builder Options:

Core Search Parameters:
  -v, --vertices n
    Description: Search for graphs with exactly 'n' vertices.
    Type: Integer

  -a, --all-graphs
    Description: Enumerate all graphs up to isomorphism satisfying the constraints. If omitted, the program terminates after finding the first graph.
    Type: Flag

Control Flow:
  --no-solve
    Description: Do not solve the constraints; only output the constraints in DIMACS format. Useful for saving constraints for later processing.
    Type: Flag

Graph Properties:
  ->, --directed
    Description: Generate directed graphs. The default is undirected graphs.
    Type: Flag

Bounds:
  -E, --num-edges-upp n
    Description: Set an upper bound on the number of edges in the generated graphs.
    Type: Integer

  -e, --num-edges-low n
    Description: Set a lower bound on the number of edges in the generated graphs.
    Type: Integer

  -D, --Delta-upp n
    Description: Set an upper bound on the maximum degree (Delta) of the generated graphs.
    Type: Integer

  -d, --delta-low n
    Description: Set a lower bound on the minimum degree (delta) of the generated graphs.
    Type: Integer

Output Formatting:
  --graph-format graph6
    Description: Output results in the graph6 format, commonly used by tools like Nauty. Note: This can significantly slow down computation.
    Type: String (specific value: 'graph6')

Argument Forwarding:
  Any unrecognized arguments are forwarded to the 'smsg' solver when in solving mode.
  The legacy `--args-SMS` option for forwarding arguments is deprecated.

Minimality Check (Tip):
  --cutoff n
    Description: Sets a time limit (cutoff) for the minimality check procedure, which filters out non-canonical isomorphic copies. This limits recursive calls and can prevent getting stuck in hard corner cases, but may result in incomplete symmetry breaking.
    Type: Integer (e.g., 20000)
    Example Usage: --cutoff 20000
```

--------------------------------

### Troubleshoot 'Illegal instruction' Error

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

This snippet addresses the 'Illegal instruction' error that may occur when running SMS built with the Glasgow Subgraph Solver on a different machine. It involves modifying CMakeLists.txt to remove architecture-specific flags and rebuilding.

```bash
# Comment out lines related to -march=native in glasgow-subgraph-solver/CMakeLists.txt
# Delete glasgow-subgraph-solver/build directory
# Re-run ./build-and-install.sh -s
```

--------------------------------

### Create Basic Graph Constraints with PySMS

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/index.md

Demonstrates creating a graph encoding with 7 vertices and a maximum degree of 3 using PySMS's GraphEncodingBuilder. It initializes the builder with graph properties and applies a built-in constraint for maximum degree.

```python
from pysms.graph_builder import GraphEncodingBuilder
builder = GraphEncodingBuilder(7, directed=False)
builder.maxDegree(3)
builder.solve(allGraphs=True)
```

--------------------------------

### Compute rainbow cycle number encoding

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Computes an encoding for the rainbow cycle number problem, specifying partition size and number of vertices. This script aims to find graphs without a rainbow cycle.

```bash
python ./encodings/efx.py --directed --partition-size 3 -v 12
```

--------------------------------

### Compute rainbow cycle number with invariant pruning

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Computes an encoding for the rainbow cycle number problem with invariant pruning, setting maximum outdegree and fixing the first vertex. This is for advanced search optimization.

```bash
python ./encodings/efx.py --directed --partition-size 3 -v 12 --delta-high-directed 6 --fix-first-vertex
```

--------------------------------

### Generate n-vertex planar graphs with even degrees

Source: https://github.com/markirch/sat-modulo-symmetries/blob/main/docs/applications.md

Generates planar graphs with n vertices where all degrees are even. Used for OEIS sequences related to Eulerian properties in planar graphs.

```bash
python ./pysms/graph_builder.py -v $n --all-graphs --planar --even-degrees
```