% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            satisfy.dtr                                              %
% Purpose:         Boolean satisfiability                                   %
%                  with an unlimited supply of propositional variables      %
% Author:          Lionel Moser, January 1992.                              %
% Email:           moser@bnr.ca                                             %
% Documentation:   Cognitive Science Research Paper CSRP 240, Univ. Sussex  %
% Related files:   arglists.dtr, arglogic.dtr                               %
% Version:         1.10                                                     %
%                                                                           %
%      Copyright (c) University of Sussex 1992.  All rights reserved.       %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# load 'arglists.dtr'.    % tools for argument manipulation.
# load 'arglogic.dtr'.    % simple logic

% Moser, Lionel, "Evaluation in DATR is co-NP-hard," Cognitive
%   Science Research Paper CSRP 240, University of Sussex,
%   Brighton, 1992.
% 
%   A lower bound of co-NP for the time complexity of DATR query
%   evaluation is established by showing that an NP-complete
%   language can be recognized in DATR, and that its complement
%   can be as well. An upper bound of co-NP is established as
%   well, thus showing that the complexity of DATR query
%   evaluation is co-NP.
%
% This theory recognises membership in boolean formulas in the set of
% satisfiable formulas. Variables are represented as sequences over alphabet
% 0, ..., 9, enclosed in square brackets, and the formula must be in
% postfix notation. e.g.,
% formula (v13 & v12) would be represented by <[ 1 3 ] [ 1 2 ] &>.
% The variables are simply distinct sequences, not arithmetic values.
% This provides the unlimited supply of variables.
%
% Assignment functions do not assign values to operators, only
% variables. Thus (0 0 0) would be an assignment function for
% formula ([ 3 ] ~ [ 2 ] ~ [ 3 ] &). An assignment function is `valid'
% if it assigns each variable uniquely.
%
%  The formulas and assignment functions look like this:
%
%         wff     <[ 1 2 ] [ 3 2 ] & [ 3 4 ] [ 3 2 ] ~ & |>
%         assn_fn <      0       1         0       1>  valid
%         assn_fn <      0       0         0       1>  invalid: [ 3 2 ]
%                                                      is not uniquely mapped
%
% An assignment function satisfies a formula if it is valid and the formula
% under that substitution evaluates to 1, which we check be evaluating it
% on the stack evaluator.

% terminals are the alphabet we use:
%     a          - used for distance list
%     0,1        - boolean values
%     0-9        - alphabet for variable names
%     [ ]        - variable name delimiters
%     & | ~      - logical operators AND, OR, and NOT.

# vars $operator: & | ~.                          % logical operators.
# vars $varletter:  0 1 2 3 4 5 6 7 8 9.          % variable alphabet
# vars $terminal: a 0 1 2 3 4 5 6 7 8 9 & | ~ [ ].

# vars $!: !.
# vars $;: ;.

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

% Code to implement a stack evaluator for boolean expressions:

% Bit Logic.

AND:
    <> == '**** Error: (AND) invalid arg'
    <0 0> == 0
    <0 1> == 0
    <1 0> == 0
    <1 1> == 1.

OR:
    <> == '**** Error: (OR) invalid arg'
    <0 0> == 0
    <0 1> == 1
    <1 0> == 1
    <1 1> == 1.

NOT:
    <> == '**** Error: (NOT) invalid arg'
    <0> == 1
    <1> == 0.

% Eval:<formula ; stack ;> = 0 or 1 (false or true)
%  where
%     formula: is a boolean expression consisting of a sequence of symbols
%              over $terminal. The formula is in Reverse Polish Notation
%              (RPN). To evaluate the expression
%                 (1 & 1) | (0 | ~1)
%              the RPN formula would be
%                  1 1 & 0 1 ~ | |
%     stack:   is a stack with the bottom at right and top at left.
%              It must be initially empty.
%
% Sample theorem:
%      Eval: <1 1 & 0 1 ~ | | ; ;> = 1.

% Argument names:

Formula1:
    <> == Arg1.

Stack1:
    <> == Arg2.

Eval:
    <;> == Top:<>                                   % return top of stack.
    <1> == Eval:< Formula1:<> ; 1 Stack1:<> ; ! >   % Push 1 on stack
    <0> == Eval:< Formula1:<> ; 0 Stack1:<> ; !>    % Push 0 on stack
    <&> == Eval:< Formula1:<>                       % Push AND of top 2 items
                  ;
                  AND:< Top:<Stack1:<>>
                        Second:<Stack1:<>> >
                  Pop:< Pop:< Stack1:<> ; > ;  > ; !
                >
    <|> == Eval:< Formula1:<>                       % Push OR of top 2 items
                  ;
                  OR:< Top:<Stack1:<> ; >
                       Second:<Stack1:<> ; > >
                  Pop:<Pop:<Stack1:<> ;> ; > ; !
                >
    <~> == Eval:< Formula1:<>                       % Push NOT of top item
                  ;
                  NOT:< Top:<Stack1:<> ;> >
                  Pop:<Stack1:<> ;> ;  !
                >.

% Some example theorems:
%
% Eval:
%   <1 ; ;> = 1
%   <0 ; ;> = 0
%   <0 ~ ; ;> = 1
%   <1 0 | ; ;> = 1
%   <1 1 & 1 0 & & ; ;> = 0
%   <1 1 & 0 1 ~ & | ; ;> = 1.

% End of stack evaluator code

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

% Primitives to deal with propositional variables of the form
% [ x1 x2 x3 ... xn ]

% Variable extractor
% Varbl:<[ x1 ... xn ]> == [ x1 ... xn ].

Varbl:
    <> == '**** ERROR: (Varbl) Invalid symbol.'
    <$varletter> == $varletter <>
    <[> == [ <>
    <]> == ].

% Extract variable or operator.
% Varbl_or_op returns the first item in the list, whether it's a
% variable or operator.

Varbl_or_op:
    <> == '**** ERROR: (Varbl_or_op) Invalid symbol.'
    <[> == Varbl
    <$operator>== $operator.

% Like Rest, removes one item, which is either a variable or operator.
% Pop_varbl_or_op:<[ 1 2 3 ] & | ;> = (& |).

Pop_varbl_or_op:
    <> == '**** ERROR: (Pop_varbl_or_op) unexpected symbol'
    <[> == Pop_varbl
    <$operator> == Arg1:<>.

% Like Rest, where first `item' is a variable.
% Pop_varbl:<[ 1 2 3 ] & | ;> = (& |).

