You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
413 lines
14 KiB
413 lines
14 KiB
%* cnfsat.tex *%
|
|
|
|
\documentclass[11pt,draft]{article}
|
|
\usepackage{amssymb}
|
|
\usepackage{indentfirst}
|
|
|
|
\setlength{\textwidth}{6.5in}
|
|
\setlength{\textheight}{8.5in}
|
|
\setlength{\oddsidemargin}{0in}
|
|
\setlength{\topmargin}{0in}
|
|
\setlength{\headheight}{0in}
|
|
\setlength{\headsep}{0in}
|
|
\setlength{\footskip}{0.5in}
|
|
\setlength{\parindent}{16pt}
|
|
\setlength{\parskip}{5pt}
|
|
\setlength{\topsep}{0pt}
|
|
\setlength{\partopsep}{0pt}
|
|
\setlength{\itemsep}{\parskip}
|
|
\setlength{\parsep}{0pt}
|
|
\setlength{\leftmargini}{\parindent}
|
|
\renewcommand{\labelitemi}{---}
|
|
|
|
\def\para#1{\noindent{\bf#1}}
|
|
\def\synopsis{\para{Synopsis}}
|
|
\def\description{\para{Description}}
|
|
\def\returns{\para{Returns}}
|
|
|
|
\newenvironment{retlist}
|
|
{ \def\arraystretch{1.5}
|
|
\noindent
|
|
\begin{tabular}{@{}p{1in}@{}p{5.5in}@{}}
|
|
}
|
|
{\end{tabular}}
|
|
|
|
\begin{document}
|
|
|
|
\title{\bf CNF Satisfiability Problem}
|
|
|
|
\author{Andrew Makhorin {\tt<mao@gnu.org>}}
|
|
|
|
\date{August 2011}
|
|
|
|
\maketitle
|
|
|
|
\section{Introduction}
|
|
|
|
The {\it Satisfiability Problem (SAT)} is a classic combinatorial
|
|
problem. Given a Boolean formula of $n$ variables
|
|
$$f(x_1,x_2,\dots,x_n),\eqno(1.1)$$
|
|
this problem is to find such values of the variables, on which the
|
|
formula takes on the value {\it true}.
|
|
|
|
The {\it CNF Satisfiability Problem (CNF-SAT)} is a version of the
|
|
Satisfiability Problem, where the Boolean formula (1.1) is specified
|
|
in the {\it Conjunctive Normal Form (CNF)}, that means that it is a
|
|
conjunction of {\it clauses}, where a clause is a disjunction of
|
|
{\it literals}, and a literal is a variable or its negation.
|
|
For example:
|
|
$$(x_1\vee x_2)\;\&\;(\neg x_2\vee x_3\vee\neg x_4)\;\&\;(\neg
|
|
x_1\vee x_4).\eqno(1.2)$$
|
|
Here $x_1$, $x_2$, $x_3$, $x_4$ are Boolean variables to be assigned,
|
|
$\neg$ means
|
|
negation (logical {\it not}), $\vee$ means disjunction (logical
|
|
{\it or}), and $\&$ means conjunction (logical {\it and}). One may
|
|
note that the formula (1.2) is {\it satisfiable}, because on
|
|
$x_1$ = {\it true}, $x_2$ = {\it false}, $x_3$ = {\it false}, and
|
|
$x_4$ = {\it true} it takes on the value {\it true}. If a formula
|
|
is not satisfiable, it is called {\it unsatisfiable}, that means that
|
|
it takes on the value {\it false} on any values of its variables.
|
|
|
|
Any CNF-SAT problem can be easily translated to a 0-1 programming
|
|
problem as follows.\linebreak A Boolean variable $x$ can be modeled by
|
|
a binary variable in a natural way: $x=1$ means that $x$ takes on the
|
|
value {\it true}, and $x=0$ means that $x$ takes on the value
|
|
{\it false}. Then, if a literal is a negated variable, i.e. $t=\neg x$,
|
|
it can be expressed as $t=1-x$. Since a formula in CNF is a conjunction
|
|
of clauses, to provide its satisfiability we should require all its
|
|
clauses to take on the value {\it true}. A particular clause is
|
|
a disjunction of literals:
|
|
$$t\vee t'\vee t''\dots ,\eqno(1.3)$$
|
|
so it takes on the value {\it true} iff at least one of its literals
|
|
takes on the value {\it true}, that can be expressed as the following
|
|
inequality constraint:
|
|
$$t+t'+t''+\dots\geq 1.\eqno(1.4)$$
|
|
Note that no objective function is used in this case, because only
|
|
a feasible solution needs to be found.
|
|
|
|
For example, the formula (1.2) can be translated to the following
|
|
constraints:
|
|
$$\begin{array}{c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c}
|
|
x_1&+&x_2&&&&&\geq&1\\
|
|
&&(1-x_2)&+&x_3&+&(1-x_4)&\geq&1\\
|
|
(1-x_1)&&&&&+&x_4&\geq&1\\
|
|
\end{array}$$
|
|
$$x_1, x_2, x_3, x_4\in\{0,1\}$$
|
|
Carrying out all constant terms to the right-hand side gives
|
|
corresponding 0-1 programming problem in the standard format:
|
|
$$\begin{array}{r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }r}
|
|
x_1&+&x_2&&&&&\geq&1\\
|
|
&-&x_2&+&x_3&-&x_4&\geq&-1\\
|
|
-x_1&&&&&+&x_4&\geq&0\\
|
|
\end{array}$$
|
|
$$x_1, x_2, x_3, x_4\in\{0,1\}$$
|
|
|
|
In general case translation of a CNF-SAT problem results in the
|
|
following 0-1 programming problem:
|
|
$$\sum_{j\in J^+_i}x_j-\sum_{j\in J^-_i}x_j\geq 1-|J^-_i|,
|
|
\ \ \ i=1,\dots,m\eqno(1.5)$$
|
|
$$x_j\in\{0,1\},\ \ \ j=1,\dots,n\eqno(1.6)$$
|
|
where $n$ is the number of variables, $m$ is the number of clauses
|
|
(inequality constraints),\linebreak $J^+_i\subseteq\{1,\dots,n\}$ is
|
|
a subset of variables, whose literals in $i$-th clause do not have
|
|
negation, and $J^-_i\subseteq\{1,\dots,n\}$ is a subset of variables,
|
|
whose literals in $i$-th clause are negations of that variables. It is
|
|
assumed that $J^+_i\cap J^-_i=\varnothing$ for all $i$.
|
|
|
|
\section{GLPK API Routines}
|
|
|
|
\subsection{glp\_read\_cnfsat --- read CNF-SAT problem data in DIMACS
|
|
format}
|
|
|
|
\synopsis
|
|
|
|
\begin{verbatim}
|
|
int glp_read_cnfsat(glp_prob *P, const char *fname);
|
|
\end{verbatim}
|
|
|
|
\description
|
|
|
|
The routine \verb|glp_read_cnfsat| reads the CNF-SAT problem data from
|
|
a text file in DIMACS format and automatically translates the data to
|
|
corresponding 0-1 programming problem instance (1.5)--(1.6).
|
|
|
|
The parameter \verb|P| specifies the problem object, to which the
|
|
0-1 programming problem instance should be stored. Note that before
|
|
reading data the current content of the problem object is completely
|
|
erased with the routine \verb|glp_erase_prob|.
|
|
|
|
The character string \verb|fname| specifies the name of a text file
|
|
to be read in. (If the file name ends with the suffix `\verb|.gz|',
|
|
the file is assumed to be compressed, in which case the routine
|
|
decompresses it ``on the fly''.)
|
|
|
|
\newpage
|
|
|
|
\returns
|
|
|
|
If the operation was successful, the routine returns zero. Otherwise,
|
|
it prints an error message and returns non-zero.
|
|
|
|
\para{DIMACS CNF-SAT problem format}\footnote{This material is based on
|
|
the paper ``Satisfiability Suggested Format'', which is publicly
|
|
available at {\tt http://dimacs.rutgers.edu/}.}
|
|
|
|
The DIMACS input file is a plain ASCII text file. It contains lines of
|
|
several types described below. A line is terminated with an end-of-line
|
|
character. Fields in each line are separated by at least one blank
|
|
space.
|
|
|
|
\para{Comment lines.} Comment lines give human-readable information
|
|
about the file and are ignored by programs. Comment lines can appear
|
|
anywhere in the file. Each comment line begins with a lower-case
|
|
character \verb|c|.
|
|
|
|
\begin{verbatim}
|
|
c This is a comment line
|
|
\end{verbatim}
|
|
|
|
\para{Problem line.} There is one problem line per data file. The
|
|
problem line must appear before any clause lines. It has the following
|
|
format:
|
|
|
|
\begin{verbatim}
|
|
p cnf VARIABLES CLAUSES
|
|
\end{verbatim}
|
|
|
|
\noindent
|
|
The lower-case character \verb|p| signifies that this is a problem
|
|
line. The three character problem designator \verb|cnf| identifies the
|
|
file as containing specification information for the CNF-SAT problem.
|
|
The \verb|VARIABLES| field contains an integer value specifying $n$,
|
|
the number of variables in the instance. The \verb|CLAUSES| field
|
|
contains an integer value specifying $m$, the number of clauses in the
|
|
instance.
|
|
|
|
\para{Clauses.} The clauses appear immediately after the problem
|
|
line. The variables are assumed to be numbered from 1 up to $n$. It is
|
|
not necessary that every variable appears in the instance. Each clause
|
|
is represented by a sequence of numbers separated by either a space,
|
|
tab, or new-line character. The non-negated version of a variable $j$
|
|
is represented by $j$; the negated version is represented by $-j$. Each
|
|
clause is terminated by the value 0. Unlike many formats that represent
|
|
the end of a clause by a new-line character, this format allows clauses
|
|
to be on multiple lines.
|
|
|
|
\para{Example.} Below here is an example of the data file in DIMACS
|
|
format corresponding to the CNF-SAT problem (1.2).
|
|
|
|
\begin{footnotesize}
|
|
\begin{verbatim}
|
|
c sample.cnf
|
|
c
|
|
c This is an example of the CNF-SAT problem data
|
|
c in DIMACS format.
|
|
c
|
|
p cnf 4 3
|
|
1 2 0
|
|
-4 3
|
|
-2 0
|
|
-1 4 0
|
|
c
|
|
c eof
|
|
\end{verbatim}
|
|
\end{footnotesize}
|
|
|
|
\newpage
|
|
|
|
\subsection{glp\_check\_cnfsat --- check for CNF-SAT problem instance}
|
|
|
|
\synopsis
|
|
|
|
\begin{verbatim}
|
|
int glp_check_cnfsat(glp\_prob *P);
|
|
\end{verbatim}
|
|
|
|
\description
|
|
|
|
The routine \verb|glp_check_cnfsat| checks if the specified problem
|
|
object \verb|P| contains a 0-1 programming problem instance in the
|
|
format (1.5)--(1.6) and therefore encodes a CNF-SAT problem instance.
|
|
|
|
\returns
|
|
|
|
If the specified problem object has the format (1.5)--(1.6), the
|
|
routine returns zero, otherwise non-zero.
|
|
|
|
\subsection{glp\_write\_cnfsat --- write CNF-SAT problem data in DIMACS
|
|
format}
|
|
|
|
\synopsis
|
|
|
|
\begin{verbatim}
|
|
int glp_write_cnfsat(glp_prob *P, const char *fname);
|
|
\end{verbatim}
|
|
|
|
\description
|
|
|
|
The routine \verb|glp_write_cnfsat| automatically translates the
|
|
specified 0-1 programming problem instance (1.5)--(1.6) to a CNF-SAT
|
|
problem instance and writes the problem data to a text file in DIMACS
|
|
format.
|
|
|
|
The parameter \verb|P| is the problem object, which should specify
|
|
a 0-1 programming problem instance in the format (1.5)--(1.6).
|
|
|
|
The character string \verb|fname| specifies a name of the output text
|
|
file to be written. (If the file name ends with suffix `\verb|.gz|',
|
|
the file is assumed to be compressed, in which case the routine
|
|
performs automatic compression on writing that file.)
|
|
|
|
\returns
|
|
|
|
If the operation was successful, the routine returns zero. Otherwise,
|
|
it prints an error message and returns non-zero.
|
|
|
|
\subsection{glp\_minisat1 --- solve CNF-SAT problem instance with
|
|
MiniSat solver}
|
|
|
|
\synopsis
|
|
|
|
\begin{verbatim}
|
|
int glp_minisat1(glp_prob *P);
|
|
\end{verbatim}
|
|
|
|
\description
|
|
|
|
The routine \verb|glp_minisat1| is a driver to MiniSat, a CNF-SAT
|
|
solver developed by Niklas E\'en and Niklas S\"orensson, Chalmers
|
|
University of Technology, Sweden.\footnote{The MiniSat software module
|
|
is {\it not} part of GLPK, but is used with GLPK and included in the
|
|
distribution.}
|
|
|
|
\newpage
|
|
|
|
It is assumed that the specified problem object \verb|P| contains
|
|
a 0-1 programming problem instance in the format (1.5)--(1.6) and
|
|
therefore encodes a CNF-SAT problem instance.
|
|
|
|
If the problem instance has been successfully solved to the end, the
|
|
routine \verb|glp_minisat1| returns 0. In this case the routine
|
|
\verb|glp_mip_status| can be used to determine the solution status:
|
|
|
|
\begin{itemize}
|
|
\item {\tt GLP\_OPT} means that the solver found an integer feasible
|
|
solution and therefore the corresponding CNF-SAT instance is
|
|
satisfiable;
|
|
|
|
\item {\tt GLP\_NOFEAS} means that no integer feasible solution exists
|
|
and therefore the corresponding CNF-SAT instance is unsatisfiable.
|
|
\end{itemize}
|
|
|
|
If an integer feasible solution was found, corresponding values of
|
|
binary variables can be retrieved with the routine
|
|
\verb|glp_mip_col_val|.
|
|
|
|
\returns
|
|
|
|
\begin{retlist}
|
|
0 & The MIP problem instance has been successfully solved. (This code
|
|
does {\it not} necessarily mean that the solver has found feasible
|
|
solution. It only means that the solution process was successful.)\\
|
|
|
|
{\tt GLP\_EDATA} & The specified problem object contains a MIP
|
|
instance which does {\it not} have the format (1.5)--(1.6).\\
|
|
|
|
{\tt GLP\_EFAIL} & The solution process was unsuccessful because of
|
|
the solver failure.\\
|
|
\end{retlist}
|
|
|
|
\subsection{glp\_intfeas1 --- solve integer feasibility problem}
|
|
|
|
\synopsis
|
|
|
|
\begin{verbatim}
|
|
int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound);
|
|
\end{verbatim}
|
|
|
|
\description
|
|
|
|
The routine \verb|glp_intfeas1| is a tentative implementation of
|
|
an integer feasibility solver based on a CNF-SAT solver (currently
|
|
it is MiniSat; see Subsection 2.4).
|
|
|
|
If the parameter \verb|use_bound| is zero, the routine searches for
|
|
{\it any} integer feasibile solution to the specified integer
|
|
programming problem. Note that in this case the objective function is
|
|
ignored.
|
|
|
|
If the parameter \verb|use_bound| is non-zero, the routine searches for
|
|
an integer feasible solution, which provides a value of the objective
|
|
function not worse than \verb|obj_bound|. In other word, the parameter
|
|
\verb|obj_bound| specifies an upper (in case of minimization) or lower
|
|
(in case of maximization) bound to the objective function.
|
|
|
|
If the specified problem has been successfully solved to the end, the
|
|
routine \verb|glp_intfeas1| returns 0. In this case the routine
|
|
\verb|glp_mip_status| can be used to determine the solution status:
|
|
|
|
\begin{itemize}
|
|
\item {\tt GLP\_FEAS} means that the solver found an integer feasible
|
|
solution;
|
|
|
|
\item {\tt GLP\_NOFEAS} means that the problem has no integer feasible
|
|
solution (if {\tt use\_bound} is zero) or it has no integer feasible
|
|
solution, which is not worse than {\tt obj\_bound} (if {\tt use\_bound}
|
|
is non-zero).
|
|
\end{itemize}
|
|
|
|
\newpage
|
|
|
|
If an integer feasible solution was found, corresponding values of
|
|
variables (columns) can be retrieved with the routine
|
|
\verb|glp_mip_col_val|.
|
|
|
|
\para{Usage Notes}
|
|
|
|
The integer programming problem specified by the parameter \verb|P|
|
|
should satisfy to the following requirements:
|
|
|
|
\begin{enumerate}
|
|
\item All variables (columns) should be either binary ({\tt GLP\_BV})
|
|
or fixed at integer values ({\tt GLP\_FX}).
|
|
|
|
\item All constraint and objective coefficients should be integer
|
|
numbers in the range\linebreak $[-2^{31},\ +2^{31}-1]$.
|
|
\end{enumerate}
|
|
|
|
Though there are no special requirements to the constraints,
|
|
currently the routine \verb|glp_intfeas1| is efficient mainly for
|
|
problems, where most constraints (rows) fall into the following three
|
|
classes:
|
|
|
|
\begin{enumerate}
|
|
\item Covering inequalities
|
|
$$\sum_{j}t_j\geq 1,$$
|
|
where $t_j=x_j$ or $t_j=1-x_j$, $x_j$ is a binary variable.
|
|
|
|
\item Packing inequalities
|
|
$$\sum_{j}t_j\leq 1.$$
|
|
|
|
\item Partitioning equalities (SOS1 constraints)
|
|
$$\sum_{j}t_j=1.$$
|
|
\end{enumerate}
|
|
|
|
\returns
|
|
|
|
\begin{retlist}
|
|
0 & The problem has been successfully solved. (This code does
|
|
{\it not} necessarily mean that the solver has found an integer
|
|
feasible solution. It only means that the solution process was
|
|
successful.) \\
|
|
|
|
{\tt GLP\_EDATA} & The specified problem object does not satisfy
|
|
to the requirements listed in Paragraph `Usage Notes'. \\
|
|
|
|
{\tt GLP\_ERANGE} & An integer overflow occured on translating the
|
|
specified problem to a CNF-SAT problem. \\
|
|
|
|
{\tt GLP\_EFAIL} & The solution process was unsuccessful because of
|
|
the solver failure. \\
|
|
\end{retlist}
|
|
|
|
\end{document}
|