Solving SAT problems with the Classiq platform on Amazon Braket

Boolean satisfiability problems (SAT) are a well-known class of difficult (NP-Complete) computational problems. The process of finding solutions to these problems can be performed using quantum computers. In this post, we will describe what SAT problems are and show you how to express SAT problems with the Classiq quantum algorithm design platform. We will outline the unique approach that Classiq takes – demonstrating how Classiq uses high-level functional modeling, synthesizes quantum circuits, and executes them on Amazon Braket. In this blog post, you’ll learn how to build and solve a SAT problem with Classiq and Amazon Braket.

Boolean satisfiability problems

SAT problems deal with finding Boolean values that, when plugged into a Boolean formula, result in that formula evaluating to TRUE. For example, if X and Y are Boolean variables, then (X AND Y) is satisfiable because X=TRUE and Y=TRUE satisfy it. In contrast, no value of X satisfies (X AND NOT X) and thus (X AND NOT X) is unsatisfiable.

SAT problems are made of clauses and literals. For instance, (A AND B) OR (C AND D AND NOT E) has two clauses: the first clause, (A AND B), has two literals (‘A’ and ‘B’) and the second clause (C AND D AND NOT E) has three literals (‘C’, ‘D’, and ‘E’). The special case where the clauses are in conjunctive normal form and each clause in the formula has at most three literals is called 3-SAT. It can be shown that any general SAT problem can be expressed as a 3-SAT problem.

From a computational complexity perspective, SAT problems are called NP-complete (short for nondeterministic polynomial-time complete). This means that they are problems where the correctness of a solution can be verified quickly, yet finding the solution itself can be hard. If the problem has many variables, brute force explorations can take significant time, exponentially increasing with the number of clauses.

Because SAT problems are NP-complete, an approach to solving these problems is applicable for any hard combinatorial problem: supply chain, packing optimizations, design verification, route planning, and many more. Improving the process for solving SAT problems would save many billions of dollars in various industries.

SAT problems are everywhere. As a concrete example, in hardware verification, designers are faced with the task of checking that a pre-silicon chip design will perform as intended. The chip logic can be mapped to a Boolean satisfiability formula together with additional assumptions on the design, and deciding satisfiability of the overall formula leads to formal proofs about the design. Moreover, this approach is commonly used in equivalence checking, model checking, and theorem proving.

In the software world, Anaconda uses SAT models to select the right combination of software package versions. For other examples of SAT problems, see the international SAT competion website.

The Classiq approach

Quantum computing offers the potential to speed up the process of solving certain problems, relative to classical computing implementations. SAT problems are an example of a problem class that can achieve quantum speed up. A straightforward way to solve a SAT problem using quantum computing is to express it in terms of a Grover search algorithm. The oracle for the Grover search serves as the engine to verify the solution, whereas the search process itself examines the entire range of possible values that might satisfy the criteria.

Let’s start with a trivial example: given two Boolean variables X, Y, can the expression X AND NOT Y be satisfied? You can easily see that X=TRUE and Y=FALSE satisfies this formula.

To envision a quantum circuit for this trivial example, let’s use the Classiq platform’s visualization. On the Classiq platform, you can navigate quantum circuit diagrams interactively. Block-level diagrams are available to show you functional components of circuits. Here is a block-level quantum oracle for this problem:

Figure 1: Block level diagram from the Classiq platform for a simple SAT problem.

The oracle receives two single-qubit variables as input: X and Y. It then inverts Y into the “NOT” of Y, and sets aux0 to be the “AND” of X AND NOT Y. Qubit aux1 is initialized to the |-⟩ state, and its phase is inverted if the Boolean expression is satisfied. Finally, qubits X, Y, and aux0 are uncomputed so they can be reused later in the circuit (the uncomputation blocks appear with a “dg” name signifying “dagger”). Overall, we can see that the oracle implements exactly what we were looking for – the input state’s phase is inverted if the expression is satisfied and is unchanged otherwise.

