autoguess

Autoguess

Autoguess is a generic, easy-to-use tool for solving guess-and-determine problems. It is especially useful for identifying guess-and-determine attacks and key bridging in cryptanalysis, enabling researchers to find minimal guess bases for a variety of cryptographic primitives. The tool supports multiple solving approaches, including:

• Constraint Programming (CP) via MiniZinc
• Mixed-Integer Linear Programming (MILP) via Gurobi
• Boolean Satisfiability (SAT) via PySAT
• Satisfiability Modulo Theories (SMT) via pySMT
• Algebraic methods via SageMath and Groebner basis computation

---

Overall Structure

The diagram below illustrates the overall structure of Autoguess. Autoguess leverages MiniZinc, PySAT, pySMT, Gurobi, and SageMath (passagemath). Through its Python interface, Autoguess translates guess-and-determine problems into SAT, SMT, MILP, or Groebner basis computations and invokes the appropriate solver. It also offers a lightweight knowledge-propagation mode, which iteratively deduces variables from an initial known set without external solvers. For visualization, Autoguess uses Graphviz to display the determination flow.

---

• Autoguess
  • Overall Structure
  • Installation
    • Prerequisites
    • Installation Methods
      • Method 1: pip install (Recommended)
      • Method 2: Build Docker Image Locally
        • For ARM64 (Apple Silicon)
        • For x86_64 (Most Linux Systems)
      • Method 3: Use Pre-built Docker Image
      • Method 4: Native Installation (Debian-based and macOS)
  • Quick Start
  • Format of Input File
  • Usage
    • Command Line Interface
    • Example 1
    • Example 2
    • Example 3
    • Example 4
    • Example 5
    • Example 6
  • Troubleshooting
    • Common Issues
      • Docker Issues
      • Missing Dependencies
      • Input File Issues
    • Performance Tips
    • Getting Help
  • Applications
    • GD Attack on 1 Round of AES with 1 Known Plaintext/Ciphertext Pair
    • GD Attack on 2 Rounds of AES with 1 Known Plaintext/Ciphertext Pair
    • GD Attack on 3 Rounds of AES with 1 Known Plaintext/Ciphertext Pair
    • GD Attack on 14 Rounds of Khudra with 1 Known Plaintext/Ciphertext Pair
    • GD Attack on 11 Rounds of SKINNY-n-n with 1 Known Plaintext/Ciphertext Pair
    • GD Attack on Enocoro128-v2
    • GD Attack on KCipher2
    • GD Attack on SNOW1
    • GD Attack on SNOW2
    • GD Attack on SNOW3
    • GD Attack on ZUC
    • GD Attack on Bivium-A
    • Key-bridging in Linear Attack on PRESENT
    • Key-bridging in Integral Attack on LBlock
    • Key Bridging in Impossible Differential Attack on LBlock
    • Key Bridging in Zero Correlation Attack on SKINNY-64-128
    • Key Bridging in Zero Correlation Attack on SKINNY-64-192
    • Key Bridging in DS-MITM Attack on SKINNY-128-384
    • Key Bridging in Impossible Differential Attack on T-TWINE-80
    • Key Bridging in Impossible Differential Attack on T-TWINE-128
  • The Paper
    • Citation
  • License

Installation

Prerequisites

Before installing Autoguess, ensure you have the following:

• Python 3.8+: Autoguess requires Python 3.8 or higher (Python 3.11+ needed for Groebner basis support)
• Docker (alternative): For a self-contained installation
• Git: For cloning the repository and dependencies

Installation Methods

Autoguess can be installed via pip (recommended), Docker, or native installer scripts.

Method 1: pip install (Recommended)

The simplest way to install Autoguess is via pip:

# Core installation (SAT solver and visualization)
pip install autoguess

# With SMT solver support (z3, cvc5 -- requires a C++20 compiler for z3)
pip install "autoguess[smt]"

# With CP solver support (also install the MiniZinc binary)
pip install "autoguess[cp]"
autoguess --install-minizinc

# With Groebner basis support (via passagemath, pip-installable SageMath; requires Python >= 3.11)
pip install "autoguess[groebner]"

# With Gurobi MILP support (requires Gurobi license)
pip install "autoguess[gurobi]"

# Everything (SMT + CP + Groebner + Gurobi)
pip install "autoguess[all]"

The following table summarizes the available extras:

Extra	Solvers included	Notes
(core)	SAT (PySAT)	Always installed
[smt]	z3, cvc5	z3-solver builds from source (needs C++20 compiler, e.g. GCC 11+). For boolector, install pyboolector manually (PyPI builds are broken).
[cp]	MiniZinc CP	Also run autoguess --install-minizinc to download the MiniZinc binary
[groebner]	Groebner basis (passagemath)	Requires Python >= 3.11 and native build tools. Falls back to system SageMath if passagemath is not installed.
[gurobi]	Gurobi MILP	Requires a Gurobi license
[all]	All of the above

System dependencies (not installed by pip):

• Python development headers (required for [groebner] / [all]): sudo apt install python3-dev (Debian/Ubuntu) / sudo dnf install python3-devel (Fedora) — needed to build native extensions like cysignals
• MiniZinc binary: Run autoguess --install-minizinc to auto-download, or install via your package manager (brew install minizinc / snap install minizinc --classic)
• Graphviz binary (optional, for visualization rendering): brew install graphviz / apt install graphviz

Method 2: Build Docker Image Locally

The easiest way is using the provided Dockerfile to get Autoguess and all of its dependencies at once. To do so, regardless of what OS you use:

1. Install Docker: Follow the Docker installation guide for your platform

