Browse Prior Art Database

Iterative Common Truth Set Detection Mechanism for Boolean Function Satisfiability Recognition

IP.com Disclosure Number: IPCOM000081447D
Original Publication Date: 1974-Jun-01
Included in the Prior Art Database: 2005-Feb-28
Document File: 4 page(s) / 48K

IBM

Related People

Etchison, KL: AUTHOR

Abstract

Boolean Function Domains and Truth Sets.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 54% of the total text.

Page 1 of 4

Iterative Common Truth Set Detection Mechanism for Boolean Function Satisfiability Recognition

Boolean Function Domains and Truth Sets.

A boolean function in "n" variables has a domain of 2/n/ n-tuples of truth values for the variables. For example, for 2 variables, a and b, the domain is ab, ab, ab, and ab, 2/2/ or 4 combinations. The truth set is defined as the subset of n-tuples for which the boolean function is true. The truth set for a function in conjunctive normal form is the intersection of the truth sets for its disjunctive clauses, and for a function in disjunctive normal form, the union of the truth sets for its conjunctive clauses.

The following function in 3 variables is in disjunctive normal form:

ab v bc v abc.

The conjunctive clauses and their truth sets are; ab abc, abc

bc abc, abc

abc abc.

The truth set for the function is [abc, abc, abc, abc].

Determining the satisfiability of a function in conjunctive normal form can be done by checking to see if its "not" is a tautology. If the "not" is a tautology, the function is not satisfiable.

The determination will be made by computation of the number of elements in the truth set for the "not". If there are 2/2/ elements (n=number of variables), the function itself is not satisfiable.

The "not" of a function in conjunctive normal form is quickly written by "not"ing all the variables and switching the "AND" and "OR" operators. For example, the "not" of the function original page 67.

The number of elements in the truth set for a clause that is the conjunct of m variables from a set of n variables is 2/n-m/.

The number of elements in the truth set for a disjunctive normal form function is not merely the sum of the number of elements of its clauses, however, as the truth sets for the clauses may contain common elements. This sum does have a use in the computation though and it is the "clause total" for the function. The clause total in the example is 2/3-2/ + 2/3-2/ + 2/3-3/ = 2+2+1 = 5.

(Note that no further computation is required, as the clause total is always >/- the actual total. This function is satisfiable, as its "not" cannot be a tautology.) Clause Total Correction.

In order to arrive at a correct total the clause total must be reduced by the number of common elements in the various truth sets. This can be done by computing the number of common elements in the truth sets for clauses 1 and 2,

1

Page 2 of 4

1 and 3, 1 and 4, etc., then for 2 and 3, 2 and 4, until all combinations of two have been made.

A single clause whose truth set is the intersection of the truth sets of two clauses may be generated in the following manner:
1) If a variable appearing in one clause appears "not"ed

in another clause, the intersection is null.
2) Otherwise, the new clause is the conjunction of all the

variables appearing in either clause.

For ins...