% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            threesat.dtr                                             %
% Purpose:         linear translation of 3SAT problems into DATR theories   %
% Authors:         Gerald Gazdar & Roger Evans, 1 September 1991            %
% Email:           geraldg@cogs.sussex.ac.uk, Roger.Evans@itri.bton.ac.uk   %
% Address:         COGS, Sussex University, Brighton BN1 9QH, UK            %
%                  ITRI, Univ. Brighton, Lewes Road, Brighton BN2 4GJ, UK   %
% Related files:   boolean2.dtr, quantifi.dtr                               %
% Version:         1.01                                                     %
%      Copyright (c) University of Sussex 1991.  All rights reserved.       %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% 3SAT is the name given to the problem of deciding whether a sentence in the
% following format is satisfiable:

%       (x1 v y1 v z1) & (x2 v y2 v z2) & (x3 v y3 v z3) ..

% where x1 .. zn represent literals (i.e., a propositional constant or the
% negation of a propositional constant).

% To encode such problems in DATR we need definitions for negation,
% conjunction and disjunction.  It will be convenient to define the latter as
% n-ary connectives.

Not:    <0> == 1
        <1> == 0.

And:    <>  == 1
        <0> == 0
        <1> == <>.

Or:     <>  == 0
        <1> == 1
        <0> == <>.

% For a given 3SAT problem involving n distinct propositional constants, we
% need to define 2^n different "worlds" (assignments of true or false to
% propositional constants).  We will restrict ourselves here to problems that
% only involve 3 distinct propositional constants, a, b and c.

W0:     <>  == Tests
        <a> == 0
        <b> == 0
        <c> == 0.

W1:     <>  == W0             <a> == 1.
W2:     <>  == W0             <b> == 1.
W3:     <>  == W1             <b> == 1.
W4:     <>  == W0             <c> == 1.
W5:     <>  == W1             <c> == 1.
W6:     <>  == W2             <c> == 1.
W7:     <>  == W3             <c> == 1.

% A (3 constant) sentence is satisfiable if and only if it true in one or more
% of these worlds.

Satisfiable:
        <>  == Or:<"W0" "W1" "W2" "W3" "W4" "W5" "W6" "W7">.

% Finally, some test examples:

Tests:  <x> == And:<Or:<"<a>" Not:<"<b>"> Not:<"<c>">>
                    Or:<Not:<"<a>"> "<b>" Not:<"<c>">>
                    Or:<Not:<"<a>"> Not:<"<b>"> "<c>">>

        <y> == And:<Or:<"<a>" "<b>" "<c>">
                    Or:<Not:<"<a>"> "<b>" Not:<"<c>">>
                    Or:<Not:<"<a>"> Not:<"<b>"> Not:<"<c>">>>

        <z> == And:<Or:<"<a>" "<a>" "<a>">
                    Or:<Not:<"<a>"> "<b>" Not:<"<c>">>
                    Or:<Not:<"<a>"> Not:<"<a>"> Not:<"<a>">>>.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# hide  Not And Or Tests W0 W1 W2 W3 W4 W5 W6 W7.

# show  <x> <y> <z>.

% The next line is the Revision Control System Id: do not delete it.
% $Id: archive.dtr,v 1.1 1997/04/09 20:40:33 root Exp $