2. Clone this repository:

   git clone https://github.com/hadipourh/autoguess.git
   cd autoguess
   

3. Build the Docker image: Navigate to the directory where you cloned the repository and build a local image of Autoguess:

   docker build --platform linux/amd64 -t autoguess -f docker/DockerfileDebian .
   

4. Run Autoguess: Once built, you can run Autoguess using the following commands:

   For ARM64 (Apple Silicon)

   docker run --platform linux/amd64 -it --rm autoguess
   

   For x86_64 (Most Linux Systems)

   docker run -it --rm autoguess
   

The provided image is self-contained and includes MiniZinc, PySAT, pySMT, and SageMath. While Autoguess also offers a direct Python interface to Gurobi, Gurobi itself and its license are not included in the image. If you wish to use the MILP-based method to solve the guess-and-determine problem, you will need to install Gurobi separately. For Linux and macOS, you can use the installer available in this repository.

One can also build an image of Autoguess with the DockerfileArch which is based on the Arch Linux distribution. To do so, you can use the following command:

docker build -f docker/DockerfileArch -t autoguess_arch .

Then, you can run Autoguess by the following command:

docker run --rm -it autoguess_arch

Method 3: Use Pre-built Docker Image

If you have already installed Docker and prefer to use a pre-built image instead of building locally, you can download a prebuilt image of Autoguess from Docker Hub:

For Debian-based image:

docker pull hoseinhadipour/autoguess

Then run Autoguess:

docker run --rm -it hoseinhadipour/autoguess

For Arch Linux-based image:

docker pull hoseinhadipour/autoguess_arch

Then run Autoguess:

docker run --rm -it hoseinhadipour/autoguess_arch

Method 4: Native Installation (Debian-based and macOS)

For Debian-based Linux operating systems, you can install Autoguess natively using the provided installer script:

git clone https://github.com/hadipourh/autoguess.git
cd autoguess
bash installer.sh

For macOS users, you can also use the installer script, but you will need to install Homebrew first. After installing Homebrew, you can use the provided installer script:

chmod +x installer_macos.sh
./installer_macos.sh

Note: This method requires manually installing all dependencies. Review the requirements.txt file for the complete list of Python dependencies.

---

Quick Start

Once you have Autoguess installed, you can quickly test it with one of the provided examples:

# If installed via pip
autoguess --inputfile ciphers/Example1/relationfile.txt --solver cp --maxsteps 5

# Using Docker (pre-built)
1- docker run --rm -it hoseinhadipour/autoguess
2- python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver cp --maxsteps 5

# Or if you built Docker locally
1- docker run --rm -it autoguess
2- python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver cp --maxsteps 5

# Or if installed natively via scripts
python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver cp --maxsteps 5

This should output something like:

Number of guesses: 2
Number of known variables in the final state: 7 out of 7
The following 2 variable(s) are guessed:
v, u

---

Format of Input File

The input file can be a plain text separated into the following parts:

• Algebraic relations. This section begins with algebraic relations and includes the algebraic relations (currently the algebraic relations over GF(2) are merely supported).
• Connection relations. This section begins with connection relations and includes the connections relations consisting of symmetric or implication relations.
• Known variables. This section begins with known key word under which all known variables are specified.
• Target variables. This section begins with target key word under which all target variables are specified.
• The input file must be ended with a line including the end key word.
• The lines starting with # character are interpreted as comments.

The following example, represents the overall structure of an input file.

# Sample input file
algebraic relations
X1*X4 + X2*X5 + X1 + X3 + X4
X2*X3 + X1*X6 + X3*X4 + X1 
X1*X4 + X1*X5 + X3 + X4 + X6
X5*X6 + X4*X3 + X2
connection relations
X3, X5, X2
X1, X2, X4, X6 => X5
known
X2
target
X1
X3
X4
X5
X6
end

You can find many other input files inside the ciphers folder. Moreover, Autoguess supports system of relations including variables with different weights when the SAT or MILP solvers are used. Example5 and ZUC are two example where the system of relations includes variables with different weights.

---

Usage

Command Line Interface

You can access a brief help for Autoguess by running:

python3 autoguess.py -h

usage: autoguess.py [-h] [-i INPUTFILE] [-o OUTPUTFILE] [-mg MAXGUESS] [-ms MAXSTEPS] [-s {cp,milp,sat,smt,groebner,propagate}] [-milpd {min,max}] [-cps {cp-sat,gecode,chuffed}] [-sats {cadical153,glucose4,minisat22}] [-smts {z3}]
                    [-cpopt {0,1}] [-tl TIMELIMIT] [-tk TIKZ] [-prep PREPROCESS] [-D D] [-tord TERM_ORDERING] [-oln OVERLAPPING_NUMBER] [-cnf2anf {simple,blockwise}]
                    [-dgl {dot,circo,twopi,fdp,neato,nop,nop1,nop2,osage,patchwork,sfdp}] [-log {0,1}] [-kn KNOWN] [-t THREADS] [--nograph] [--findmin] [--reducebasis] [--install-minizinc] [-V]

This tool automates the Guess-and-Determine and Key-Bridging techniques using a variety of CP, MILP, SMT and SAT solvers, as well as the algebraic method based on Groebner basis

