Skip to content

Latest commit

 

History

History
55 lines (35 loc) · 3.72 KB

constraints_format.md

File metadata and controls

55 lines (35 loc) · 3.72 KB
Raw

Constraints String Format

Under the hood, the program accepts a string of constraints in a low-level defined format. It is also possible to feed into the program a string of constraints in a high-level setting, and a translation layer will take care of the necessary conversion.

Supported features

The program accepts:

  • Multiple constraints combined into a single string. Each constraint must reside inside round brackets and must be separated from neighboring constraints by commas. A general description: "(--CONSTRAINT_1--),(--CONSTRAINT_2--),...,(--CONSTRAINT_N--)".
  • Every single constraint can be either an arithmetic constraint or a boolean constraint.
  • An arithmetic constraint must contain one comparison operator - that is "==" (EQUAL) or "!=" (NOT EQUAL), and may contain the "+" (PLUS) arithmetic operator along with variables or natural numbers. A general description: "(--LEFT_OPERAND-- --COMPARISON_OPERATOR-- --RIGHT_OPERAND--)". Each operand can possibly be a sum of sub-operands (variables or natural numbers).
  • A boolean constraint must contain binary variables (i.e single-bit long) only, along with boolean operators: that can be binary - "||" (OR) and "&&" (AND), or unary - "~" (NOT). For now, a mixture of binary boolean operators is not allowed - i.e a single constraint can contain either "&&" or "||" operators. The "~" unary operator is always allowed. A general description: "(--VAR_0-- && --~VAR_1-- && --VAR_2--)" or "(--VAR_0-- || --~VAR_1-- || --VAR_2--)".

The features listed above are accessible via a high-level setting or a low-level format.

Low-level format

The low-level format specifies explicitly the bit-indexes of each variable, in a little-endian fashion (the most significant bit is the leftmost bit). Each bit index must reside inside square brackets, and natural numbers must be bare.

Low-level examples of arithmetic constraints (each example is a single constraint):

  • ([3][2] != [0])
  • ([6] == [5])
  • ([6][5][4] == [3])
  • ([2] + 2 != [4][3])
  • ([0] + [1] + [2] + [6][5][4] == 7)

Low-level examples of boolean constraints (each example is a single constraint):

  • ([7] || ~[1] || ~[0])
  • ([7] && ~[1] && ~[0])
  • ([3] || [2] || [1] || [0])

High-level setting

It is possible to define constraints with variables and not worry about bits-indexing issues, using a high-level simple API defined by the class sat_circuits_engine.interface.translator.ConstraintsTranslator. It is required to set as inputs the constraints string with variables named as you like, along with a dictionary object that specifies how many bits each variable requires. Then the translate method will return a suitable low-level string.

For example, for the given code:

vars = {'x0': 3, 'x1': 1, 'x2': 3, 'x3': 4}
high_level_string = "(x0 != 4),(x1 + x2 == x0),(x3 + x0 + x1 + x2 != 27)"

translator = ConstraintsTranslator(high_level_string, vars)
low_level_string = translator.translate()

print(low_level_string)

The output is:

([2][1][0] != 4),([3] + [6][5][4] == [2][1][0]),([10][9][8][7] + [2][1][0] + [3] + [6][5][4] != 27)

NOTE: The recommended way to use the high-level format is via SATInterface's API, which seamlessly executes the translation as demonstrated above. To do so it is required to call SATIntreface with the arguments high_level_constraints_string and high_level_vars. For an example please see "demo 1" in the demonstration notebook.

Important Notes

  1. Many examples may be found in test_data.json.
  2. The program usually naively assumes valid user inputs, i.e disobeying the defined format will probably lead to an error or wrong results.