It defines the structure of a BigFPL Formula

It allows defining BFPL from text strings, through a parser. To do this, a series of rules are established:

• Atomic formulas (propositional variables) correspond to propositional variables, made up of text strings, with uppercase characters, and can optionally be sub-indexed by a series of indices that correspond to arithmetic expressions. Said indices are specified between the symbols _{ and }; and separated by commas. Examples of atomic formulas are: P,Q_{i, j},AL_{i + k, i-k}.

• An arithmetic expression can correspond to an integer, to a variable specified as a string of characters in lowercase followed, optionally, by some numeric digits (x, i1, y33), or the binary combination of two arithmetic expressions through the infix operators: + (sum), - (subtraction), * (product), // (integer division),% (modulus).

• The formulas can be defined as atomic formulas or as associations of them through infix binary connectives: & (conjunction), | (disjubation), -> (implication), <-> (equivalence ); the unitary connective: ¬ (negation); or two big connectives that follow the format: BigOp + PARAMETERS + CONDITION + BigFPL

  • The BigOp can correspond to !& (BigAnd) or !| (BigOr).

  • The list of parameters that establishes associations between the parameter's Paramifier and its variation universe in the form Paramifier {universe} or Paramifier (universe) (according to the cases described below). These associations are enclosed in brackets [, ], and separated by commas. Note that, for example, !& [I (1..8), j (1..8)] {T} (...) would be equivalent to !& [I (1..8) ] {T}!& [J (1..8)] {T} (....)

  • The universe of variation of a parameter can be specified through discrete integer values, expressed between braces and separated by commas, for example i {1,2,3,4,5,6,7,8}; Or as a range expressed as (ll:up) in the way ll corresponds to the lower limit, andul to the upper limit, both included in the range, equivalent to the previous example i (1:8)

  • The condition is established from a Boolean expression expressed between braces and that can correspond to: the true condition T, the false expressionF, a comparison between arithmetic expressions (in which parameters defined in the operator itself or in predecessor, more external operators). These comparative expressions are expressed in brackets and can correspond to the comparative ones: = (equal), != (Different), > = (greater or equal), <= (less or equal), >(major strict),<(minor strict); Or with Boolean expressions created from Boolean operators AND,OR, NOT.

As a final example, the restriction of the absence of two queens on the same secondary diagonal, in the 8 Queens problem, could be expressed as:

!& [i (0:7), j (0:7)] {T} (P_{i, j} ->!& [k (-7:7)] {[k!= 0] AND [i + k> = 0] AND [j-k> = 0] AND [i + k <= 7] AND [j-k <= 7]} (¬P_{i + k, j-k}))

It allows to extract the formula readed. If there is a parsing error, then it returns Insat formula

It converts a BigFPL to a FPL

It converts a BigFPL to a FPL

It allows resolve the satisfiability of a set of BigFormulas using Backtracking + MRV

It allows resolve the satisfiability of a set of clauses using Backtracking + MRV

It generates the String representation of a BigFPL formula.

It generates the String representation of a BigFPL formula in Latex Format

It generates the String representation of a BigFPL formula in Latex Format, separating the representation of the formula and the representations of the conditions.

It gives the true variables of the model in a string

It gives the true variables of the model in a string in Latex format