options:
  -h, --help            show this help message and exit
  -i, --inputfile INPUTFILE
                        Use an input file in plain text format
  -o, --outputfile OUTPUTFILE
                        Use an output file to write the output into it
  -mg, --maxguess MAXGUESS
                        An upper bound for the number of guessed variables
                        (default: number of target variables)
  -ms, --maxsteps MAXSTEPS
                        An integer number specifying the depth of search
                        (default: number of variables before preprocessing)
  -s, --solver {cp,milp,sat,smt,groebner,propagate}
                        Solver choice
  -milpd, --milpdirection {min,max}
                        MILP direction
  -cps, --cpsolver {cp-sat,gecode,chuffed}
                        CP solver choice
  -sats, --satsolver {cadical153,glucose4,minisat22}
                        SAT solver choice
  -smts, --smtsolver {z3}
                        SMT solver choice
  -cpopt, --cpoptimization {0,1}
                        CP optimization
  -tl, --timelimit TIMELIMIT
                        Time limit for the search in seconds
  -tk, --tikz TIKZ      Generate the tikz code of the determination flow graph
  -prep, --preprocess PREPROCESS
                        Enable the preprocessing phase
  -D, --D D             Degree of Macaulay matrix generated in preprocessing phase
  -tord, --term_ordering TERM_ORDERING
                        Term ordering such as 'degrevlex' or 'deglex'
  -oln, --overlapping_number OVERLAPPING_NUMBER
                        Overlapping number in block-wise CNF to ANF conversion
  -cnf2anf, --cnf_to_anf_conversion {simple,blockwise}
                        CNF to ANF conversion method
  -dgl, --dglayout {dot,circo,twopi,fdp,neato,nop,nop1,nop2,osage,patchwork,sfdp}
                        Layout of determination flow graph
  -log, --log {0,1}     Store intermediate generated files and results
  -kn, --known KNOWN    Comma-separated list of additionally known variables
  -t, --threads THREADS
                        Number of threads for CP/MILP solvers
                        (default: 0 = use all available cores)
  --nograph             Skip generating the determination flow graph (faster)
  --findmin             Iteratively decrease max_guess to find the minimum number of guesses (SAT/SMT only)
  --reducebasis         Reduce a known guess basis via propagation: test subsets of
                        decreasing size (requires -s propagate and -kn)
  --install-minizinc    Download and install MiniZinc binary to ~/.autoguess/minizinc/
  -V, --version         show program's version number and exit

Here we also provide some examples to show how our tool can easily be used to find a minimal guess basis.

Example 1

In this example, given a system of symmetric relations we use Autoguess to find a minimal guess basis. The input file of this example is located in Example1 which includes the following content:

connection relations
x, s, v
x, u, s, y, z
v, u, s
z, s, v, t
u, t, x
end

CP

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver cp --maxsteps 5 --dglayout circo

Terminal output:

Number of guessed variables is set to be at most 7
============================================================
CP SOLVER — Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
============================================================
Variables: 7 | Relations: 5
Max guess: 7 | Max steps: 5
Solver: cp-sat
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
CP model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.29 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (2):
  v
  u
============================================================

Autoguess also generates the following graph visualizing the determination flow:

Groebner

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver groebner

Terminal output:

============================================================
GRÖBNER BASIS SOLVER — Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
============================================================
Variables: 7 | Relations: 5
Term ordering: degrevlex | Overlapping: 2
CNF→ANF method: simple
------------------------------------------------------------
POLYNOMIAL RING CONSTRUCTION
------------------------------------------------------------
Generating Boolean Polynomial Ring in 7 variables ...
Ring constructed in 0.00 seconds
------------------------------------------------------------
HORN-SAT GENERATION
------------------------------------------------------------
Horn-SAT problem generated in 0.00 seconds
------------------------------------------------------------
CNF → ANF CONVERSION (simple)
------------------------------------------------------------
ANF representation generated in 0.00 seconds
------------------------------------------------------------
GRÖBNER BASIS COMPUTATION
------------------------------------------------------------
Gröbner basis computed in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
------------------------------------------------------------
Guessed variable(s) (2):
  u
  y
============================================================

SAT

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver sat --maxguess 2 --maxsteps 5

Terminal output:

============================================================
SAT SOLVER — Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
============================================================
Variables: 7 | Relations: 5
Max guess: 2 | Max steps: 5
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (2):
  x
  s
============================================================

Now, we try to find the minimum number of guesses by using the --findmin switch. This will reduce the optimization problem (COP) into a sequence of decision problems (CSP) and solve them using SAT solvers. So, it may take more time to find the minimum number of guesses compared to finding some bounds on the number of guesses using SAT solvers.

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver sat --findmin 

Terminal output:

FIND-MIN MODE: searching for minimum guesses (starting from 7)
============================================================
  max_guess = 7:  SAT  — a guess basis of size 7 exists  (0.00s)
  max_guess = 6:  SAT  — a guess basis of size 6 exists  (0.00s)
  max_guess = 5:  SAT  — a guess basis of size 5 exists  (0.00s)
  max_guess = 4:  SAT  — a guess basis of size 4 exists  (0.00s)
  max_guess = 3:  SAT  — a guess basis of size 2 exists  (0.00s)
  max_guess = 2:  SAT  — a guess basis of size 2 exists  (0.00s)
  max_guess = 1:  UNSAT  (0.00s)

############################################################
FIND-MIN RESULT: minimum number of guesses = 2
Total findmin time: 0.00s
############################################################

Re-solving with max_guess = 2 for detailed output ...

(Note: the timings below are for this single verification
 solve only, not for the entire findmin search.)

============================================================
SAT SOLVER — Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
============================================================
Variables: 7 | Relations: 5
Max guess: 2 | Max steps: 7
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      7 / 7
Max steps used:            7
------------------------------------------------------------
Guessed variable(s) (2):
  x, s
============================================================

Total findmin search time: 0.00s

SMT

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver smt --maxguess 2 --maxsteps 5

Terminal output:

