tqecd.match_utils.sat

Semi-private module providing functions to construct SAT problems.

This module is semi-private in the sense that even though the two functions it implements are not private, they are quite low-level and are not expected to be used by external users of the library.

The module defines 2 functions that each take a SAT solver able to encode XOR clauses, a target Pauli string, a list of potential Pauli strings and a set of qubits to consider and encode in the provided SAT solver a cover problem, either exact (i.e., find Pauli strings in the list of potential Pauli strings such that their product is exactly the target Pauli string on the considered qubits) or commuting (i.e., the product only needs to commute with the target Pauli string on the considered qubits).

Functions

encode_pauli_string_commuting_cover_sat_problem_in_solver(...)	Build the SAT problem that should be solved to find a commuting cover.
encode_pauli_string_exact_cover_sat_problem_in_solver(...)	Build the SAT problem that should be solved to find an exact cover.