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 (boolean) formula (e.g. '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
- for satisfiable models, find one by one all possible assignments to not assigned boolean variables as solutions of the model, such that the model (i.e. 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,nand): '(x and (y or not z)' is equivalent to 'x*(y+-z)'), or for comment capabilities ('#','//','{}')
- 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 (e.g. NNF or CNF) of propositional formulas associated with each model or constraint; e.g. the Disjunctive Normal Form of propositional formula 'x&(y|~z) is 'x&y|x&~z'
- evaluation of the propositional formula corresponding to all possible SAT solutions with variables assignments to get valid (true) propositional formulas for constraints or models
- 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 URLs 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, with comment capability using '#')
* 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 Disjunctive 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')