============================================================
SMT SOLVER — Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
============================================================
Variables: 7 | Relations: 5
Max guess: 2 | Max steps: 5
Solver: z3
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SMT model generated in 0.01 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (2):
  x
  v
============================================================

MILP

python3 autoguess.py --inputfile ciphers/Example1/relationfile.txt --solver milp --maxsteps 5

Terminal output:

Generating the MILP model ...
MILP model was generated after 0.00 seconds
Set parameter Username
Set parameter LicenseID to value 2782105
Academic license - for non-commercial use only - expires 2027-02-23
Read LP format model from file temp/milp_mg50_ms5_min_5d734ea45aa1173beb95c81f6cbc98.lp
Reading time = 0.00 seconds
: 287 rows, 167 columns, 1084 nonzeros
Set parameter MIPFocus to value 0
Set parameter Threads to value 0
Set parameter OutputFlag to value 1
Gurobi Optimizer version 13.0.1 build v13.0.1rc0 (mac64[arm] - Darwin 24.6.0 24G517)

CPU model: Apple M4
Thread count: 10 physical cores, 10 logical processors, using up to 10 threads

Optimize a model with 287 rows, 167 columns and 1084 nonzeros (Min)
Model fingerprint: 0x0de8c583
Model has 7 linear objective coefficients
Variable types: 0 continuous, 167 integer (167 binary)
Coefficient statistics:
  Matrix range     [1e+00, 5e+00]
  Objective range  [1e+00, 1e+00]
  Bounds range     [1e+00, 1e+00]
  RHS range        [1e+00, 5e+01]

Found heuristic solution: objective 7.0000000
Presolve removed 90 rows and 67 columns
Presolve time: 0.01s
Presolved: 197 rows, 100 columns, 802 nonzeros
Variable types: 0 continuous, 100 integer (100 binary)

Root relaxation: objective 2.516199e-02, 119 iterations, 0.00 seconds (0.00 work units)

    Nodes    |    Current Node    |     Objective Bounds      |     Work
 Expl Unexpl |  Obj  Depth IntInf | Incumbent    BestBd   Gap | It/Node Time

     0     0    0.02516    0   75    7.00000    0.02516   100%     -    0s
H    0     0                       2.0000000    0.02516  98.7%     -    0s
     0     0    1.00000    0   55    2.00000    1.00000  50.0%     -    0s

Cutting planes:
  Gomory: 2
  Cover: 6
  Clique: 6
  MIR: 2
  RLT: 12
  BQP: 6

Explored 1 nodes (245 simplex iterations) in 0.02 seconds (0.02 work units)
Thread count was 10 (of 10 available processors)

Solution count 2: 2 7 

Optimal solution found (tolerance 1.00e-04)
Best objective 2.000000000000e+00, best bound 2.000000000000e+00, gap 0.0000%
Solving process was finished after 0.02 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (2):
  x
  v
============================================================

Propagate

The propagate solver does not search for a minimal guess basis. Instead, given a set of initially known variables (via -kn), it iteratively deduces new variables using the relations until no further progress can be made. This is useful for quickly checking how far a particular guess set can reach.

autoguess --inputfile ciphers/Example1/relationfile.txt --solver propagate --known "u,v"

Terminal output:

============================================================
Knowledge propagation started - 2026-02-23 22:29:19.842286
Problem: Taken from https://doi.org/10.1007/978-3-642-00862-7_11: Speeding up Collision Search for Byte-Oriented Hash Functions
Total variables: 7
Total relations: 5 (symmetric: 5, implication: 0)
Initially known variables: 2
  u, v
============================================================

Iteration 1: learned 1 new variable(s)
  s  <--  [v, u, s]

Iteration 2: learned 1 new variable(s)
  x  <--  [x, s, v]

Iteration 3: learned 1 new variable(s)
  t  <--  [u, t, x]

Iteration 4: learned 1 new variable(s)
  z  <--  [z, s, v, t]

Iteration 5: learned 1 new variable(s)
  y  <--  [x, u, s, y, z]

============================================================
PROPAGATION SUMMARY
============================================================
Total iterations:          5
Initially known:           2
Newly learned:             5
Total known after prop.:   7 / 7
Unreachable variables:     0
Target variables covered:  7 / 7
Elapsed time:              0.0001 seconds
============================================================

Example 2

In this example we specify a subset of variables as the target and known variables. Note that, if you don’t specify any target variable, Autoguess considers all variables as the target variables. You can find the input file of this example in Example2 which includes the following contents:

connection relations
u, v, x, y, z
u, w, y, z
w, x, y, z
u, w, z
u, w => t
t, z, v
target
u
v
x
known
w
end

CP

python3 autoguess.py --inputfile ciphers/Example2/example2.txt --solver cp --maxsteps 5 --dglayout circo

Terminal output:

Number of guessed variables is set to be at most 7
============================================================
CP SOLVER — Example of our paper
============================================================
Variables: 7 | Relations: 6
Max guess: 7 | Max steps: 5
Solver: cp-sat
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
CP model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.27 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  u
============================================================

Groebner

python3 autoguess.py --inputfile ciphers/Example2/example2.txt --solver groebner

Terminal output:

============================================================
GRÖBNER BASIS SOLVER — Example of our paper
============================================================
Variables: 7 | Relations: 6
Term ordering: degrevlex | Overlapping: 2
CNF→ANF method: simple
------------------------------------------------------------
POLYNOMIAL RING CONSTRUCTION
------------------------------------------------------------
Generating Boolean Polynomial Ring in 7 variables ...
Ring constructed in 0.00 seconds
------------------------------------------------------------
HORN-SAT GENERATION
------------------------------------------------------------
Horn-SAT problem generated in 0.00 seconds
------------------------------------------------------------
CNF → ANF CONVERSION (simple)
------------------------------------------------------------
ANF representation generated in 0.00 seconds
------------------------------------------------------------
GRÖBNER BASIS COMPUTATION
------------------------------------------------------------
Gröbner basis computed in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
------------------------------------------------------------
Guessed variable(s) (1):
  x
