[FOM] Re: Truth value algorithm for tokens
Axiomize@aol.com
Axiomize at aol.com
Thu Nov 7 17:32:23 EST 2002
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.
More information about the FOM
mailing list