\documentclass[conference]{IEEEtran}
% packages
\usepackage{xspace}
\usepackage{hyperref}
\usepackage{todonotes}
\usepackage{tikz}
\usepackage[utf8]{inputenc}

\def\CC{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}}
\def\ea{\,et\,al.\ }

\begin{document}
	
% paper title
\title{At Least Two Solutions}

% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{
\IEEEauthorblockN{Norbert Manthey}
\IEEEauthorblockA{nmanthey@conp-solutions.com\\Dresden, Germany}
}

\maketitle

\def\coprocessor{\textsc{Coprocessor}\xspace}
\def\ALT{\textsc{AtLeastTwo}\xspace}

% the abstract is optional
\begin{abstract}
This document describes the \ALT tool, as well as the benchmarks that have been submitted to the SAT competition 2021.
The tool takes a CNF and encodes a new CNF which is satisfiable only if the initial CNF has at least two satisfying solutions. The difference of the two solutions can be restricted to input variables only, to support formulas that have been encoded with auxiliary variables.
The generated formulas are expected to reduce the effectiveness of symmetry breaking, as well as reduce the number of autarkies in formulas.
\end{abstract}

\section{Introduction}

When encoding problems, one might ask whether given problem has more than one solution.
This property is for example useful when generating logic puzzles to know whether a generated puzzle has multiple solutions.
A related property is to encode that a formula has exactly one solution.
Similarly, the encoding could be extended to ask for at least two satisfying assignments, or at most $k$ satisfying assignments.
However, the result formula would grow quadratically with $k$.
The current tool only supports asking for at least two solutions.
Other extensions would be to encode that at least a given number of $K$ assignments need to be different.
In this case, the currently used \emph{at-least-$k$} constraint -- a clause -- would have to be replaced by a properly encoded cardinality constraint.

The generated formulas are expected to reduce the effectiveness of symmetry breaking, because for a symmetry in the output formula, there would need to by a symmetry in the input formula that works for pairs of solutions.
Similarly, for an autarky in the input formula would have to be extended to the clauses that require the assignment of variables being different.
This results at least in larger autarkies.

\section{Encoding At Least Two Solutions}

The input for the \ALT tool is an uncompressed CNF file with the formulas $F$.
This formula has $n$ variables, and $m$ clauses, where we assume all variables $n$ to be present.
As in CNF, variables are represented as integers, we will use math rules to describe transformations.
The resulting formula is basically encoded by the following steps:
(1) duplicate $F$ into a formula $G$, but add the offset $n$ to all variables to obtain fresh variables,
(2) encode the equivalence for all variable pairs in $F$ and $G$, respecting the offset, and
(3) enforce that are least one equivalence from (2) is falsified.
The three steps will be explained in more details next.

\subsection{Duplicate Input Formula}

As a first step, we duplicate all clauses in $F$.
During this step, for all clauses $C_i$, we add the offset $n$ to the variable representation of all literals $l_i$ when creating the new clauses.

\[G := \bigwedge_{C_i \in F} \bigvee_{l_i \in C_i} l_i + n \]

\subsection{Encode Solution Equality}

To encode whether two variable assignments are equivalent, we need to introduce a new variable for each existing variable in $F$, or at least for the range of selected variables whose satisfying assignment should be different.
Let $e$ be the number of variables from $1$ to $e$ which should have at least one different assignment.
As the default case, the number of variables to consider is the number of variables in the input, i.e. $e = n$.

\[E := \bigwedge_{i=1}^{e} a_i \leftrightarrow (f_i \leftrightarrow g_i), \]

\noindent
where $a_i$ are variables that do not occur in $F$ nor in $G$.
Note, the variables $f_i$ and $g_i$ again have the offset of $n$ again, i.e. $g_i = f_i +n$.

\subsection{Force Inequality of Solutions}

When combining all formulas above, we obtain a formula that encodes the same formulas twice, and a sub-formula that indicates whether the assignments for both formulas are equal:

\[R' = F \land G \land E. \]

\noindent
A model for this formula can assign the same truth value for all variable pairs in $F$ and $G$.
To make sure, the models are different, we need to ensure that at least one pair of variables is not equal, by encoding an at-least-one constraint for the new auxiliary variables:

\[R = F \land G \land E \land \bigvee_{i=1}^{e} \neg a_i.  \]

\noindent
Formula $R$ is the resulting formula that will be generated by the tool.

\subsection{Properties of the Generated Formula}

First, we discuss the relationship between the satisfiability of the input formula $F$ and the produced formula $R$.
When the input formula $F$ is unsatisfiable, the resulting formula $R$ is also unsatisfiable.

Next, when $F$ has exactly one model, the truth values of this model can be assigned to satisfy $F$.
Formula $G$ will can only be satisfied with the same set of assignments.
Consequently, all variables $a_i$ will be assigned to $\top$.
In this case, the last sub-formula of $R$ will be falsified.

In the final case, multiple model $I$ and $J$ exist to satisfy $F$.
Then, $I$ can satisfy $F$, and $J$ can satisfy $G$ by respecting the offset $n$.
As $I$ and $J$ are different, at least one variable $a_i$ will be assigned to $\bot$, resulting in a satisfying assignment for $R$.
Note, such a satisfying assignment to $R$ contains the two models $I$ and $J$ that satisfy the input formula $F$.

Given a formula $F$ with $n$ variables and $m$ clauses, as well as targetting $e$ variables with $e \leq n$ for the in-equality results in a formula $R$ with $2n + e$ variables.
Furthermore, $R$ has $2m + 4e$ clauses, because an equality of three variables can be encoded with $4$ clauses.

\section{The Submitted Benchmark}

The submitted benchmark formulas have been generated by using formulas from previous SAT competition benchmarks.
\newpage

\noindent
The initial set of formulas to select the submitted formulas from is the robust benchmark for tuning SAT solvers from~\cite{SATgauss}.



\section{Availability}

The source of the tool is publicly available under the MIT license at \url{https://github.com/conp-solutions/cnfmiter}.

\bibliographystyle{IEEEtranS}
\bibliography{local}

\end{document}