============================================================

SAT

python3 autoguess.py --inputfile ciphers/Example2/example2.txt --solver sat --maxguess 1 --maxsteps 5

Terminal output:

============================================================
SAT SOLVER — Example of our paper
============================================================
Variables: 7 | Relations: 6
Max guess: 1 | Max steps: 5
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  u
============================================================

SMT

python3 autoguess.py --inputfile ciphers/Example2/example2.txt --solver smt --maxguess 1 --maxsteps 5

Terminal output:

============================================================
SMT SOLVER — Example of our paper
============================================================
Variables: 7 | Relations: 6
Max guess: 1 | Max steps: 5
Solver: z3
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SMT model generated in 0.01 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  z
============================================================

MILP

python3 autoguess.py --inputfile ciphers/Example2/example2.txt --solver milp --maxsteps 5

Terminal output:

Generating the MILP model ...
MILP model was generated after 0.00 seconds
Set parameter Username
Set parameter LicenseID to value 2782105
Academic license - for non-commercial use only - expires 2027-02-23
Read LP format model from file temp/milp_mg50_ms5_min_493b0329677a8e4da2a20c8408b175.lp
Reading time = 0.00 seconds
: 308 rows, 177 columns, 1200 nonzeros
Set parameter MIPFocus to value 0
Set parameter Threads to value 0
Set parameter OutputFlag to value 1
Gurobi Optimizer version 13.0.1 build v13.0.1rc0 (mac64[arm] - Darwin 24.6.0 24G517)

CPU model: Apple M4
Thread count: 10 physical cores, 10 logical processors, using up to 10 threads

Optimize a model with 308 rows, 177 columns and 1200 nonzeros (Min)
Model fingerprint: 0xbd74212b
Model has 6 linear objective coefficients
Variable types: 0 continuous, 177 integer (177 binary)
Coefficient statistics:
  Matrix range     [1e+00, 6e+00]
  Objective range  [1e+00, 1e+00]
  Bounds range     [1e+00, 1e+00]
  RHS range        [1e+00, 5e+01]

Found heuristic solution: objective 6.0000000
Presolve removed 215 rows and 130 columns
Presolve time: 0.00s
Presolved: 93 rows, 47 columns, 352 nonzeros
Variable types: 0 continuous, 47 integer (47 binary)

Root relaxation: objective 1.269841e-01, 39 iterations, 0.00 seconds (0.00 work units)

    Nodes    |    Current Node    |     Objective Bounds      |     Work
 Expl Unexpl |  Obj  Depth IntInf | Incumbent    BestBd   Gap | It/Node Time

     0     0    0.12698    0   30    6.00000    0.12698  97.9%     -    0s
H    0     0                       3.0000000    0.12698  95.8%     -    0s
H    0     0                       1.0000000    0.12698  87.3%     -    0s
     0     0    0.12698    0   30    1.00000    0.12698  87.3%     -    0s

Explored 1 nodes (41 simplex iterations) in 0.01 seconds (0.01 work units)
Thread count was 10 (of 10 available processors)

Solution count 3: 1 3 6 

Optimal solution found (tolerance 1.00e-04)
Best objective 1.000000000000e+00, best bound 1.000000000000e+00, gap 0.0000%
Solving process was finished after 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      7 / 7
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  z
============================================================

Example 3

In this example, we show the application of Autoguess to discover the possible early abortion techniques. The input file of this example is located in Example3 which includes the following contents:

# Example to describe the early abortion technique
# (x0 <<< 3) + S(x1) + x2 = 0
# S(x0) + S(x2) + (x5 <<< 2) = 0
# L(x1 + x2) + x5 = 0
# x2 + L(x3) = 0
# S(x3 * S(x1 * x4)) + L(x0) + x6 = 0
# (S(x4) xor L(x6)) + x3 = 0
connection relations
x0, x1, x2
x0, x2, x5
x1, x2, x5
x2, x3
x3, x1, x4 => t
t, x0, x6
x4, x6, x3
#known
#x0
#x4
#x5
end

We emphasize that the lines starting with # are considered as comments.

CP

python3 autoguess.py --inputfile ciphers/Example3/relationfile.txt --solver cp --maxguess 5

Terminal output:

============================================================
CP SOLVER — Example to describe the early abortion technique
============================================================
Variables: 8 | Relations: 7
Max guess: 5 | Max steps: 5
Solver: cp-sat
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
CP model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.20 seconds

============================================================
RESULTS
============================================================
Number of guesses:         3
Known in final state:      8 / 8
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (3):
  x1
  x5
  t
============================================================

The following graph represents the determination flow in the discovered GD attack.

The full content of the output file generated by Autoguess is as follows which includes many useful information guiding the user to find possible early abortion techniques:

Number of relations: 7
Number of variables: 8
Number of target variables: 8
Number of known variables: 0
Number of guessed variables: 3
Number of state copies (max_steps): 5
An upper bound for the number of guessed variables given by user (max_guess): 5
8 out of 8 state variables are known after 5 state copies
############################################################
The following 3 variable(s) are guessed:
x1, x5, t
############################################################
The following 0 variable(s) are initially known:

############################################################
Target variables:
x0, x1, x2, x5, x3, x4, t, x6
############################################################
Determination flow:

