Notice on BooLean software (ppc or 68000 platform)
This software is built on for handling Boolean functions written in conjunctive
normal form (conjunction of clauses or CNF) or disjunctive normal form (disjunction of implicants or DNF); the forms are without absorption.
Except for some easy procedures (edition, sorting and some boolean operations) most of them (dualization, disjoint forms, satisfiability) are really hard, need a lot of memory and may scratch the software even if a maximum number of precautions have been taken.
The software has been developed on a Macintosh (with a 680x0 Motorola or a PowerMac processor) and in its first release the number of variables is bounded by 32. Each variable has an invisible rank from 0 to 31.
Calling by term of a boolean function F, either a clause (if F is CNF) or an implicant if F is DNF, a term is mainly encoded by two characteristic vectors of 32 bits; the first vector corresponds to positive literals (uncomplemented variables) present in the term and the second to its negative literals (complemented variables).
Concerning the function, besides some information fields such that its number of variables, its number of terms, its Variable-set, its normal form type (disjunctive or conjunctive), its possible positiveness quality (where positiveness means without negative literals), the main information is given by a simple linked list of terms (with a starting pointer). The number of terms is thus bounded only by the dynamical allocation capability of the system.
In order to avoid the naming of a variable by its absolute rank (because taking possibly two characters), we have chosen to name these variables by one character. Ranks between 0 and 25 are respectively denoted by the lowercase letters between 'a' and 'z' while ranks from 26 to 31 use the characters '1' to '6'.
Each function H in its window is presented in the top zone, by a general board which displays the following informations: the number nX of its variables, its variable-set VarSet, the number mH of its terms, its normal form type Normform , its General or Positive quality and its size i.e. the total number of characters (including blanks) for describing the list of its terms.
Below this top zone, the text zone displays the list of all terms written as simple words, separated by + (resp. & ) if DNF (resp. CNF) form of H. Each word begins generally by the alphabetical list of positive literals followed by the minus sign - and ended by the alphabetical list of negative literals. For example, if H is DNF, the word cdf-bg represents the implicant
c & d & f & ~b &~g.
An empty list (mH=0) means a constant function ( 0 constant function or basic antilogy if H is DNF and 1 constant function or basic tautology if H is CNF). Thus an empty list is displayed F (false) for DNF, and T (true) for CNF.
An empty term is allowed in H: by absorption's law, H has then only this term and is a basic tautology if H is DNF, and a basic antilogy if H is CNF; thus an empty term is written T (in DNF) and F (in CNF).
In the text zone, when a modification of window's shape is involved, no terms are horizontally hidden but are rehoused between vertical limits (so that a window needs only a vertical lift bar).
The chosen text editor for displaying these terms is very simple (TEXTEDIT) and thus has a size limitation of 32768 characters. In many cases, the function may have a size largely beyond this limit; in this case the display is truncated to the first terms of the list, within this TEXTEDIT limitation. A major disadvantage is then the impossibility of saving directly this function in one document. We must split it in many little parts. An automatic procedure may fulfill this task together with other ones in the Menu Bar. Apart from this disadvantage, one can even process the function for other purposes as long as the system heap is not full.
Actually, this sensitive part is not robust; many bugs still remain. The next task will be to eliminate them.
The mouse events are the following:
The insertion point is always just before a term or after the last term (this last position being the standard position). Therefore it cannot be inside a term. Similarly, a non empty selection starts always from the beginning of a term and ends at the end of the last term of the selection. Simple or double clicks (with possible dragging) mouse events follow the standard interface of the Macintosh (according to the previous specifications).
The keyboard events are the following:
With an empty selection, one can type any sequence of characters a z 1 6 (a backspace is allowed for local correction) together with the - character (only once); in order to take into account this entry, one must type space or return key. One may type also the majuscule F (in conjunctive normal form) or T (in disjunctive normal form). After a space or return key, the term is actualized (elimination of multiple literals, of the term itself if it contains two opposite literals, and alphabetical ordering of the two parts of the term); then it is added to the current list (if no absorption appears) at the insertion point (which is automatically set at the end). If one leaves the typing (for any active purpose) without validating by blank or return key, the entry is definitely lost.
With a non empty selection, after any correct typing (including the backspace), the selected terms are deleted (except if an immediate Undo command is performed in Edit menu). Then everything runs as with an empty selection.
The New item creates a null function (without terms) in disjunctive normal form with 32 variables.
The Open item is standard but enlarged. Besides Boolean documents, it allows to open without problem any Clutter document (from Clutter software) but with some risk any text document (an alert is displayed in this case). The annex gives the text structure of a Boolean file so that the user may prepare a Boolean formula (from any application) by a text file following this text structure.
The Random item opens a dialog for generating a random function. Six fields may be filled: the number of variables, an upper bound for the number of terms, a specification of uniform (or homogeneous) quality, the minimum degree (number of literals) of each term, the positiveness (or not) of the function and at last the conjunctive (or disjunctive) characteristic of the normal form.
The Threshold item opens a dialog for generating a threshold function (not necessarily positive but monotonous). First the number nn of variables is required. Then a grid is open with nn+1 boxes to be filled by integers (positive or negative) : the threshold and the weigths of the nn variables.
The Close, Save, Save as items are standard except that we cannot save a big function (whose size exceeds 32768 characters). One may close a big function without saving it: a message (without progress bar) alerts that we are deallocating this big function.
The Forced Close item is like Close except that no preliminary alert (concerning a modified document) is done.
The Quit item is usual (with preliminary alerts for saving the created or modified documents).
In this version, FILE menu has no Print item. Next version will provide such an item. We can nevertheless print a document by means of the scrap, as it is explained in the next section.
The Undo item is often inactive except when a modification (in EDIT or VARIATION menu or by manual editing) is done. It applies only once.
The Cut, Copy items are standard. The scrap has a private structural part (available only during the session) and a public text part (available, after leaving the session, in any text handling application).
The Select All item is standard with the following precision: when a function is big (its size is more than 32768), only the displayed (truncated) part is selected.
The Paste item (when active) tries to add (with absorption constraint) the terms of the private scrap. If you leave for a while the application (by jumping to another) when you come back to Boolean, your private scrap (if non empty) is not modified (even if you use a scrap of the other application).
The Clear item deletes all the selected terms.
The Change Nform item is a formal change of the current normal form into its dual.
The Formal Complement item changes formally all the & into + (or + into &) and replaces each literal by its opposite (permutation of the rigth part and the left part in each term).
The Variable Sorting item opens a dialog box for getting a lexicographic order (possibly partial) of the variables by means of a word (with distinct letters). If one types for example the word uedg, the corresponding action consists first in writing all the terms containing u followed by all the terms containing ~u, then all the terms without u or ~u; then, in each of these 3 sublists all the terms containing e followed by all the terms containing ~e followed by all the terms without e or ~e (and so on) Note that we change the order of the terms but that each term is always written according to the conventions (of alphabetic order). If the typed word is a full permutation of X, we get a total lexicographic order. But if the chosen word is shorter than nX (for example b) the effect is to put first the terms with b, followed by the terms with ~b and at last all the others; each sublist keeps its relative order.
The Degree Sorting item intends to sort the terms of the current function according to increasing or decreasing degrees (chosen in a dialog box).
The Rename.. item waits for a bijection of the Variable set X by means of a simple (i.e. with distinct letters) word. For example (with X = acdf) when entering uabc, the variable a is changed into u, c into a, d into b and f into c.
The Shift.. item waits for a positive integer t (within a displayed bound). Indeed, if k is the largest rank of the variables of the current function, one may shift of at most 31-k. Let t be the entered number; each variable whose rank is i will get the rank t+i.
The Compacting item acts firstly by deleting all absent variables and secondly by replacing the ranks i1 < i2 < < in of the n present variables respectively by 0,1, n-1.
The two last items: Delete dummy and Add dummy allow to delete or add (if possible) dummy variables (among a displayed set).
PRESENTATION MENU
All the items of this menu are conceived in order to give an equivalent boolean formula (with respect to logical calculus) to the current function HH. All the computations are generally very hard and then are alerted by the suffix (NP). For each item, a new window is created whose name is the initial name HH followed by a symbolic character recalling the corresponding item.
The Dual Form item gives an equivalent expression of the function in dual normal form. The result is the list of all prime implicants (if we are in CNF) or all prime clauses (if we are in DNF); it is unique up to the order of the terms. It is based on an incremential algorithm using distributivity of +/& and a progress bar shows the hardness of the computation. One may attempt to stop it (insist on cancel). The name of the new form is HH*
The Disjoint Form item finds a disjoint expression, a form in which any two terms have conflictual literals so that they cover disjoint sets of true points (case of DNF) or false points (case of CNF). The algorithm is incremential but no progress bar is active in this item: next versions will provide such a feature. The name of this new form is HH#
The IrredundantForm item finds an irredundant expression by deleting terms in such a way that this does not change the function. It is based on satisfiability (or refutability) algorithm of Davies and Putnam. The chosen name is HH- (a subset of HH terms).
The Full Prime item yields all the prime terms (no progress bar). It results in a unique form (up to the order of the terms); it is based on consensus method and the chosen name is HH"
The Prime Basis item (also with no progress bar) finds an irredundant list of prime terms (generally a proper subset of HH"). It is based on intensive use of Davies and Putnam. The chosen name is HH'
CONSTRUCTION MENU
Here we put together ten various constructions of functions from the current one called HH whose variable set is called X. A new window is generated. Items with suffix (NP) alert that it may take a prohibitive time. As for the Presentation menu, a naming procedure sets a name for the generated window relying to the type of creation. Give now all the details.
The Duplicate item yields a duplication of HH with the name =HH
The Assignment.. item asks (by a dialog box) for the two sets of variabes which we want to assign the values 1 and 0. The resulting function depends on the variables X-A where A is the set of assigned variables. The chosen name is B+HH-C where B is the set of 1-variables and C the set of 0-variables.
The Fusion variable item waits for a subset A of X. It consists in identifying in each term, every variable from A which belongs to this term with the variable of A of minimum rank (while taking into account the absorption constraint). The chosen name is HH=A
The Extract by size item waits for an integer k (within displayed bounds) and yields all the terms of HH with k literals. The chosen name is X.kHH
The Positive Bound item deletes from each term of HH the negative literals (while taking into account the absorption constraint). We know that the resulting function is the minimum (resp. maximum) positive function greater (resp. smaller) than the current disjunctive (resp. conjunctive) HH. The results is named MajHH (resp. MinHH) according to the current normal form.
The Switch item asks for a subset A of X and replaces in HH each literal of A by its opposite. The chosen name is _AHH
The Regularization.. item requires that the current function is positive; by opening a dialog box, it asks for a linear (influential and decreasing) order by means of a simple word W (permutation of X). The resulting function is regular (2-monotone) and is named HH>W.
The Complement item gives the complement of HH (full prime) in the same normal form than the current one. For the used algorithm, see Dual Form item in the Presentation Menu. A progress bar is displayed. The chosen name is ~HH
The Dual function item gives the dual of HH (full prime) in the same normal form than the current one. Same remark concerning the used algorithm. A progress bar is displayed. The chosen name is *HH
At last, the Split item (which is not well working) is announced here (but not recommended); it is available only when the current function is big (needing more than 32768 characters). When it works successfully, the function HH is splitted into a first one named HH1 (of size < 32768) consisting of the first terms of HH within this limit, followed by a second function (possibly big also) and named HH1> giving the sequence (possibly truncated) of the remaining terms.
OPERATIONS MENU
Here we put together three basic constructions of functions from two ones: the active (front) function called HH and the below function called HS. So this menu is active only when at least two documents are present. A new document is created and its name is computed (taking into account the operation and the two components names). The algorithms are generally polynomial in the size of the components. Under a separating bar, all the documents are listed from the top (active document) until the low (the least active one). Acting with mouse on some document of the list puts it in the top (making it active). One can thus control the two components and their order to operate.
The Union item generates the function HH v HS and names the result by HH+HS. The functions HH and HS may have any normal form. When these normal forms are different, the conjunctive normal form function is transformed in disjunctive form (no longer polynomial algorithm) and the result has disjunctive normal form. In all other cases, the resulting function keeps the same normal form as its components.
The Product item is nothing else than the dual of the previous item and the same remarks apply dually. The chosen name is HH.HS
The Composition item intends to replace one variable (say x) (obtained by a dialog box) of HH by the function HS. The chosen name is HH-x>HS
COMPUTATIONS MENU
All hard computations are alerted by the suffix (NP), all others being polynomial (except if further computations are performed after answering a dialog box).
The Positive?.. item intends to test the positivity of the current function mainly when its form is not. Then the computation may be NP-hard since we must go through Prime Basis in Presentation Menu; when the function appears to be positive, its presentation is updated (positive form).
The Monotone?.. item intends to test the monotonicity of the current function (isotone on some variables and antitone on other variables). A first easy examination (detection of no pairs of opposite literals) may be continued after agreement by Prime Basis computation. When the function appears to be monotone, its presentation is updated (monotone form).
The Regular(2-Monot)? item tests the 2-monoticity of the current function and when it is, gives a list of words W1 W2 .. Wk meaning that all variables in a same word are iso-influential while variables of Wi are more influential that all variables of Wj (j>i). The (polynomial) algotithm is based on a paper by Boros, Hammer, Ibaraki and Kawakami (SIAM J. on Comp)
The Quadratic?.. item tests that the form is or not quadratic (i.e. each term has degree at most two) and, if not, suggests (without doing it) that you go to Prime Basis.
The Q-Horn?.. item tests if the current form is pure Horn or disguised-Horn or quasi-Horn-quadratic and when it is yields an appropriate answer. If not, it suggests to go to Prime Basis. Except for Prime Basis, the linear algorithm is based on a paper by Boros, Hammer and Sun (DAM, 55, 1994).
The Refutable? item [for disjunctive normal form] changing in Satisfiable? item [for conjunctive normal form] tests that the current disjunctive [resp. conjunctive] function is a tautology or not [resp. an antilogy or not]. The algorithm is based on Davies and Putnam method. If it is refutable [resp. satisfiable] a dialog suggests to compute the exact number of false [resp. true] points; if we agree, the process go to the Disjoint Form routine in the Presentation Menu.
ANNEX: TEXT FILE STRUCTURE ON THE DISK OF A BOOLEAN DOCUMENT
Consider for example the boolean conjuctive normal form with 8 variables
{a, b, c, d, e, f, g, h}
and 5 clauses
ab-e
g-abde
h-ag
-agh
bcd
(to the rigth of -sign are the negative literals and to the left the positive literals))
The corresponding text Boolean file consists of 6 words (one more than the clauses number) separated by a 3-sequence of a blank, the connective &, the blank (for disjunctive form the connective is +). The 5 first words describe the clauses; the last word (without -sign) gives (in one word) all the variables. Thus dummy variables (like f in the example) are keeped.
The given example has thus the text file structure (size 34 ?)
ab-e & g-abde & h-ag & -agh & bcd & abcdefgh