\Smodels: A System for Answer Set Programming\thanks{% The work has been funded by the Academy of Finland (Project 43963) and by Helsinki Graduate School in Computer Science and Engineering. }
Ilkka Niemel\"a
Patrik Simons
Tommi Syrj\"anen
Dept.\ of Computer Science and Eng.
Laboratory for Theoretical Computer Science
P.O.Box 5400
FIN-02015 HUT
Finland
\noindent The \Smodels\ system implements the stable model semantics for normal logic programs. It handles a subclass of programs which contain no function symbols and are domain-restricted but supports extensions including built-in functions as well as cardinality and weight constraints. On top of this core engine more involved systems can be built. As an example, we have implemented total and partial stable model computation for disjunctive logic programs. An interesting application method is based on answer set programming, i.e., encoding an application problem as a set of rules so that its solutions are captured by the stable models of the rules. \Smodels\ has been applied to a number of areas including planning, model checking, reachability analysis, product configuration, dynamic constraint satisfaction, and feature interaction.
nss-sd-nmr2000.tex
\documentclass{article}

\usepackage{aaai}

\copyrighttext{}

\newcommand{\Smodels}{\textsc{Smodels}}
\newcommand{\smodels}{\mbox{{\tt smodels}}}
\newcommand{\lparse}{\mbox{{\tt lparse}}}


\begin{document}

\title{\Smodels: A System for Answer Set Programming\thanks{%
The work has been funded by the Academy of Finland
(Project 43963) and by 
Helsinki Graduate School in Computer Science and Engineering. 
}} 

\author{Ilkka Niemel\"a \and Patrik Simons \and Tommi Syrj\"anen \\
Helsinki University of Technology \\ 
Dept.\ of Computer Science and Eng. \\
Laboratory for Theoretical Computer Science, \\
P.O.Box 5400, FIN-02015 HUT, Finland \\
\{Ilkka.Niemela, Patrik.Simons, Tommi.Syrjanen\}\@hut.fi
}

            
\maketitle

\begin{abstract}
\noindent The \Smodels\ system implements the stable model semantics for normal
logic programs. It handles a subclass of programs which contain no
function symbols and are domain-restricted but supports extensions including 
built-in functions as well as cardinality and weight
constraints. 
On top of this core engine  more involved systems can be built. As an
example, we have implemented total and partial stable model computation for
disjunctive logic programs.
An interesting application method is based on answer set programming, i.e.,
encoding an application problem as a set of rules so that its solutions
are captured by the stable models of the rules. 
\Smodels\ has been applied to a number of areas including 
planning, model checking, reachability analysis, 
product configuration, dynamic constraint satisfaction, and feature
interaction.
\end{abstract}


\section{General Information}

% MANDATORY
% 1. On what platforms (e.g., PC, SPARC, ...) does your system work? 
% 2. In what language has it been written? 
% 3. How big is the program? 

