GnT (Generate'n'Test): A Solver for Disjunctive Logic Programs

GnT is an experimental implementation of the stable model semantics for disjunctive logic programs [Gelfond and Lifschitz, 1991]. Our implementation is based on an architecture consisting of two interacting smodels solvers for non-disjunctive programs. One of the them is responsible for generating as good as possible model candidates while the other checks for minimality, as required from disjuctive stable models. Please see [Janhunen et al., 2006] for details.

This program is to be compiled under the smodels (versions 2.*) source distribution; and it is to be used with the front-end lparse.

Using the Software

• Disjunctive rules are written in the following syntax:
  a1|a2|a2 :- b1, b2, b3, not c1, not c2, not c3.

• Also rules with variables can be used, but the front-end lparse performs an instantation for the rules using domain predicates like d(.) below:
  a(X)|b(X)|c(X) :- d(X). d(1..10).

• Parametrized disjunctions (lparse versions 1.0.14 and later) in the heads of rules are also supported:
  |a(X):d(X)|. d(1..4).

• The stable models of a disjunctive logic program can be computed by giving a command line like
  lparse --dlp disjunctive-program.lp | gnt2 0
  If the command line argument 0 is replaced by a positive integer n, then the first n stable models are to be computed (if so many stable models exist).
• Even partial stable models can be computed by giving the the command line option --partial for lparse.
• Similarly, regular models can be computed by giving the command line option -r for lparse.

Version Information

The author of the first version of GnT (also included as example4.cc in the smodels source distribution) is Patrik Simons. The version GnT1 (given below) is basically the orginal one -- only few lines of code have been added to handle command line options. The second version (GnT2.* below), which is a derivative of the first one, was developed by Tomi Janhunen to speed up computation.

Terms and Conditions

This software is distributed under the GNU General Public License (available from Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA). In particular, as stated in the licence agreement, the software is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Download

Source code: files for GnT1 (the first version) and GnT2 (version 2.1) -- to be placed and compiled (Makefile) in a subdirectory of the smodels source directory (such as examples therein). Inline functions may cause problems with some compilers (g++ series 3.* and 4.*). This problem is fixed in the smodels 2.32 distribution.

Related Publications

T. Janhunen, I. Niemelä, D. Seipel, P. Simons, and J.-H. You. Unfolding Partiality and Disjunctions in Stable Model Semantics. ACM Transactions on Computational Logic, 7(1), 1-37, January 2006. (Also in Proc. of KR 2000, 411-419).

M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9 (1991), 365-385.

J. You and L. Yuan. A three-valued semantics for deductive databases and logic programs. Journal of Computer Systems and Sciences, 49 (1994), 334--361.