talk.tex

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath, amssymb}
\usepackage{graphicx}
\usepackage{titlesec}
\usepackage{enumitem}
\usepackage{lmodern}
\usepackage{hyperref}
\usepackage{xcolor}

\definecolor{titleblue}{RGB}{10,45,120}
\definecolor{graytext}{gray}{0.2}

\titleformat{\section}{\normalfont\Large\bfseries\color{titleblue}}{}{0pt}{}
\titleformat{\subsection}{\normalfont\large\bfseries\color{titleblue}}{}{0pt}{}

\renewcommand{\baselinestretch}{1.15}

\title{\textbf{SAT Solvers and Permutation Patterns: A New Frontier in Combinatorics}}
\author{Seyyed Ali Mohammadiyeh \\
Department of Pure Mathematics, University of Kashan \\
\texttt{max@std.kashanu.ac.ir}, \texttt{alim@kashanu.ac.ir}
}

\date{
\vspace{0.5em}
\large
\textit{Permutation Patterns 2025} \\
International Conference on Permutation Patterns \\
St Andrews, Scotland \\
July 7--11, 2025
}

\begin{document}

\maketitle

\vspace{-1.5em}
\section*{Abstract}

The study of permutation patterns is a rich and evolving area in combinatorics, deeply connected to sorting algorithms, enumerative structures, and discrete geometry. In this talk, we introduce a novel approach that brings together the power of \textbf{Boolean satisfiability solvers (SAT solvers)} and the theory of permutation patterns. 

\medskip

We investigate how modern SAT solvers can be harnessed to model and solve problems in \textbf{pattern containment}, \textbf{avoidance}, and \textbf{classification of permutation classes}. By encoding constraints into propositional logic, we enable automated reasoning about the existence of permutations that satisfy complex pattern conditions, including classical, vincular, and barred patterns.

\medskip

This computational methodology allows us to explore longstanding open problems, such as verifying \textbf{Wilf-equivalence}, generating minimal counterexamples, and testing conjectures that are beyond current enumeration techniques. Our encoding is flexible, efficient, and extensible, designed to reduce variable count and solve time for patterns of increasing complexity.

\medskip

We present experimental results and case studies where SAT-based approaches provide new insights, particularly in analyzing permutation classes of length 4 and 5. These results show how tools from theoretical computer science can contribute to pure mathematical discovery.

\medskip

This fusion of logic and combinatorics opens new doors for researchers, suggesting a broader framework for the use of SAT solvers in algebraic and enumerative combinatorics.

\vfill
\noindent
\textbf{Keywords:} SAT solvers, permutation patterns, pattern avoidance, pattern containment, Wilf-equivalence, computational combinatorics, logic encoding

\end{document}