qat.opt.boolexpr.Clause

class qat.opt.boolexpr.Clause(operator, arity, *children)

Class representing a boolean clause (boolean formula).

Clauses are trees whose leaves are Var objects and internal nodes are labelled by boolean operators (&, |, ^, ~).

Clauses are meant to be built either using the .and_clause, .or_clause, .xor_clause, neg_clause static methods, or via boolean operators overloading:

Parameters
  • operator (str) – the operator (in [”&”, “|”, “^”, “~”])

  • arity (int) – the arity of the operator

  • *children (Clause) – the subclauses

static and_clause(*children)

Creates a logical and of two clauses

evaluate(assignment)

Evaluate the clause using a list of values assigned to the variables

Parameters

assignment (list<bool>) – A list of boolean representing the value of each variables

Returns

The result of the evaluation

Return type

bool

get_observable()

Returns a boolean valued diagonal cost observable matching the evaluation of the clause.

The cost observable is built by induction:

\(H(A \wedge B) = H(A) H(B)\)

\(H(A \vee B) = H(A) + H(B) - H(A) H(B)\)

\(H(A \oplus B) = H(A) + H(B) - 2 H(A) H(B)\)

\(H(\neg A) = 1 - H(A)\)

\(H(v) = (1 - \sigma_z^v)/2\)

Consequently: the resulting Hamiltonian is {0, 1} valued and has as 1-eigenstates the states that satisfy the clause.

get_variables()

Returns the set of variables appearing in the clause.

Returns

a set of variable indexes

Return type

set

static neg_clause(*children)

Creates a logical negation of a clause

static or_clause(*children)

Creates a logical or of two clauses

static xor_clause(*children)

Creates a logical xor of two clauses