The circuit described in the previous block diagram can be seen in greater detail in the following full circuit:

Figure 2: Gate level from the Classiq platform showing the circuit visualized in Figure 1.

For any given Boolean expression, there are many possible oracle implementations. Since the truth table for X AND NOT Y is trivial, it might be possible to construct a simpler oracle by hand for this particular problem, but once the problems get larger and more complex, it becomes impractical to create circuits by coding at the gate-level or by assembling together pre-written blocks.

Classiq lets you run automatic synthesis of quantum circuits from high-level functional models. When using the Classiq platform, you specify two key inputs:

1. A functional decomposition of the algorithm.
2. The constraints that are important to you. For instance, you might want to limit the number of available qubits, the maximum depth of the circuit, or define a list of the native gates that should be used.

The Classiq platform then automatically explores numerous options to find circuits that meet the functional requirements and also the constraints.

The Classiq platform

As the number of qubits increases and the complexity of quantum circuits grows, we believe that existing methods of writing quantum software will be difficult to scale and would not be able to take advantage of next-generation computers. The development of classical programming languages progressed to higher level abstractions over time. At Classiq, we offer a similar approach to quantum programming: providing you with the ability to define a high-level functional model and the constraints that are important to you. The Classiq platform turns this model into an optimized, hardware-aware quantum circuit.

Classiq provides a SaaS platform that synthesizes these high-level models into quantum circuits, which can then be executed on any universal gate-based quantum computer. Models are defined either through a Pythonic interface or through an interactive plugin to Microsoft VS Code.

Figure 3. The Classiq workflow demonstrating the path from inputs to QPU

The Classiq platform generates quantum computing code in a wide variety of formats such as QASM, Q#, Cirq, QIR, and Amazon Braket. You can then deploy the output on Amazon Braket.

The Classiq platform architecture

The Classiq platform is hosted on AWS to provide Classiq customers with an easy-to-use and secure working environment. At Classiq, we use AWS solutions to help us easily develop, deploy, and maintain our product. For example, we use Amazon CloudWatch for logging, Amazon Elastic Container Registry (Amazon ECR) for container storage, Amazon Route 53 for DNS, and Amazon Elastic Kubernetes Service (Amazon EKS) for orchestrating the deployed platform.

For quantum computing, we use Amazon Braket, enabling you to work with quantum hardware comfortably and securely, conveniently integrating Classiq’s circuit synthesis capabilities with Amazon Braket’s circuit execution features. The Classiq platform connects with your AWS account when you use it to run quantum circuits on Amazon Braket using AWS Security Token Service (AWS STS) to connect the Classiq SDK.

Classiq uses Amazon Braket for two functions:

1. Fetching data from the target quantum computer – such as the number of qubits, connectivity map, and the native gates. This is performed through Amazon Braket in the Classiq account.
2. Executing quantum tasks – submitting tasks, querying the status of running tasks, and fetching results. This is performed through Amazon Braket in customers’ accounts.

Figure 4: Architecture diagram for the Classiq platform and customers’ AWS accounts, showing how Amazon Braket is used to run quantum circuits created by customers using the Classiq platform. The customer is billed for Amazon Braket through their own account, while circuit design and optimization are carried out on the Classiq platform. A secure connection between the Classiq AWS account and customer’s accounts is created using STS after being enabled by customers using a CloudFormation template provided by Classiq.

Programming a SAT problem with the Classiq SDK

Let’s examine a realistic example. Imagine that you must supplement your diet with vitamins A, B, C, and D, as well as zinc and manganese. You look at several supplement pills but discover that no single pill exists with all 100% of the desired micronutrients. Here’s what you see in the health aisle:

An additional constraint is that you don’t want to take more than one dose of vitamin A, no more than two doses of manganese, and no more than three doses of zinc. Also, there is word that Sunsate may soon be out of stock, so you want a solution that, at least for now, does not contain Sunsate.

Is there a combination in which all vitamins and minerals have been accounted for?

