MySVC
an open source UNIX framework for shell script based web services provider
»Home
»Tools
»Man Page
»User Guide
»ChangeLog
»Installation
»Source Code
»Downloads
»FAQ
»Support
»License

»My Apps

Icon.png

Features

The Constraints application is a SAT based propositional (boolean) logic engine defined by a list of models, where a model includes a list of constraints (a Knowledge Base) each defined by a propositional formula (x and (y or not z)) including a set of propositional (boolean) variables (x,y,z) and operators (and,or,not).

To each model corresponds a propositional formula equal to the logical and of propositional formulas of currently enabled constraints, and based on a selected model from a list of models that you can add, modify or delete, the application user interface contains three main screen tabs (constraints,variables,solutions) to:

  • add, modify, delete, enable or disable constraints

  • assign values (true,false) to boolean variables (any alphanumeric string including . and _ characters) used by the model propositional formula

  • for satisfiable models (SAT), find one by one all possible assignments to not assigned boolean variables as solutions of the model, such that the model (its corresponding propositional formula) is always true regardless remaining variables assignments.

Include advanced features such as:

  • support of multiple syntax for boolean operators of propositional formulas (not,and,or,implies,equivalent,if,unless, nor and nand): (x and (y or not z) is equivalent to x*(y+-z))

  • real time evalution of constraints and models status (undefined,unsatisfiable,satisfiable,valid), where a propositional formula is valid when is true regardless assignments to its not assigned variables

  • conversion to normal forms NNF, CNF and DNF of propositional formulas associated with each model or constraint; e.g. the Disjunctive Normal Form (DNF) of propositional formula x&(y|~z) is x&y|x&~z

  • evaluation of the propositional formula corresponding to all possible SAT solutions variables assignments to get valid (true) propositional formulas for constraints or models (SAT)

  • export to email or clipboard of:

    • models and constraints definition

    • variable assignments

    • model solutions

    • normal forms of constraints and models

  • import from web (from a configurable set of 'URL’s) of:

    • models definition (a simple text containing an optional model description and a list of constraint names)

    • constraints definition (a simple text containing an optional constraint description and its propositional formula)

    • mailing list for export to email (including a list of email address or http URL of text files containing mailing list)

    • evaluation of (true,false) value of variables

  • percistence

  • Feature Models (FM) and Propositional Logic Truth Maintenance System (LTMS) capabilities, such as find the smallest set of requires and excludes rules based on selected features (boolean variables, true iff the feature is selected) and propositional formula related to logical constraints of these features; e.g. if from model constraints you get four features a,b,c,d and four product lines (a,c), (d), (b) and (a,b,d) (from DNF normal form) with Requires functionality you get rules (represented as propositional formulas) such as the selection of c feature requires feature a and excludes features b and d (c→a&~b&~d) or the selection of a and b features requires feature d (a&b→d)

User interface

The user interface of Constraints application contains three tab screens, each containing on the first table row the name and status of the actual (selected) model

  • the first one (X&Y) contains a table with the list of all constraints; you can add, modify or delete item.

  • the second one (T|F) contains a table with the list of all boolean variables used into all enabled constraints

  • the third one (123) contains a table with the actual solution based on the set of enabled constraints and the assigned variables

First Tab (X&Y)

The first tab screen handle models and constraints definition:

  • each model is defined by:

    • a name

    • an optional description

    • a list of constraints

  • each constraint is defined by:

  • each constraint can be enabled (if doesn’t contains syntax errors) or disabled

  • each model and each constraint have a status:

  • if a constraint doesn’t contains syntax errors it’s enabled by default, else is undefined

  • a model is undefined if it does not include any enabled constraints.

  • a constraint is undefined if its propositional formula is empty or with syntax errors.

  • the propositional formula used to compute the status of a model is the logical and of all propositional formulas of its enabled constraints

  • selecting the first row of each screen tabs can be selected another model, edited the model list (add, delete) or view a model description; with the right button on the first row of each screen tabs you get the Model screen for:

    • view model status or edit the actual model properties (name, description)

    • edit, import or export the model definition (optional description plus . plus list of constraint names) selecting the first row of Model screen; with the right button on this screen you get the Requires screen with Feature Models rules

  • pushing the top right button on the Model screen you get the Normalize screen to evaluate normal forms and SAT solutions, with export capability.

  • selecting a single constraints on the first main tab you get the screen Constraint like Model screen but applied to propositional formula of selected constraint.

Second Tab (T|F)

The second tab screen handle model variables assignment depending on the set of enabled constraints:

  • the top left button is used to select a circular mode between:

    • True

    • False

    • Import

  • the actual mode is on tile of second table section

  • with True and False you:

    • select the default assigned value used with single tap on a variable row

    • the double tap swap boolean value (from true to false and from false to true)

  • with Import the boolean value (true,false) assigned to variables is imported from web

  • to each variable row is associated a status: true, false or (without checkmark) undefined

  • the top right button is for:

    • with True or False mode: select (with default assigned value) or unselect all not assigned (i.e. undefined) variables

    • with Import mode all values of not assigned (undefined) variables are imported from web

  • pushing the right button on the first table row (related to model and its status) you get a propositional formula representing all assignments (e.g. x&~y if x=T and y=F), with export capability

Third Tab (123)

The third tab screen handle model solutions (one by one) depending on the set of enabled constraints:

  • with the top right button you get the next solution (if any)

  • with the top left button you return to the first solution (if any)

  • variables already assigned don’t have checkmark (as opposite from second tab of variable assignments)

  • pushing the right button on the first table row (related to model and its status) you get a propositional formula representing all value of current solution with export capability

Propositional Logic

Propositional logic deals with statements or propositions and the connections between them, where each proposition is represented by a variable with true (T) or false (F) value.

Besides variables representing propositions, propositional logic also includes boolean operators that represent logical relations such as and, or, not, implies (if-then) and equivalent (if-and-only-if), when not is the unique unary (boolean) operator and the others are all binary (boolean) operators.

Let p be the proposition The sun is shining, and let q be the proposition It is raining. The most commonly used operators in propositional logic correspond to the English words and, or, not, if-then, and if-and-only-if:

  • Conjunction (and). p and q represents the proposition The sun is shining, and it is raining.

  • Disjunction (or). p or q represents The sun is shining, or it is raining.

  • Negation (not). not p represents The sun is not shining.

  • Implication (if-then). p implies q represents If the sun is shining, then it is raining.

  • Equivalence (if-and-only-if). p equivalent q represents The sun is shining if and only if it is raining.

The rules used by propositional logic compute the truth value of a compound proposition (propositional formula) from the truth or falsity of the elementary propositions (variables) contained within it.

They are therefore called truth functions, whose inputs are the truth values T for true and F for false.

The following tables, called truth tables, shows the outputs generated by the five truth functions and, or, not, implies, and equivalent for all possible combinations of the two inputs p and q.

Table 1. and
p q p and q

T

T

T

T

F

F

F

T

F

F

F

F

Table 2. or
p q p or q

T

T

T

T

F

T

F

T

T

F

F

F

Table 3. not
p not p

T

F

T

F

F

T

F

T

Table 4. implies
p q p implies q

T

T

T

T

F

F

F

T

T

F

F

T

Table 5. equivalent
p q p equivalent q

T

T

T

T

F

F

F

T

F

F

F

T

There are 16 possible truth functions of two arguments, but and, or, not, implies and equivalent are the most commonly used.

Other boolean operators are xor, nand and nor:

  • p xor q (exclusive or), equivalent to (p or q) and not (p and q) (p or q, but not both)

  • p nand q equivalent to not (p and q)

  • p nor q equivalent to not (p or q)

Following are some common equivalences. When two formulas are equivalent, either one can be substituted for any occurrence of the other, either alone or as part of some larger formula:

  • Idempotency. p and p is equivalent to p, and p or p is also equivalent to p.

  • Commutativity. p and q is equivalent to q and p, and p or q is equivalent to q or p.

  • Associativity. p and (q and r) is equivalent to (p and q) and r, and p or (q or r) is equivalent to (p or q) or r.

  • Distributivity. p and (q or r) is identical to (p and q) or (p and r), and p or (q and r) is equivalent to (p or q) and (p or r).

  • Absorption. p and (p or q) is equivalent to p, and p or (p and q) is equivalent to p.

  • Double negation. p is equivalent to not not p.

  • De Morgan’s laws. not (p and q) is equivalent to not p or not q, and not (p or q) is equivalent to not p and not q.

A propositional formula is said unsatisfiable when it is always false regardless from assignments of truth values to its variables.

A propositional formula is said valid (or tautology) when it is always true regardless from assignments of truth values to its variables.

A propositional formula is said satisfiable when it can be true or false depending from assignments of truth values to its variables.

To prove that proposition B is a logical consequence of proposition A (i.e. A→B) you must prove that its negate not (A→B) is unsatisfiable:

  • not (A→B) = not (not A or B) = A and not B

So to prove that B is a logical consequence of A is equivalent to prove that A and not B is unsatisfiable.

Normal forms

The main normal forms of propositional logic are:

  • Negation Normal Form (NNF)

  • Conjunctive Normal Form (CNF)

  • Disjunctive Normal Form (DNF)

A propositional formula is in Negation Normal Form (NNF) if negation occurs only immediately above elementary variables, and { not, or, and } are the only allowed boolean connectives.

Each formula can be brought into this form by replacing implications and equivalences by their definitions, using De Morgan’s laws to push negation inside, and eliminating double negations.

E.g.: the NNF of formula not (a and not b) is not a or b

A propositional formula is in Conjunctive Normal Form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals and a literal is a variable or its complement (negated variable), and where a literal and its complement cannot appear in the same clause.

The only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

E.g.: (a or b or not c) and (d or not e or f)

A propositional formula is in Disjunctive Normal Form (DNF) if it is a disjunction of clauses, where a clause is a conjunction of literals and a literal is a variable or its complement (negated variable), and where a literal and its complement cannot appear in the same clause.

The only propositional connectives a formula in DNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

E.g.: (a and b and not c) or (d and not e and f)

SAT

SAT (from satisfiability) is the test to verify if a propositional formula is satisfiable.

When a propositional formula is satisfiable, the SAT solutions of a propositional formula represents the set of all assignments of truth values (true or false) such that the truth value of the propositional formula is true

E.g.: the three SAT solutions of the propositional formula a and (b or not c) are:

  • a=T, b=T, c=T (a and b and c)

  • a=T, b=T, c=F (a and b and not c)

  • a=T, b=F, c=F (a and not b and not c)

Propositional formula

Each propositional formula of the Constraints application is case sensitive and include:

  • any string of alphanumeric characters (A-Z,a-z,0-9) (including . and _ characters) as boolean variables

  • spaces and newlines (can be written on more text lines)

  • the opened and closed parentheses:

(

)

  • one of the following syntax for constants true and false:

Table 6. true

true

TRUE

t

T

Table 7. false

false

FALSE

f

F

  • one of the following syntax for not unary operator:

Table 8. not

not

NOT

-

~

!

  • one of the following syntax for binary operators and, or, implies, equivalent, if, unless (xor), nor, nand:

Table 9. and

and

AND

*

&

&&

^

,

Table 10. or

or

OR

+

|

||

v

V

implies

p implies q = not p or q

implies

IMPLIES

->

=>

equivalent

p equivalent q = (p implies q) and (q implies p)

equivalent

EQUIVALENT

iff

IFF

<->

<=>

=

if

p if q = q implies p

if

IF

<-

<=

:-

unless

p unless q = (p or q) and not (p and q)

unless

UNLESS

xor

XOR

;

nor

p nor q = not (p or q)

nor

NOR

nand

p nand q = not (p and q)

nand

NAND

The precedence order of the binary operators (from higher) is: and,or,implies,equivalent,if,xor,nor,nand

The formulas can include the following type of comments (ignored by parser):

p and q // a comment from begin to end of line…

p {an internal comment…} and q

p /* a comment… on more lines… */

Settings

On Settings there are:

  • the email field, used for export to mail, must contains a list of email address (one for each text line) and can include commented lines if the email address starts with a # character (without spaces between # and the email address).

  • the URL for models, where the related web resource (of Content-Type text/plain), e.g. a .txt file, must contains an optional model description followed by a line with a single . and a list of constraints name; you are including commented lines if the constraints name starts with the # character and you can use into URL special parameter ${m} representing the name of model (then replaced with the current name of model)

  • the URL for constraints, where the related web resource (of Content-Type text/plain), e.g. a .txt file, must contains an optional model description followed by a line with a single . and its propositional formula; you can use into URL special parameters ${m} and ${c} representing the name of model (then replaced with the current name of model) and the name of the constraint (then replaced with the current name of constraint)

  • the URL for variables, where the related web resource (of Content-Type text/plain), e.g. a .txt file, must contains a single character:

    • T, t (or a string starting with T or t such as True or true) or 1 if the variable value is true

    • F, f (or a string starting with F or f such as False or false) or 0 if the variable value is false

Feature Models

Feature Models (FM) application capabilities permits, given a propositional formula related to a constraint or to a model and related to the logical relationship of a set of features, to find the smallest number of logica rules (propositional formulas) describing what features are required or excluded if a set of features is selected.

E.g.: if you have the following propositional formula describing four product lines on a set of four features a, b, c and d:

(a&~b&c&~d)| (~a&~b&~c&d)| (~a&b&~c&~d)| (a&b&~c&d)

you can get as output (from Requires screen) a propositional formula made of the logical and of the following rules:

  • b→~c

  • c→a&~b&~d (the selection of c feature requires feature a and excludes features b and d)

  • d→~c

  • a&b→d (the selection of a and b features requires feature d)

  • a&d→b

  • b&d→a

Examples

For model examples see models Party and Expert preloaded into Constraints application.

You can find these models on this web site too, under the following URLs (preconfigured on Constraints) in order to test import from web features.

Before you can import a model from web the model must exists on Constraints application, even if empty (without constraints), so to import the predefined party or expert from web you must create two new models with these names (lowercase, because the uppercase names are used for preloaded model versions on Constraints application).

Party

A simple example where four friends give constraints to party organizer.

Expert

A simple application of expert system for automobile diagnosis based on Knowledge Representation.

In order to prove that either the line or the cable line is broken add to the model the constraint representing the negate of that proposition: not (not FuelLineOK or not CablesOK); iff the model is unsatisfiable the proposition is a logical consequence of the other model constraints, because to prove that proposition B is a logical consequence of proposition A (i.e. A→B) you must prove that its negate not (A→B) is unsatisfiable:

  • not (A→B) = not (not A or B) = A and not B

Support

For support contact davide6169@gmail.com