The \Smodels\ system is written in C++ and the source code, test cases
and documentation are available at
\texttt{http://www.tcs.hut.fi/Software/smodels/}. In order to compile the system
a C++ compiler is needed as well as other standard tools such
as make, tar, bison, and perl. The system has been developed under Linux and should
work as is on any platform having the appropriate GNU tools installed.
It has been used on a wide range of hardware (PC/SPARC/Alpha) mostly
running Unix.
The total number of lines of codes is about 20000.


\section{Description of the System} 

The \Smodels\ system implements the stable model semantics for normal
logic programs extended by built-in functions as well as cardinality
and weight constraints for domain-restricted programs. In this section
we briefly discuss the syntax, implementation techniques and use of
the system. More information can be found at the home page
\texttt{http://www.tcs.hut.fi/Software/smodels/}.

As input the \Smodels\ system takes logic program rules basically in 
Prolog style syntax:
\begin{verbatim}
    ancestor(X,Y) :- ancestor(X,Z), 
                     parent(Z,Y),  
                     person(X). 
    ancestor(X,Y) :- parent(X,Y). 
    son(X,Y) :- parent(Y,X), male(X). 
    daughter(X,Y) :- parent(Y,X), female(X). 
    person(X) :- male(X). 
    person(X) :- female(X). 
    parent(jack, jill). parent(joan, jack). 
    male(jack). female(jill). female(joan). 
\end{verbatim}

However, in order to support efficient implementation techniques and
extensions the programs are required to be \emph{domain-restricted}
where the idea is the following. No proper function symbols are
allowed (but we do allow built-in functions) and the predicate symbols
in the program are divided into two classes, \emph{domain predicates}
and \emph{non-domain predicates}. 
Domain predicates are predicates that are defined
non-recursively. In the program above all predicates except
\verb+ancestor+ are domain predicates. The predicate \verb+ancestor+
is not a domain predicate because it depends recursively on itself. 

The main intuition of domain predicates is that they are used to define 
the set of terms over which the variables range in each rule of a program $P$.
All rules of $P$ have to be domain-restricted in the sense that every
variable in a rule must appear in a domain predicate which appears
positively in the rule body. For instance, in the first rule of the program
above all variables appear in domain predicates \verb+parent+ and
\verb+person+ in the body of the rule.

In addition to normal logic program rules, \Smodels\  supports rules with
cardinality and weight constraints. 
The idea is that, e.g.,  a cardinality constraint
\[
\verb+1 { a,b,not c } 2+
\]
holds in a stable model if at the least 1 but at most 2 of the literals
%$a,b,not\ c$
in the constraint are satisfied in the model and a weight constraint
\[
\verb+ 10 [ a=10, b=10, not c=10 ] 20+
\]
holds if the sum of weights of the literals satisfied in the model is
between 10 and 20 (inclusive).
With built-in functions for integer arithmetic (included in the
system), these kinds of rules allow compact and fairly straightforward
encodings of many interesting problems. For example, the N queens
problem can be captured using rules as a program \verb+queens.lp+ as follows:
\begin{verbatim}
    1 { q(X,Y):d(X) } 1 :- d(Y).
    1 { q(X,Y):d(Y) } 1 :- d(X).
    :- d(X), d(Y), d(X1), d(Y1),
       q(X,Y), q(X1,Y1),
       X != X1,  Y != Y1, 
       abs(X - X1) == abs(Y - Y1).
    d(1..n).
\end{verbatim}
where \verb+d(1..n)+ is a domain predicate giving the dimension of the
board (from 1 to integer $n$ which can be specified during run time). 
The first rule says that for each row $y$, a stable model contains
exactly one atom $q(x,y)$ where for $x$, $d(x)$ holds and similarly
in the second rule for all columns.
The third rule is an integrity constraint saying that there cannot be
two queens on the same diagonal.
Now each stable model corresponds to a legal configuration of $n$ queens
on a $n\times n$ board, i.e., $q(x,y)$ is in a stable 
model iff $(x,y)$ is a legal position for a queen.


Stable models of a domain-restricted logic program with variables are
computed in three stages. First, the program is transformed into
a ground program without variables. Second, the rules of the
ground program are translated into primitive rules, and third, a
stable model is computed using a Davis-Putnam like
procedure~\cite{Simons99:lpnmr}. The first two stages have been implemented
in the program \lparse, which functions as a front end
to \smodels\ which in turn implements the third stage.

In the first stage \lparse\ automatically determines the domain
predicates and then using database techniques evaluates the domain
predicates and creates a ground program which has exactly the same
stable models as the original program with variables. 
Then the rules are compiled into primitive rules~\cite{NSS99:lpnmr}.

The \smodels\ procedure is a Davis-Putnam like backtracking search procedure
that finds the stable models of a set of primitive rules by assigning truth values to
the atoms of the program. Moreover, it uses the properties of the
stable model semantics to infer and propagate additional truth
values. Since the procedure is in effect traversing a binary search
tree, the number of nodes in the search space is in the worst case on
the order of $2^n$, where $n$ can be taken to be the number of atoms
that appear in a constraint in a head of a rule or that appear as a
negative literal in a recursive loop of the program.

Hence, in order to compute stable models, one uses the two programs
\lparse, which translates logic
programs into an internal format, and \smodels, which
computes the models, see 
Figure~\ref{fig:architecture}. 

\begin{figure*}
\setlength{\unitlength}{1mm}
\center
\begin{picture}(100,15)(0,0)
\put(0,10){\vector(1,0){15}}
\put(7.5,12){\makebox(0,0)[b]{\shortstack{domain-\\ restricted}}}
\put(7.5,8){\makebox(0,0)[t]{\shortstack{logic\\ program}}}
\put(20,5){\framebox(15,10){\lparse}}
\put(40,10){\vector(1,0){15}}
\put(47.5,12){\makebox(0,0)[b]{internal}}
\put(47.5,8){\makebox(0,0)[t]{representation}}
\put(60,5){\framebox(15,10){\smodels}}
\put(80,10){\vector(1,0){15}}
\put(87.5,12){\makebox(0,0)[b]{stable}}
\put(87.5,8){\makebox(0,0)[t]{models}}
\end{picture}
\caption{Overall Architecture}\label{fig:architecture}
\end{figure*}

For instance, a solution to the 8 queens problem given the program 
\verb+queens.lp+ above, would be typically computed by a command line:
\begin{verbatim}
lparse -c n=8 -d none queens.lp | smodels
\end{verbatim}
where \verb+-c n=8+ option instructs to use the value 8 for the constant $n$
and \verb+-d none+ option instructs to remove all domain predicates from
the rules as soon as they have been evaluated. The command line produces output:
\begin{verbatim}
Answer: 1
Stable Model: q(4,1) q(2,2) q(7,3) q(5,4) 
q(1,5) q(8,6) q(6,7) q(3,8) 
\end{verbatim}

\subsection{A Further Example}

The graph coloring problem may be encoded to a program
\verb+ncolor.lp+ using the following two \Smodels\ rules:
\begin{verbatim}
  1 { col(N, C) : color(C) } 1 :- node(N).
  :- col(X, C), col(Y,C), edge(X,Y), color(C).
\end{verbatim}
Here the predicate \verb+col(N,C)+ denotes that the color of the node
\verb+N+ is \verb+C+. The first rule states that each node has exactly
one color and the second rule states that two adjacent nodes may not
have the same color. Suppose we have a fully connected three node
graph and we want to find all 3-colorings of it where the first node is
colored red. We can encode the problem instance to a program
\verb+graph.lp+:
\begin{verbatim}
  node(a ; b; c).
  edge(a,b). edge(a,c). edge(b,c).
  color(red ; green ; blue).
  compute { col(a, red) }.
\end{verbatim}
The first two lines define the graph and the third line defines the
three colors. The \verb+compute+ statement tells \Smodels\ that we are
interested only in those models where \verb+col(a, red)+ is true, i.e., the node \verb+a+ has color \verb+red+. We can find all stable
models that satisfy the compute statement with the command line:
\begin{verbatim}
lparse -d none ncolor.lp graph.lp | smodels 0
\end{verbatim}
This input produces the output:
\begin{verbatim}
Answer: 1
Stable Model: col(c,blue) col(b,green)
col(a,red) 
Answer: 2
Stable Model: col(c,green) col(b,blue)
col(a,red) 
\end{verbatim}

More information about the syntax and use of the system can be found in
the \lparse\ user's manual at
\texttt{http://www.tcs.hut.fi/Software/smodels/lparse/} and about the 
implementation in~\cite{Simons99:lpnmr,NSS99:lpnmr}.



\section{Applying the System}

% MANDATORY

\subsection{Methodology}

% 1. Is there a general methodology as to how to encode a problem,
%    to take advantage of your work? 

An interesting application methodology for \Smodels\ is based on answer set
programming~\cite{MT99:slp,Niemela99:amai} which has emerged as a viable
approach to declarative logic-based knowledge representation.  It is
based on the stable model semantics of logic programs and can be seen as
a novel form of constraint programming where constraints are expressed
as rules.  The underlying idea is to encode an application problem using
logic program rules so that the solutions to the problem are captured by
the stable models of the rules. The solution of the N queens problem in
the previous section illustrates nicely main ideas of answer set
programming.


% 2. If there is no general methodology, is it likely to be developed in
%    the near future? 


\subsection{Specifics}

                                        
% 1. What is the significance of your system being logic-based? 
% 2. What is the semantics of your system (e.g. propositional logic,
%    first-order logic, default logic, stable or well-founded semantics, etc.)? 
% 3. Why is this an important feature of your work? 
% 4. How will your work influence other areas such as artificial
%    intelligence,  knowledge bases and deductive databases? 

It is important that the system is based on an
implementation-independent declarative semantics. This makes it much
easier to develop applications because one does not have to worry too
much about the internal implementation-specific aspects of the system.
Hence, the system is relatively easy to learn to use. On the other
hand, declarative semantics provides much more flexibility in
developing implementation approaches and in optimizing different parts
of the implementation. We have taken advantage of this and developed
methods which are substantially different from usual implementation
methods for logic programming (Prolog) but still work efficiently in
new kinds of applications where Prolog style systems are not
appropriate.

\Smodels\ implements the stable model semantics for range-restricted
function free normal programs. It can also compute well-founded models
for these programs.
%
\Smodels\ supports built-in functions, e.g.,
for integer arithmetic. Basic \Smodels\ extends normal logic programs
with cardinality and weight
constraints~\cite{Simons99:lpnmr,NSS99:lpnmr}. On top of this core engine
 more involved systems can be built. As an example, we have implemented
total and partial stable model computation for disjunctive logic
programs~\cite{JNSY2000:kr}. 


The semantics for logic programs with cardinality and weight constraints
supported by the core engine is an interesting compromise: it is rather
simple to learn, its complexity stays in NP in the ground case (like for
propositional logic) but it seems strictly more expressive than
propositional logic (or other standard constraint satisfaction
formalisms).

With our work on \Smodels\ we hope to demonstrate that nonmonotonic
reasoning techniques are useful conceptual tools as well as bring
computational advantages which can lead to new interesting applications
and to developments of novel implementation techniques and tools.


\subsection{Users and Usability} 
% 1. Must the potential user be an expert in logic or need to have a 
%    deep knowledge of the specific area of the application?
% 2. Is your system sufficiently flexible to handle other problems? 
% 2. If so, what kind of problems, and what would have to be done
%    to apply your system? 
% 3. Is your system applied outside your research group or even in other areas? 
% 4. Is it likely to be used in the future (are there concrete plans to do so)? 
The basic semantics of \Smodels\ rules seems to be simple
enough that it can be explained to a non-expert or a student in a
relatively short amount of time sufficiently so that one can start using
\Smodels. 

\Smodels\ has been employed in a number of areas including 
planning~\cite{DNK97,Niemela99:amai,Lifschitz99:iclp}, 
model checking~\cite{LRS98:tacas}, reachability 
analysis~\cite{Heljanko99:tacas,Heljanko:Fundamenta99}, 
product configuration~\cite{SN99:padl,Syrjanen99:dtyo}, 
dynamic constraint satisfaction~\cite{SNG99:cp}, feature
interaction~\cite{AAR99}, and logical cryptanalysis~\cite{HMN2000:nmr}.

In order to make \Smodels\ more flexible an API has been added to
\lparse\ and \smodels. Hence, they can be used through the
API and embedded into a C/C++ program as 
libraries. Furthermore, it is possible to define new built-in functions
for the front-end \lparse\ in order to accommodate new applications.
These new functions are written in C/C++ and they are dynamically
linked to \lparse\ when needed. 

As a further usability feature, \lparse\ performs simple analysis of
the program and warns about constructs that are often erroneous. For
example, \lparse\ detects if a variable is accidentally mistyped as a
constant or vice versa. These warnings can be enabled with command
line options.

\section{Evaluating the System}

% MANDATORY

\subsection{Benchmarks}
% 1. How can users evaluate comparative systems?
% 2. For example, are there accepted benchmarks for testing your 
%    system and comparing it to others? 
% 3. How user friendly is the system? 
% 4. What are important features for such systems? 

We have compiled quite a large collection of families of benchmarks that
we use to evaluate new developments and improvements in our system and
which we can employ to compare our system to other competing ones 
and which can be used also by others
(see, \texttt{http://www.tcs.hut.fi/Software/smodels/tests/}).
Similar testing methodology (e.g., generating test
cases from graph problems) has also been used by the groups in Kentucky
(DeReS/TheoryBase system~\cite{CMMT99:aij})  and in
Vienna  (dlv system~\cite{ELMPS98}). 
These kinds of tests can be used for measuring the base level
performance and to compare different systems. 
However, it is unclear what is a portable way of representing such
benchmarks. We use Prolog style syntax which is quite generally
accepted but it seems that each system has its specialties. 

%We have not been developing a nice graphical user interface to our
%system but use a text-based (Prolog syntax) language to give the
%programs.


\subsection{Comparison} 
% 1. Can your system compete with other special-purpose, 
%    possibly non logic-based systems? 
% 2. If yes, how exactly would you be able to compare it to such systems? 
% 3. Are there generally accepted benchmarks for these areas? 

\Smodels\ can already compete with special purpose systems and 
we have even cases where it outperforms commercial top edge tools, e.g., 
in a verification application it has performance better than that of 
one of the most efficient commercial integer programming tools (CPLEX)
%see the mcsmodels tool (http://www.tcs.hut.fi/~kepa/tools/)
\cite{Heljanko:Fundamenta99}.


\subsection{Problem Size} 
% 1. What is the current problem size your system can handle? 
% 2. Is your system a prototype, or do you believe it
%    can be used on problems of realistic size? 
% 3. Assuming your system is a prototype, what has to be done to 
%    assure that it scales to large-sized problems? 

We believe that \Smodels\ is no longer a mere prototype but it can
handle realistic size problems. We have applications where 
programs with hundreds of thousands of non-trivial ground rules are
treated efficiently, see e.g.~\cite{Niemela99:amai,Heljanko:Fundamenta99}. 

%\bibliography{/home/ini/bib/ini,/home/ini/bib/nmr,/home/ini/bib/smodels}
%\bibliographystyle{aaai}

%input the bbl file

\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Accorsi, Areces, \& de Rijke}{1999}]{AAR99}
Accorsi, R.; Areces, C.; and de~Rijke, M.
\newblock 1999.
\newblock Towards feature interaction via stable models.
\newblock In {\em Proceedings of the Second Workshop on Formal Methods}.

\bibitem[\protect\citeauthoryear{Cholewi\'{n}ski \bgroup \em et al.\egroup
  }{1999}]{CMMT99:aij}
Cholewi\'{n}ski, P.; Marek, V.; Mikitiuk, A.; and Truszczy\'{n}ski, M.
\newblock 1999.
\newblock Computing with default logic.
\newblock {\em Artificial Intelligence} 112:105--146.

\bibitem[\protect\citeauthoryear{Dimopoulos, Nebel, \& Koehler}{1997}]{DNK97}
Dimopoulos, Y.; Nebel, B.; and Koehler, J.
\newblock 1997.
\newblock Encoding planning problems in non-monotonic logic programs.
\newblock In {\em Proceedings of the Fourth European Conference on Planning},
  169--181.
\newblock Toulouse, France: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Eiter \bgroup \em et al.\egroup
  }{1998}]{ELMPS98}
Eiter, T.; Leone, N.; Mateis, C.; Pfeifer, G.; and Scarnello, F.
\newblock 1998.
\newblock The {KR} system {dlv}: Progress report, comparisons and benchmarks.
\newblock In {\em Proceedings of the 6th International Conference on Principles
  of Knowledge Representation and Reasoning},  406--417.
\newblock Trento, Italy: Morgan Kaufmann Publishers.

\bibitem[\protect\citeauthoryear{Heljanko}{1999a}]{Heljanko99:tacas}
Heljanko, K.
\newblock 1999a.
\newblock Using logic programs with stable model semantics to solve deadlock
  and reachability problems for 1-safe {Petri} nets.
\newblock In {\em Proceedings of the 5th International Conference on Tools and
  Algorithms for the Construction and Analysis of Systems},  240--254.
\newblock Amsterdam, the Netherlands: Sprin\-ger-Ver\-lag.

\bibitem[\protect\citeauthoryear{Heljanko}{1999b}]{Heljanko:Fundamenta99}
Heljanko, K.
\newblock 1999b.
\newblock Using logic programs with stable model semantics to solve deadlock
  and reachability problems for 1-safe {Petri} nets.
\newblock {\em Fundamenta Informaticae} 37(3):247--268.

\bibitem[\protect\citeauthoryear{Hietalahti, Massacci, \&
  Niemel\"a}{2000}]{HMN2000:nmr}
Hietalahti, M.; Massacci, F.; and Niemel\"a, I.
\newblock 2000.
\newblock {DES}: a challenge problem for nonmonotonic reasoning systems.
\newblock In {\em Proceedings of the 8th International Workshop on
  Non-Monotonic Reasoning}.
\newblock Accepted for publication.

\bibitem[\protect\citeauthoryear{Janhunen \bgroup \em et al.\egroup
  }{2000}]{JNSY2000:kr}
Janhunen, T.; Niemel\"a, I.; Simons, P.; and You, J.
\newblock 2000.
\newblock Unfolding partiality and disjunctions in stable model semantics.
\newblock In Cohn, A.; Guinchiglia, F.; and Selman, B., eds., {\em Proceedings
  of the Seventh International Conference on Principles of Knowledge
  Representation and Reasoning}.
\newblock Breckenridge, Colorado, USA: Morgan Kaufmann Publishers.
\newblock Accepted for publication.

\bibitem[\protect\citeauthoryear{Lifschitz}{1999}]{Lifschitz99:iclp}
Lifschitz, V.
\newblock 1999.
\newblock Answer set planning.
\newblock In {\em Proceedings of the 16th International Conference on Logic
  Programming},  25--37.
\newblock Las Cruces, New Mexico: The MIT Press.

\bibitem[\protect\citeauthoryear{Liu, Ramakrishnan, \&
  Smolka}{1998}]{LRS98:tacas}
Liu, X.; Ramakrishnan, C.; and Smolka, S.~A.
\newblock 1998.
\newblock Fully local and efficient evaluation of alternating fixed points.
\newblock In Steffen, B., ed., {\em Proceedings of the 4th International
  Conference on Tools and Algorithms for the Construction and Analysis of
  Systems},  5--19.
\newblock Lisbon, Portugal: Sprin\-ger-Ver\-lag.

\bibitem[\protect\citeauthoryear{Marek \& Truszczy\'{n}ski}{1999}]{MT99:slp}
Marek, W., and Truszczy\'{n}ski, M.
\newblock 1999.
\newblock Stable models and an alternative logic programming paradigm.
\newblock In {\em The Logic Programming Paradigm: a 25-Year Perspective}.
  Sprin\-ger-Ver\-lag.
\newblock  375--398.

\bibitem[\protect\citeauthoryear{Niemel\"a, Simons, \&
  Soininen}{1999}]{NSS99:lpnmr}
Niemel\"a, I.; Simons, P.; and Soininen, T.
\newblock 1999.
\newblock Stable model semantics of weight constraint rules.
\newblock In {\em Proceedings of the 5th International Conference on Logic
  Programming and Nonmonotonic Reasoning},  317--331.
\newblock El Paso, Texas, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Niemel\"a}{1999}]{Niemela99:amai}
Niemel\"a, I.
\newblock 1999.
\newblock Logic programming with stable model semantics as a constraint
  programming paradigm.
\newblock {\em Annals of Mathematics and Artificial Intelligence}
  25(3,4):241--273.

\bibitem[\protect\citeauthoryear{Simons}{1999}]{Simons99:lpnmr}
Simons, P.
\newblock 1999.
\newblock Extending the stable model semantics with more expressive rules.
\newblock In {\em Proceedings of the 5th International Conference on Logic
  Programming and Nonmonotonic Reasoning},  305--316.
\newblock El Paso, Texas, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Soininen \& Niemel\"a}{1999}]{SN99:padl}
Soininen, T., and Niemel\"a, I.
\newblock 1999.
\newblock Developing a declarative rule language for applications in product
  configuration.
\newblock In Gupta, G., ed., {\em Proceedings of the First International
  Workshop on Practical Aspects of Declarative Languages},  305--319.
\newblock San Antonio, Texas: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Soininen, Niemel\"a, \&
  Gelle}{1999}]{SNG99:cp}
Soininen, T.; Niemel\"a, I.; and Gelle, E.
\newblock 1999.
\newblock A fixpoint definition of dynamic constraint satisfaction.
\newblock In Jaffar, J., ed., {\em Proceedings of the Fifth International
  Conference on Principles and Practice of Constraint Programming},  419--433.
\newblock Alexandria, Virginia, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Syrj\"anen}{1999}]{Syrjanen99:dtyo}
Syrj\"anen, T.
\newblock 1999.
\newblock A rule-based formal model for software configuration.
\newblock Research report A55, Helsinki University of Technology, Laboratory
  for Theoretical Computer Science, Helsinki, Finland.

\end{thebibliography}


\end{document}


cs0003033.extracted_bib
\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Accorsi, Areces, \& de Rijke}{1999}]{AAR99}
Accorsi, R.; Areces, C.; and de~Rijke, M.
\newblock 1999.
\newblock Towards feature interaction via stable models.
\newblock In {\em Proceedings of the Second Workshop on Formal Methods}.

\bibitem[\protect\citeauthoryear{Cholewi\'{n}ski \bgroup \em et al.\egroup
  }{1999}]{CMMT99:aij}
Cholewi\'{n}ski, P.; Marek, V.; Mikitiuk, A.; and Truszczy\'{n}ski, M.
\newblock 1999.
\newblock Computing with default logic.
\newblock {\em Artificial Intelligence} 112:105--146.

\bibitem[\protect\citeauthoryear{Dimopoulos, Nebel, \& Koehler}{1997}]{DNK97}
Dimopoulos, Y.; Nebel, B.; and Koehler, J.
\newblock 1997.
\newblock Encoding planning problems in non-monotonic logic programs.
\newblock In {\em Proceedings of the Fourth European Conference on Planning},
  169--181.
\newblock Toulouse, France: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Eiter \bgroup \em et al.\egroup
  }{1998}]{ELMPS98}
