[FOM] Re: Truth value algorithm for tokens

[Axiomize@aol.com]

On 6 Nov 2002, Sandy Hodges wrote:

> You have coded the fact that token a is
> ~ Fa(d) & (0=0 <=> Fa(c))
> as:

>> a1 <=> (~d2^c2)

> However it could be the case that token d is not false, and token c is
> false, without token a being true.   This could happen if token a is
> gap.

Yes, if you allow clauses created by a token with a value of gap to not be 
satisfied.

> Furthermore, if you modify your proposal to read
> [ a1 => (~d2 ^ c2) ] ^ [ (~d2 ^ c2) => (a1 or a3) ]
> which is the correct condition, then the model which calls all tokens
> gap, would satisfy the conditions, but that woudn't make it right.

Yes, but under the above treatment of the value gap, this anomaly occurs with 
any set of clauses.

You are considering two variations of SAT: allowing variables to assume a 3rd 
value (multivalued SAT) and allowing clauses to not be satisfied 
(unconstrained SAT.)  Furthermore, you are imposing the constraint that a 
token (variable) must have the value gap if any of its clauses is not 
satisfied.

I would segregate these rules, and classify any set of clauses according to 
which types of solutions exist, to determine the best solution for the set.  
For example:

1. Boolean Solution: All variables are Booleans.  (SAT - no paradox)

2. Tertiary Solution: All variables are tertiary, allowing the value gap.  
(multivalued SAT, possibly solved by encoding it into Boolean SAT)

3. Unconstrained Gap Solution: Tertiary variables and clauses associated with 
variables assigned the value gap need not be satisfied.  (SAT with this gap 
rule incorporated into the clauses)

4. Unconstrained Solution: All clauses need not be satisfied.  (discrete 
unconstrained SAT)

To solve the given problem, it is not actually necessary to use the value gap 
(assuming & binds more tightly than <=> in token c.)  There exists a Boolean 
Solution and no paradox.  Running a SAT program against the entire set of 
clauses (I wrote my own for the sake of this discussion) yields 4 Boolean 
Solutions, with the following values for variables 1-8:

 T F F T T T T T
 T F F T F T T T
 F F T T T F T T
 F F T T F F T T

Note that, in toto:

4 = 7 = 8 = true
2 = false
5 is arbitrary
1 = 6 = ~3 is arbitrary,

yielding the 4 Boolean Solutions.  This gives us a succinct characterization 
of the possible values of these 8 variables (which is then easily proved to 
define the complete set of Boolean Solutions.)

For a discussion of the discrete unconstrained formulation, see: Algorithms 
for the Satisfiability (SAT) Problem: A Survey - J. Gu, P. W. Purdom, J. 
Franco, and B. W. Wah, in "Satisfiability Problem: Theory and Applications", 
DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 
American Mathematical Society, 1997, pp. 19-152, 
http://citeseer.nj.nec.com/56722.html (pg. 12.)

> If the definition which I am proposing were to be generally accepted,
> ideas from satisfiability research would be worth considering.

Or perhaps vice versa.

Charlie Volkstorf
Cambridge, MA

> Sandy Hodges / Alameda,  California,   USA
> mail to SandyHodges at attbi.com will reach me.