State 0:
x1, x5 in symmetric relation [x1, x2, x5] are known: x1, x5 ===> x2
############################################################
State 1:
x1, x2 in symmetric relation [x0, x1, x2] are known: x1, x2 ===> x0
x2, x5 in symmetric relation [x0, x2, x5] are known: x2, x5 ===> x0
x2 in symmetric relation [x2, x3] are known: x2 ===> x3
############################################################
State 2:
t, x0 in symmetric relation [t, x0, x6] are known: t, x0 ===> x6
############################################################
State 3:
x6, x3 in symmetric relation [x4, x6, x3] are known: x6, x3 ===> x4
############################################################
The following variables are known in final state:
x0, x1, x2, x5, x3, x4, t, x6
############################################################
The following relations have not been used in determination (they might be used to check the correctness of guesses):
x3, x1, x4 => t
############################################################
The following variables can be deduced from multiple paths:

x0 can be deduced from:
x0, x1, x2
x0, x2, x5

The first lines give a brief description of the input. The main body, describes how the remaining variables can be deduced from the guessed variables. As you can see, three steps (state copies) are sufficient to determine all of the variables. According to the last two lines of the output files, x0 can be deduced from two different equations, i.e., (x0 <<< 3) + S(x1) + x2 = 0 and S(x0) + S(x2) + (x5 <<< 2) = 0. By the way, according to the determination flow, x0 is determined before guessing t. Hence, a portion of wrong values for the two guessed variables, namely, x1, x5 can be detected and excluded from the search space before guessing x0 which results in a GD attack with less time complexity by a factor of 2^|x0|.

Groebner

python3 autoguess.py --inputfile ciphers/Example3/relationfile.txt --solver groebner

Terminal output:

============================================================
GRÖBNER BASIS SOLVER — Example to describe the early abortion technique
============================================================
Variables: 8 | Relations: 7
Term ordering: degrevlex | Overlapping: 2
CNF→ANF method: simple
------------------------------------------------------------
POLYNOMIAL RING CONSTRUCTION
------------------------------------------------------------
Generating Boolean Polynomial Ring in 8 variables ...
Ring constructed in 0.00 seconds
------------------------------------------------------------
HORN-SAT GENERATION
------------------------------------------------------------
Horn-SAT problem generated in 0.00 seconds
------------------------------------------------------------
CNF → ANF CONVERSION (simple)
------------------------------------------------------------
ANF representation generated in 0.00 seconds
------------------------------------------------------------
GRÖBNER BASIS COMPUTATION
------------------------------------------------------------
Gröbner basis computed in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         3
------------------------------------------------------------
Guessed variable(s) (3):
  x0
  x1
  x2
============================================================

SAT

python3 autoguess.py --inputfile ciphers/Example3/relationfile.txt --solver sat --maxguess 3 --maxsteps 3

Terminal output:

============================================================
SAT SOLVER — Example to describe the early abortion technique
============================================================
Variables: 8 | Relations: 7
Max guess: 3 | Max steps: 3
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         3
Known in final state:      8 / 8
Max steps used:            3
------------------------------------------------------------
Guessed variable(s) (3):
  x3
  x4
  t
============================================================

SMT

python3 autoguess.py --inputfile ciphers/Example3/relationfile.txt --solver smt --smtsolver z3 --maxguess 3 --maxsteps 3

Terminal output:

============================================================
SMT SOLVER — Example to describe the early abortion technique
============================================================
Variables: 8 | Relations: 7
Max guess: 3 | Max steps: 3
Solver: z3
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SMT model generated in 0.01 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         3
Known in final state:      8 / 8
Max steps used:            3
------------------------------------------------------------
Guessed variable(s) (3):
  x1
  x2
  x4
============================================================

MILP

python3 autoguess.py --inputfile ciphers/Example3/relationfile.txt --solver milp --maxsteps 3

Terminal output:

Generating the MILP model ...
MILP model was generated after 0.00 seconds
Set parameter Username
Set parameter LicenseID to value 2782105
Academic license - for non-commercial use only - expires 2027-02-23
Read LP format model from file temp/milp_mg50_ms3_min_c74688273c88de841250efd06ea0d9.lp
Reading time = 0.00 seconds
: 176 rows, 110 columns, 574 nonzeros
Set parameter MIPFocus to value 0
Set parameter Threads to value 0
Set parameter OutputFlag to value 1
Gurobi Optimizer version 13.0.1 build v13.0.1rc0 (mac64[arm] - Darwin 24.6.0 24G517)

CPU model: Apple M4
Thread count: 10 physical cores, 10 logical processors, using up to 10 threads

Optimize a model with 176 rows, 110 columns and 574 nonzeros (Min)
Model fingerprint: 0x7dfef622
Model has 8 linear objective coefficients
Variable types: 0 continuous, 110 integer (110 binary)
Coefficient statistics:
  Matrix range     [1e+00, 5e+00]
  Objective range  [1e+00, 1e+00]
  Bounds range     [1e+00, 1e+00]
  RHS range        [1e+00, 5e+01]

Found heuristic solution: objective 8.0000000
Presolve removed 94 rows and 66 columns
Presolve time: 0.00s
Presolved: 82 rows, 44 columns, 286 nonzeros
Variable types: 0 continuous, 44 integer (44 binary)

Root relaxation: objective 4.130435e-01, 49 iterations, 0.00 seconds (0.00 work units)

    Nodes    |    Current Node    |     Objective Bounds      |     Work
 Expl Unexpl |  Obj  Depth IntInf | Incumbent    BestBd   Gap | It/Node Time

     0     0    0.41304    0   29    8.00000    0.41304  94.8%     -    0s