Pop_varbl: <> == '**** ERROR: (Pop_varbl) unexpected symbol'
    <[> == <>
    <$varletter> == <>
    <]> == Arg1:<>.

% Typeof returns the type of its operand, either var or op.

Typeof:
    <> == '**** ERROR: (Typeof) Invalid symbol'
    <$operator> == op
    <[> == var.

% Distance_list takes a formula and returns a sequence of a's of
% the same length; a variable has length 1.

Distance_list:
    <> == '**** ERROR: (Distance_list) Invalid symbol'
    <$operator> ==  <>
    <[ > == <scan>
    <scan $varletter> == <scan>
    <scan ]> == a <>
    <;> == .

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

% Satisfy:<Formula ;> = () or an assn_fn.

Satisfy:
    <> == Generate:<Distance_list:<Arg1 ; !> ; Arg1 ; ; ! >.

% Some theorems:
%
% Satisfy:
%   <[ 1 2 3 4 ] ~ ;> = 0
%   <[ 1 2 3 4 ] [ 1 2 3 4 ] | ;> = 1 1
%   <[ 1 2 3 4 5 ] [ 1 2 3 4 ] | ;> = 0 1
%   <[ 3 ] [ 3 ] | ;> = 1 1
%   <[ 3 ] [ 3 ] & ;> = 1 1
%   <[ 3 ] [ 3 ] ~ & ;> = 
%   <[ 3 ] [ 3 ] [ 3 ] & & ;> = 1 1 1.

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

% Generate: generates and tests possible solutions.
%
% Generate:<Length ; Formula ; Assn_fn ;> = some Assn_fn or () if none exists.
%    where
%        Length  -  <Sn Sn-1 ... S0> (Si is any terminal symbol);
%        Formula -  a wff over variables and operators;
%        Assn_fn -  a partial assignment function.
%    satisfying
%        length(Length) + length(Assn_fn) = length(Formula).

% Length is a distance list, used to measure the length (n) of the assignment
% function needed. Any sequence of terminal symbols of length n will do;
% Satisfy passes a copy of the formula itself. Generate recurses to the bottom
% left of the powerset tree, and at leaf nodes it passes the assignment
% function of length n and the formula to Test, which returns the empty list
% "()" if it is not a solution, or returns the assignment function itself if
% it is. If Test returns a non-nil list, then the assignment function
% satisfied the formula, and this is returned.  Otherwise, the right branch is
% descended.  Negative path extension is used to determine what result was
% returned from Test.

% Left branches have label zero (ie, 0 is appended to the assignment function)
% and right branches have label one (ie, 1 is appended to the assignment
% function).
%
% The initial call must provide a nil list as Assn_fn, which will be appended
% to as Generate recurses down to terminal nodes of the search tree.
%
% A simple version of this algorithm is illustrated in file `powertest.dtr'.

% Argument names: we name the arguments as this makes it easier to read the
% main node definitions. Argument names must be unique in the theory. The
% integer at the end is arbitrary (but unique).

% Generate:<Length ; Formula ; Assn_fn ;>

LengthG:
    <> == Arg1.

FormulaG:
    <> == Arg2.

Assn_fnG:
    <> == Arg3.

Left_branch_result:
    <> == Arg1.

Generate:
    <;> == % Length = nil (leaf node);
           Test:< FormulaG ; Assn_fnG ; !>
    <a > == <if Generate:<LengthG:<> ; FormulaG ; Assn_fnG 0 ; !> ;>

    <if ;> == Generate:<LengthG:<> ; FormulaG:<> ; Assn_fnG:<> 1 ; !>
    <if> == Left_branch_result:<>.

% Some theorems used in the derivation of theorem
%       Satisfy:  <[ 3 ] [ 4 ] [ 3 ] ~ & | ;> = 0 1 0.
%
%  (root)
%  Generate: <a a a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; ;> = 0 1 0
%  (descending left branch)
%            <a a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 ;> = 0 1 0
%            <a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 0 ;> = 
%            <; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 0 0 ;> =  
%  (back up)
%            <if ; ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 0 ;> = 
%  (descend right branch)
%            <; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 0 1 ;> = 
%  (back up)
%           <if ; a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 ;> = 0 1 0
%  (descend right branch)
%            <a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 ;> = 0 1 0
%  (descend left branch)
%            <; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 0 ;> = 0 1 0
%  (back up)
%            <if 0 1 0 ; ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 ;> = 0 1 0
%  (back up)
%            <if 0 1 0 ; a a ; [ 3 ] [ 4 ] [ 3 ] ~ & | ; ;> = 0 1 0

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

% Test:<Formula ; Assn_fn ;> == Assn_fn or ()
%
% Test returns nil if the assignment function is not a solution, and returns
% the assignment function if it is a solution. Test first calls Assn_fn_valid to
% determine whether the assignment function is a valid substitution (ie,
% whether it assigns the same value to each occurrence of each variable). If
% not, it returns a nil list. Otherwise, it instantiates the formula using the
% assignment function (ie, substitutes each variable with the value it is
% assigned by the assignment function), evaluates the instantiated formula on
% the stack evaluator. If this result is 0 it returns (); if it is 1 it
% returns Assn_fn.

% Test:<Formula ; Assn_fn ;> == Assn_fn or ()

% Argument names

FormulaT:
    <>==Arg1.

Assn_fnT:
    <>==Arg2.

Test:
    <> == <If:<Assn_fn_valid:<FormulaT ; Assn_fnT ; !>>>
    <then> == <result Eval:< Instantiate:<FormulaT:<> ;
                                          Assn_fnT:<> ; ; !>
                                  ; ; !
                                >
                           ;
                           Assn_fnT:<> ; !>
       <result 0> == 
       <result 1> == Assn_fnT:<>
    <else> == .

% Sample theorems:
%
% (1) Initial call
%     Test:<[ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 0 ;> = 0 1 0.
% (2) Assn_fn is valid and satisfies the formula:
%     Test:<then [ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 0 ;> = 0 1 0
%          <result 1 ; 0 1 0 ;> = 0 1 0.

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

% Instantiate:< Formula ; Assn_fn ; Inst_formula ; > == Instantiated_formula
%   where
%      Formula        - is a sequence of variables and operators
%      Assn_fn        - is a sequence of bits (same length as Formula)
%      Inst_formula   - is the part of the Formula which has already
%                       been instantiated.
%
%  Note: Inst_formula must be initially nil.
%
% Instantiate takes a formula (a sequence of variables and operators) and an
% assignment function (a binary string of the same length). It returns the
% instantiation of the formula under the assignment function. Operators, which
% have assignments, are not mapped, since when we evaluate the instantiated
% formula we won't care about the value of any operator. Inst_formula (the
% instantiated formula so far) must be initially nil.
%
% e.g., Instantiate: <v1 v2 ~ & | ; 0 1 1 1 0 ; ;> = 0 1 ~ & |.

% Instantiate:< Formula ; Assn_fn ; Inst_formula ; > == Instantiated_formula
% Instantiate:< Formula ; Assn_fn ; Inst_formula ; > == Instantiated_formula

% Argument names

FormulaI:
    <> == Arg1.

Assn_fnI:
    <> == Arg2.

Inst_formulaI:
    <> == Arg3.

Instantiate:
    <> == '**** ERROR: (Instantiate) Invalid argument'
    <; ;> == Inst_formulaI    % Formula & Assn_fn exhausted.
    <;> == '**** ERROR: (Instantiate) Assignment function too short'  % NPE

                   % Remove var from Formula and its mapping from Assn_fn,
                   % append the mapping of the var to the assn_fn, and recurse.
    <[>         == Instantiate:< Pop_varbl:<FormulaI ;> ;
                                 Rest:<Assn_fnI ;> ;
                                 Inst_formulaI First:<Assn_fnI ;> ; !
                               >
 
                   % Remove op from Formula and its mapping from Assn_fn,
                   % append the op to the assn_fn, and recurse.
    <$operator> == Instantiate:< Rest:<FormulaI ;> ;
                                 Assn_fnI ;
                                 Inst_formulaI $operator ; !
                               >.

% Sample theorems:
%
% (1) Initial call:
%     Instantiate:<[ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 0 ; ;> = 0 1 0 ~ & |.
% (2) During recursion: 
%     Instantiate:<~ & | ; ; 0 1 0 ;> = 0 1 0 ~ & |.
% (3) Recursion termination: 
%     Instantiate:<; ; 0 1 0 ~ & | ;> = 0 1 0 ~ & |.

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

% Assn_fn_valid:<Formula ; Assn_fn ;> =
%    true    -  if Assn_fn is valid;
%    false   -  if Assn_fn is invalid.
%
% An assignment function is valid if it assigns the same value to each
% occurrence of each variable in the formula, operators excepted. Operators are
% ignored. The technique is rather inefficient: Assn_fn is valid if it assigns
% the first symbol correctly and is valid on the rest of the formula. If the
% first symbol is a variable, we test its mapping in the rest of the list,
% remove the first symbol from both the assignment function and the formula,
% and recurse. So every occurrence of a variable is checked against the rest of
% the list.

% Assn_fn_valid:<Formula ; Assn_fn ;>

% Argument names

FormA:
    <> == Arg1.

Assn_fnA:
    <> == Arg2.

Assn_fn_valid:
    <> == '**** ERROR: (Assn_fn_valid) Invalid symbol'
    <; ;> == true  % Formula and Assn_fn exhausted
    <;> == true
                   % first symbol in Formula is var; check its assn for
                   % consistency
    <[> == <If:< Var_map_ok:<First:<Assn_fnA ;> ;
                             FormA ;
                             Varbl ;
                             Assn_fnA ; !
                            >
               > [ >
                   % var is prefixed to default extn so
                   % that entire formula is preserved.
    <$operator> == Assn_fn_valid:< FormA:<> ;
                                   Assn_fnA:<> ; !>
                   % ditto for operator. No consistency check.
    <then> ==      % mapping of first symbol is okay. Check rest.
              Assn_fn_valid:< Pop_varbl_or_op:<FormA:<> ;> ;
                              Rest:<Assn_fnA:<> ;> ; !>
    <else> == false.

% Sample theorems:
%
% (1) Initial call
%     Assn_fn_valid:<[ 3 ] [ 4 ] [ 3 ] ~ & | ; 0 1 0 ;> = true.
% (2) During recursion
%     Assn_fn_valid:<then [ 4 ] [ 3 ] ~ & | ; 1 0 ;> =  true.
% (3) During recursion
%     Assn_fn_valid:<~ & | ; ;> = true.
% (4) Recursion termination
%     Assn_fn_valid:<; ;> = true.

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

% Var_map_ok: <Val ; Form ; Var ; Assn_fn ;> = true/false
% where
%    Val:     is either 0 or 1
%    Form:    is the formula being tested. (eg, (v1 v1 ~ &))
%    Var:     is the name of the variable
%    Assn_fn: is as assignment function, a la Montague, i.e., assn_fn
%             is a model for the formula.
%
% Var_map_ok tests whether all occurrences of variable Var in formula Form
% are assigned the value Val by the assignment function Assn_fn.
% For example,
%   Var_map_ok: <0 ; v2 v1 v2 ; v2 ; 0 0 0 ;> = true
% because the assignment function (0 0 0) applied to formula (v2 v1 v2) assigns
% every occurrence of variable v2 the value 0. However,
%   Var_map_ok: <0 ; v2 v1 v2 ; v2 ; 0 1 1 ;> = false
% because not every occurrence of variable v2 is assigned value 0 (the second
% occurrence is assigned value 1).
% Var_map_ok: <Val ; Form ; Var ; Assn_fn ;>

% Argument names

ValV:
    <>  == Arg1.

FormV:
    <> == Arg2.

VarV:
    <>  == Arg3.

AssnV:
    <> == Arg3:<Pop_arg>.  % arglists.dtr only defines up to 3.

Var_map_ok:
    <0 ; ;> == true   % Formula = nil
    <1 ; ;> == true   % ditto

    % Is assn fn finished? If so so are we.
    <> == <done First:<AssnV> ; Arglist !>
    <done 0 ;> == <more>
    <done 1 ;> == <more>
    <done ;> == true

    % Is first symbol of Formula the Var we are checking?
    <more> == <1 If:< Equal:< Varbl_or_op:<FormV:<> ; > ; VarV:<> ;> > >

    <1 then> == % Yes. Is it assigned the right value?
                <2 If:< Equal:<ValV:<> ; First:<AssnV:<>> ; > > >
        <2 then> == <reduce var>
        <2 else> == false

    <1 else> == <reduce Typeof:<FormV:<> ;> >
        <reduce op> == Var_map_ok:< ValV:<> ;
                                    Rest:<FormV:<> ; ! > ;
                                    VarV:<> ;
                                    AssnV:<>  ;
                                ! >
        <reduce var> == Var_map_ok:< ValV:<> ;
                                     Pop_varbl:<FormV:<> ; ! > ;
                                     VarV:<> ;
                                     Rest:<AssnV:<> ;> ;
                                     ! >.
% Sample theorems:
%
% Var_map_ok: <Val ; Form ; Var ; Assn_fn ;>
% (1) Initial call
%     Var_map_ok:<0 ; [ 3 ] ~ & | ; [ 3 ] ; 0 ;> = true.
% (2) During recursion
%     Var_map_ok:<1 then 0 ; [ 3 ] ~ & | ; [ 3 ] ; 0 ;> = true.
% (3) during recursion
%      Var_map_ok:<more 0 ; [ 3 ] ~ & | ; [ 3 ] ; 0 ;> = true.
% (5) during recursion
%     Var_map_ok:<done 0 ; 0 ; [ 3 ] ~ & | ; [ 3 ] ; 0 ;> = true.
% (6) during recursion
%     Var_map_ok:<reduce op 0 ; & | ; [ 3 ] ; ;> = true.
% (4) Recursion termination
%     Var_map_ok:<0 ; ; [ 3 ] ; ;> = true.

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

# show
    <[ 0 ] ~ ;> 
    <[ 1 2 3 4 5 ] [ 1 2 3 4 ] | ;>
    <[ 1 2 3 4 ] [ 1 2 3 4 ] | ;>
    <[ 1 2 3 4 ] ~ ;>
    <[ 3 4 4 4 ] ~ [ 3 4 4 4 ] ~ [ 4 4 4 4 2 ] & | ;> 
    <[ 3 4 5 ] [ 3 4 5 ] ~ & ;> 
    <[ 3 ] [ 3 ] & ;>
    <[ 3 ] [ 3 ] & ~ ;> 
    <[ 3 ] [ 3 ] [ 3 ] & & ;>
    <[ 3 ] [ 3 ] | ;>
    <[ 3 ] [ 3 ] ~ & ;>
    <[ 3 ] [ 4 ] [ 3 ] ~ & | ;>
    <[ 3 ] ~ [ 3 ] ~ [ 2 ] & | ;>
    <[ 3 ] ~ [ 4 ] & ;>.

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

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