Eiter, T.; Leone, N.; Mateis, C.; Pfeifer, G.; and Scarnello, F.
\newblock 1998.
\newblock The {KR} system {dlv}: Progress report, comparisons and benchmarks.
\newblock In {\em Proceedings of the 6th International Conference on Principles
  of Knowledge Representation and Reasoning},  406--417.
\newblock Trento, Italy: Morgan Kaufmann Publishers.

\bibitem[\protect\citeauthoryear{Heljanko}{1999a}]{Heljanko99:tacas}
Heljanko, K.
\newblock 1999a.
\newblock Using logic programs with stable model semantics to solve deadlock
  and reachability problems for 1-safe {Petri} nets.
\newblock In {\em Proceedings of the 5th International Conference on Tools and
  Algorithms for the Construction and Analysis of Systems},  240--254.
\newblock Amsterdam, the Netherlands: Sprin\-ger-Ver\-lag.

\bibitem[\protect\citeauthoryear{Heljanko}{1999b}]{Heljanko:Fundamenta99}
Heljanko, K.
\newblock 1999b.
\newblock Using logic programs with stable model semantics to solve deadlock
  and reachability problems for 1-safe {Petri} nets.
\newblock {\em Fundamenta Informaticae} 37(3):247--268.

\bibitem[\protect\citeauthoryear{Hietalahti, Massacci, \&
  Niemel\"a}{2000}]{HMN2000:nmr}
Hietalahti, M.; Massacci, F.; and Niemel\"a, I.
\newblock 2000.
\newblock {DES}: a challenge problem for nonmonotonic reasoning systems.
\newblock In {\em Proceedings of the 8th International Workshop on
  Non-Monotonic Reasoning}.
\newblock Accepted for publication.

\bibitem[\protect\citeauthoryear{Janhunen \bgroup \em et al.\egroup
  }{2000}]{JNSY2000:kr}
Janhunen, T.; Niemel\"a, I.; Simons, P.; and You, J.
\newblock 2000.
\newblock Unfolding partiality and disjunctions in stable model semantics.
\newblock In Cohn, A.; Guinchiglia, F.; and Selman, B., eds., {\em Proceedings
  of the Seventh International Conference on Principles of Knowledge
  Representation and Reasoning}.
\newblock Breckenridge, Colorado, USA: Morgan Kaufmann Publishers.
\newblock Accepted for publication.

\bibitem[\protect\citeauthoryear{Lifschitz}{1999}]{Lifschitz99:iclp}
Lifschitz, V.
\newblock 1999.
\newblock Answer set planning.
\newblock In {\em Proceedings of the 16th International Conference on Logic
  Programming},  25--37.
\newblock Las Cruces, New Mexico: The MIT Press.

\bibitem[\protect\citeauthoryear{Liu, Ramakrishnan, \&
  Smolka}{1998}]{LRS98:tacas}
Liu, X.; Ramakrishnan, C.; and Smolka, S.~A.
\newblock 1998.
\newblock Fully local and efficient evaluation of alternating fixed points.
\newblock In Steffen, B., ed., {\em Proceedings of the 4th International
  Conference on Tools and Algorithms for the Construction and Analysis of
  Systems},  5--19.
\newblock Lisbon, Portugal: Sprin\-ger-Ver\-lag.

\bibitem[\protect\citeauthoryear{Marek \& Truszczy\'{n}ski}{1999}]{MT99:slp}
Marek, W., and Truszczy\'{n}ski, M.
\newblock 1999.
\newblock Stable models and an alternative logic programming paradigm.
\newblock In {\em The Logic Programming Paradigm: a 25-Year Perspective}.
  Sprin\-ger-Ver\-lag.
\newblock  375--398.

\bibitem[\protect\citeauthoryear{Niemel\"a, Simons, \&
  Soininen}{1999}]{NSS99:lpnmr}
Niemel\"a, I.; Simons, P.; and Soininen, T.
\newblock 1999.
\newblock Stable model semantics of weight constraint rules.
\newblock In {\em Proceedings of the 5th International Conference on Logic
  Programming and Nonmonotonic Reasoning},  317--331.
\newblock El Paso, Texas, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Niemel\"a}{1999}]{Niemela99:amai}
Niemel\"a, I.
\newblock 1999.
\newblock Logic programming with stable model semantics as a constraint
  programming paradigm.
\newblock {\em Annals of Mathematics and Artificial Intelligence}
  25(3,4):241--273.

\bibitem[\protect\citeauthoryear{Simons}{1999}]{Simons99:lpnmr}
Simons, P.
\newblock 1999.
\newblock Extending the stable model semantics with more expressive rules.
\newblock In {\em Proceedings of the 5th International Conference on Logic
  Programming and Nonmonotonic Reasoning},  305--316.
\newblock El Paso, Texas, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Soininen \& Niemel\"a}{1999}]{SN99:padl}
Soininen, T., and Niemel\"a, I.
\newblock 1999.
\newblock Developing a declarative rule language for applications in product
  configuration.
\newblock In Gupta, G., ed., {\em Proceedings of the First International
  Workshop on Practical Aspects of Declarative Languages},  305--319.
\newblock San Antonio, Texas: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Soininen, Niemel\"a, \&
  Gelle}{1999}]{SNG99:cp}
Soininen, T.; Niemel\"a, I.; and Gelle, E.
\newblock 1999.
\newblock A fixpoint definition of dynamic constraint satisfaction.
\newblock In Jaffar, J., ed., {\em Proceedings of the Fifth International
  Conference on Principles and Practice of Constraint Programming},  419--433.
\newblock Alexandria, Virginia, USA: Springer-Verlag.

\bibitem[\protect\citeauthoryear{Syrj\"anen}{1999}]{Syrjanen99:dtyo}
Syrj\"anen, T.
\newblock 1999.
\newblock A rule-based formal model for software configuration.
\newblock Research report A55, Helsinki University of Technology, Laboratory
  for Theoretical Computer Science, Helsinki, Finland.

\end{thebibliography}