H    0     0                       3.0000000    0.41304  86.2%     -    0s
     0     0    1.14286    0   28    3.00000    1.14286  61.9%     -    0s
     0     0    2.00000    0   31    3.00000    2.00000  33.3%     -    0s

Cutting planes:
  Gomory: 4
  Cover: 19
  Clique: 6
  MIR: 1
  Zero half: 3
  RLT: 14
  Relax-and-lift: 5

Explored 1 nodes (110 simplex iterations) in 0.02 seconds (0.01 work units)
Thread count was 10 (of 10 available processors)

Solution count 2: 3 8 

Optimal solution found (tolerance 1.00e-04)
Best objective 3.000000000000e+00, best bound 3.000000000000e+00, gap 0.0000%
Solving process was finished after 0.02 seconds

============================================================
RESULTS
============================================================
Number of guesses:         3
Known in final state:      8 / 8
Max steps used:            3
------------------------------------------------------------
Guessed variable(s) (3):
  x0
  x5
  t
============================================================

Example 4

In this example, we aim to show the advantage of preprocessing phase when some algebraic relations are included in the input file. The input file of this example which is located in Example4 includes the following quadratic equations over GF(2):

algebraic relations
X1*X3 + X2*X4 + X1 + X3 + X4
X2*X3 + X1*X4 + X3*X4 + X1 + X2 + X4
X2*X4 + X3*X4 + X1 + X3 + 1
X1*X2 + X1*X3 + X2*X3 + X3 + X4 + 1
X1*X2 + X2*X3 + X1*X4 + X3
X1*X3 + X1*X4 + X3*X4 + X1 + X2 + X3 + X4
X1*X2 + X2*X4 + X1 + 1
end

CP

The preprocessor of Autoguess is enabled by default and to disable it you can use --preprocess 0 in front of your command when you call Autoguess. To adjust the degree of preprocessing phase you can use this switch --D <your favorite degree, e.g., 2>. For example in the following command, we apply the preprocessing phase of Autoguess with degree of 2.

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver cp --maxsteps 10 --preprocess 1 --D 2 --dglayout circo

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 7 by 11 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:44:51.835018
#Dependent variables: 7
#Free variables: 3
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_676e0e7043290f519ee6de0bac1b84.txt - 2026-02-23 22:44:51.835115
Result was written into temp/macaulay_basis_676e0e7043290f519ee6de0bac1b84.txt after 0.00 seconds
Preprocessing finished in 1.4718 seconds
Number of guessed variables is set to be at most 10
============================================================
CP SOLVER — gdproblem
============================================================
Variables: 10 | Relations: 19
Max guess: 10 | Max steps: 10
Solver: cp-sat
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
CP model generated in 0.01 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.26 seconds

============================================================
RESULTS
============================================================
Number of guesses:         2
Known in final state:      10 / 10
Max steps used:            10
------------------------------------------------------------
Guessed variable(s) (2):
  X2
  X4
============================================================

Next, we call Autoguess with preprocessing of degree 3 to get a better result.

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver cp --maxsteps 10 --preprocess 1 --D 3 --dglayout circo

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 35 by 15 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:46:12.429585
#Dependent variables: 13
#Free variables: 1
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_88e597205e4bd22daf4ee4c083f4dc.txt - 2026-02-23 22:46:12.429697
Result was written into temp/macaulay_basis_88e597205e4bd22daf4ee4c083f4dc.txt after 0.00 seconds
Preprocessing finished in 1.5163 seconds
Number of guessed variables is set to be at most 14
============================================================
CP SOLVER — gdproblem
============================================================
Variables: 14 | Relations: 24
Max guess: 14 | Max steps: 10
Solver: cp-sat
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
CP model generated in 0.01 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.30 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      14 / 14
Max steps used:            10
------------------------------------------------------------
Guessed variable(s) (1):
  X2
============================================================

The Tikz code of the determination graph can also be generated by putting --tikz 1 in front of your command when you call Autoguess.

Groebner

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver groebner --preprocess 1 --D 3

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 35 by 15 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:47:05.293590
#Dependent variables: 13
#Free variables: 1
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_7f40767192abe937548909a93544f6.txt - 2026-02-23 22:47:05.293753
Result was written into temp/macaulay_basis_7f40767192abe937548909a93544f6.txt after 0.00 seconds
Preprocessing finished in 0.0808 seconds
============================================================
GRÖBNER BASIS SOLVER — gdproblem
============================================================
Variables: 14 | Relations: 24
Term ordering: degrevlex | Overlapping: 2
CNF→ANF method: simple
------------------------------------------------------------
POLYNOMIAL RING CONSTRUCTION
------------------------------------------------------------
Generating Boolean Polynomial Ring in 14 variables ...
Ring constructed in 0.00 seconds
------------------------------------------------------------
HORN-SAT GENERATION
------------------------------------------------------------
Horn-SAT problem generated in 0.00 seconds
------------------------------------------------------------
CNF → ANF CONVERSION (simple)
------------------------------------------------------------
ANF representation generated in 0.00 seconds
------------------------------------------------------------
GRÖBNER BASIS COMPUTATION
------------------------------------------------------------
Gröbner basis computed in 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
------------------------------------------------------------
Guessed variable(s) (1):
  X3
============================================================

SAT

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver sat --maxguess 1 --maxsteps 5 --preprocess 1 --D 3

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 35 by 15 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:47:55.291771
#Dependent variables: 13
#Free variables: 1
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_c918ac2c862f0bfbd05f830067a239.txt - 2026-02-23 22:47:55.291903
Result was written into temp/macaulay_basis_c918ac2c862f0bfbd05f830067a239.txt after 0.00 seconds
Preprocessing finished in 1.5456 seconds
============================================================
SAT SOLVER — gdproblem
============================================================
Variables: 14 | Relations: 24
Max guess: 1 | Max steps: 5
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      14 / 14
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  X2
============================================================