We can rewrite this as a SAT problem:

• Vitamin A is in Sunsate, OntraVita, or Rample, but take no more than one dose.
• Vitamin B is in Celebrane, Natriar, or OntraVita.
• Vitamin C is in Celebrane, Sunsate, or Rample.
• Vitamin D is in Sunsate, Natriar, or Rample.
• Zinc is in Celebrane, Sunsate, Natriar, or OntraVita, but take no more than three doses.
• Manganese is in Celebrane, Natriar, or Rample, but take no more than two doses.
• Sunsate should not be taken alone.
• Sunsate is out of stock.

With some refactoring, we can write out this problem in terms of Boolean clauses:

• Sunsate OR OntraVita OR Rample
• Celebrane OR Natiar OR OntraVita
• Celebrane OR Sunsate OR Rample
• Sunsate OR Natriar OR Rample
• Celebrane OR Sunsate OR Natriar OR OntraVita
• NOT (Celebrane AND Sunsate AND Natriar AND OntraVita)
• NOT Sunsate OR Celebrane OR Natriar OR Rample OR Ontravita
• NOT (Sunsate OR OntraVita AND Rample)
• NOT (Celebrane AND Natriar AND Rample)

While converting these Boolean clauses into quantum circuits may be a complex task, the Classiq SDK makes it easy for you. Here is how it’s done.

Step 1: Define the SAT problem

Define and allocate qubits for your variables. A 1 qubit register is allocated for each Boolean variable.

from classiq_interface.generator.arith.arithmetic 
import RegisterUserInput
celebrane = RegisterUserInput(size=1)
sunsate = RegisterUserInput(size=1)
natriar = RegisterUserInput(size=1)
ontravita = RegisterUserInput(size=1)
rample = RegisterUserInput(size=1)
variables = {
    "celebrane": celebrane,
    "sunsate": sunsate,
    "natriar": natriar,
    "ontravita": ontravita,
    "rample": rample
    }

Create a string that defines the expression that defines the SAT problem using the variables that you’ve specified.

clauses = []
clauses.append("(sunsate | ontravita | rample)")  # Vitamin A
clauses.append("(celebrane | natriar | ontravita)")  # Vitamin B
clauses.append("(celebrane | sunsate | rample)")  # Vitamin C
clauses.append("(sunsate | natriar | rample)")  # Vitamin D
clauses.append("(celebrane | sunsate | natriar | ontravita)")  # Zinc
clauses.append("(celebrane | natriar | rample)")  # Manganese
clauses.append("(~(celebrane & sunsate & natriar & ontravita))")  # Mustn't take more than 3 doses of Zinc
clauses.append("(~sunsate | celebrane | natriar | rample | ontravita)")  # Sunsate should not be taken alone
clauses.append("(~(sunsate | ontravita & rample))")  # Mustn't take more than 1 dose of Vitamin A. Sunsate is out of stock
clauses.append("(~(celebrane & natriar & rample))")  # Mustn't take more than 2 doses of Manganese
combined_clauses = " & ".join(clauses)
expression = f"({combined_clauses}) == 1"
print(expression)

The final expression is a string that defines the SAT problem, which is

((sunsate | ontravita | rample) & (celebrane | natriar | ontravita) & (celebrane | sunsate | rample) & (sunsate | natriar | rample) & (celebrane | sunsate | natriar | ontravita) & (celebrane | natriar | rample) & (~(celebrane & sunsate & natriar & ontravita)) & (~sunsate | celebrane | natriar | rample | ontravita) & (~(sunsate | ontravita & rample)) & (~(celebrane & natriar & rample))) == 1.

Now, you can use the Classiq platform to create a quantum circuit to solve this.

The Classiq platform ingests this model and a list of desired operational constraints. The platform then creates a possible “solution space” for the resulting circuit that it designs by using a variety of methods, including:

1. Selecting the algorithm that implements each functional block
2. Finding the right choice of auxiliary qubits vs. number of gates and depth
3. Changing the order of the functions, since some functions commute
4. Reusing auxiliary qubits at expense of uncomputation