SMT

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver smt --maxguess 1 --maxsteps 5 --preprocess 1 --D 3

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 35 by 15 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:48:10.731367
#Dependent variables: 13
#Free variables: 1
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_41304864ec176a77963f8daabe4832.txt - 2026-02-23 22:48:10.731486
Result was written into temp/macaulay_basis_41304864ec176a77963f8daabe4832.txt after 0.00 seconds
Preprocessing finished in 1.6922 seconds
============================================================
SMT SOLVER — gdproblem
============================================================
Variables: 14 | Relations: 24
Max guess: 1 | Max steps: 5
Solver: z3
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SMT model generated in 0.03 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      14 / 14
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  VULX1x3 (represents: X2 * X4)
============================================================

MILP

python3 autoguess.py --inputfile ciphers/Example4/algebraic_relations.txt --solver milp --maxsteps 5 --preprocess 1 --D 3

Terminal output:

------------------------------------------------------------
PREPROCESSING (Macaulay matrix)
------------------------------------------------------------
Number of algebraic equations: 7
Number of algebraic variables: 4
Number of algebraic monomials: 11
Spectrum of degrees: [2]
Macaulay matrix was generated in full matrixspace of 35 by 15 sparse matrices over finite field of size 2
Gaussian elimination was started - 2026-02-23 22:48:29.854185
#Dependent variables: 13
#Free variables: 1
Gaussian elimination was finished after 0.00 seconds
Writing the results into the temp/macaulay_basis_170a23f2bde01f3bbf6fb967d3c415.txt - 2026-02-23 22:48:29.854295
Result was written into temp/macaulay_basis_170a23f2bde01f3bbf6fb967d3c415.txt after 0.00 seconds
Preprocessing finished in 1.6932 seconds
Generating the MILP model ...
MILP model was generated after 0.00 seconds
Set parameter Username
Set parameter LicenseID to value 2782105
Academic license - for non-commercial use only - expires 2027-02-23
Read LP format model from file temp/milp_mg50_ms5_min_11d3a43ee22ec0813703f97835cb8d.lp
Reading time = 0.00 seconds
: 728 rows, 444 columns, 3268 nonzeros
Set parameter MIPFocus to value 0
Set parameter Threads to value 0
Set parameter OutputFlag to value 1
Gurobi Optimizer version 13.0.1 build v13.0.1rc0 (mac64[arm] - Darwin 24.6.0 24G517)

CPU model: Apple M4
Thread count: 10 physical cores, 10 logical processors, using up to 10 threads

Optimize a model with 728 rows, 444 columns and 3268 nonzeros (Min)
Model fingerprint: 0xc1841a82
Model has 8 linear objective coefficients
Variable types: 0 continuous, 444 integer (444 binary)
Coefficient statistics:
  Matrix range     [1e+00, 1e+01]
  Objective range  [1e+00, 1e+00]
  Bounds range     [1e+00, 1e+00]
  RHS range        [1e+00, 5e+01]

Found heuristic solution: objective 8.0000000
Presolve removed 687 rows and 417 columns
Presolve time: 0.01s
Presolved: 41 rows, 27 columns, 208 nonzeros
Variable types: 0 continuous, 27 integer (27 binary)
Found heuristic solution: objective 7.0000000

Root relaxation: objective 1.000000e+00, 1 iterations, 0.00 seconds (0.00 work units)

    Nodes    |    Current Node    |     Objective Bounds      |     Work
 Expl Unexpl |  Obj  Depth IntInf | Incumbent    BestBd   Gap | It/Node Time

*    0     0               0       1.0000000    1.00000  0.00%     -    0s

Explored 1 nodes (1 simplex iterations) in 0.01 seconds (0.01 work units)
Thread count was 10 (of 10 available processors)

Solution count 3: 1 7 8 

Optimal solution found (tolerance 1.00e-04)
Best objective 1.000000000000e+00, best bound 1.000000000000e+00, gap 0.0000%
Solving process was finished after 0.01 seconds

============================================================
RESULTS
============================================================
Number of guesses:         1
Known in final state:      14 / 14
Max steps used:            5
------------------------------------------------------------
Guessed variable(s) (1):
  AADO0x2x3 (represents: X1 * X3 * X4)
============================================================

Example 5

In this example, we show how to build an input file consisting of variables with different weights. The input file of this example is located in Example5 which includes the following contents:

connection relations
x0, x1, x2
x0, x2, x5
x1, x2, x5
x2, x3
x3, x1, x4 => t
t, x0, x6
x4, x6, x3
weights
x0 1
x1 2
x2 1
x3 3
x4 1
x5 2
x6 3
t 2
end

SAT

python3 autoguess.py --inputfile ciphers/Example5/example5.txt --solver sat --maxguess 3 --maxsteps 5 --dglayout circo

Terminal output:

============================================================
SAT SOLVER — gdproblem
============================================================
Variables: 8 | Relations: 7
Max guess: 3 | Max steps: 5
Solver: cadical153
------------------------------------------------------------
MODEL GENERATION
------------------------------------------------------------
SAT model generated in 0.00 seconds
------------------------------------------------------------
SOLVING
------------------------------------------------------------
Solving finished in 0.00 seconds

============================================================
RESULTS
==================================================</your>

> README 内容过长，已截取前 64 KB。完整内容请前往 GitHub 仓库查看。