Each of the possible circuits that implement the required functionality and satisfies the constraints might use a different number of qubits and gates. Classiq’s automatic synthesis engine explores the solution space to find the circuit with optimal circuit depth and qubit count.

Step 2: Define a quantum oracle

To solve your SAT problem, define a quantum oracle – a quantum circuit that receives the defined quantum registers as inputs and multiplies the state vector by -1 if it satisfies a certain condition. The condition is the Boolean expression created previously. If the state vector doesn’t satisfy the Boolean expression, it leaves it unchanged.

To create your oracle, initialize a ModelDesigner object, which compiles your code and generates a quantum circuit.

from classiq import ModelDesigner
from classiq_interface.generator.function_param_list import ArithmeticOracle
model_designer = ModelDesigner()
arithmetic_oracle=ArithmeticOracle(expression=expression, definitions=variables)
model_designer.ArithmeticOracle(params=arithmetic_oracle)
oracle_circuit = model_designer.synthesize()

A show_interactive() function can now be used to create an interactive visualization of the circuit.

oracle_circuit.show_interactive()

You can explore this example’s resulting circuit interactively here. These interactive circuits are expandable – click on the “+” sign to expand each block.

You can also check the depth and qubit count of the result by printing the relevant properties of your circuit.

print("Circuit depth: ", oracle_circuit.depth)
Circuit depth : 473
print("Qubit count: ", oracle_circuit.qubit_count)
Qubit Count: 43

This is a big circuit that uses 43 qubits. Fortunately, we can ask our ModelDesigner to synthesize an optimized circuit using fewer qubits by simply adding the method=”optimized” property during the ArithmeticOracle initialization.

model_designer = ModelDesigner()
model_designer.ArithmeticOracle(
    params=ArithmeticOracle(
        expression=expression, 
        definitions=variables, 
        method="optimized"
        )
    )
oracle_circuit = model_designer.synthesize()

The resulting oracle only uses 23 qubits, at the cost of a slightly deeper circuit, 481 gates as opposed to 473 gates in the unoptimized circuit. Take a moment and compare the interactive diagram for this unoptimized circuit with the interactive diagram for the optimized circuit.

Step 3: Execute Grover’s algorithm

When you have an oracle that you’re happy with, use it to execute Grover’s algorithm. You can run the circuit on Amazon Braket QPUs or simulators using Classiq’s Executor. This example uses the SV1 simulator. When using this code, replace YOUR_AWS_ROLE with the ARN of an IAM role with access to Amazon Braket.


from classiq import Executor
from classiq_interface.generator.function_param_list import GroverOperator
from classiq_interface.executor.execution_preferences import ExecutionPreferences, AmplitudeAmplification
from classiq_interface.backend.backend_preferences import AwsBackendPreferences
preferences = ExecutionPreferences(
    amplitude_amplification=AmplitudeAmplification(iterations=1),
    backend_preferences=AwsBackendPreferences(
        backend_name="SV1",
        aws_role_arn="YOUR_AWS_ROLE"
        )
    )
executor = Executor(preferences=preferences)
res = executor.execute_generated_circuit(generation_result=grover_circuit)
print(res)

You can validate that the result satisfies the vitamin problem defined in the preceding code block by comparing this result with the table and constraints that define the solution.

GroverSimulationResults(
    result={
        'sunsate': 0.0, 
        'rample': 1.0, 
        'ontravita': 0.0, 
        'celebrane': 0.0, 
        'natriar': 1.0
        }
    )

The output says that you’ll need 1 dose of Rample and one dose of Natriar to achieve your objective vitamin regimen.

Summary

SAT problems are important problems, and in this post, we showed several ways of solving them using the Classiq platform and Amazon Braket. To test drive the Classiq platform, reach out to Classiq at hello@classiq.io or on the Classiq evaluation request website. For more information on Classiq, please visit www.classiq.io.