# ---
# jupyter:
#   jupytext:
#     text_representation:
#       extension: .py
#       format_name: light
#       format_version: '1.5'
#       jupytext_version: 1.14.4
#   kernelspec:
#     display_name: Python 3
#     language: python
#     name: python3
# ---

# + [markdown] id="71mQEXWm964S"
# <a href="https://www.peqnp.com"><img border="0" alt="PEQNP" src="https://raw.githubusercontent.com/maxtuno/SATX/main/SAT-X.jpg" width="640" height="400">
#
# # SAT-X 
# ## [![Downloads](https://pepy.tech/badge/satx)](https://pepy.tech/project/satx) 
# ### The constraint modeling language for SAT solvers
#
# SAT-X is a language for constrained optimization and decision problems over positive integers, that work with any SAT Competition standard SAT solver. Is based on Python, and is ase to learn and easy to use with all technologies associated to this language.
#
# # Some excelent SAT Solvers
#
# 1- https://github.com/maxtuno/SLIME (standalone and cloud [MPI] - Oscar Riveros)
#
# 2- https://github.com/arminbiere/kissat (The Kissat SAT Solver - <NAME>)
#
# 3- https://github.com/maxtuno/MiniSat (MiniSat 2.2.0 with DRUP proof, CMake and StarExec Ready. -  <NAME>, <NAME>)
#
# 4- https://github.com/maxtuno/blue (A Powerful SAT Solver for Java - Oscar Riveros)
#
# 5- Any SAT Solver with the SAT Competition standars. (http://www.satcompetition.org)

# + [markdown] id="JzM69hBn964T"
# # INSTALLATION
# ```python
# pip install SATX
# ```

# + colab={"base_uri": "https://localhost:8080/"} id="GMnjfDhU_EEc" tags=[] outputId="b0e32304-9ed8-4a6f-e484-0a4353f722ed"
# !pip install SATX --upgrade --force

# + [markdown] id="n71dPAXZecdj"
# # INTRODUCION
# On SAT-X all elements are integers, the relations are at bit level or arithmetic level. All integers live on $\mathbb{N}_{2 ^ {bits} - 1}$ and always positives, i.e. for two integer $(x, y)$ the operation, $(x - y)$ take all possibilities such that $x - y >= 0$.
#
# # SUPPORTED OPERATIONS
# $+$, $-$, $*$, $/$, $**$, $abs$, $powmod$, $\%$, $\&$, $|$, $^$, $==$, $=$, $<$, $<=$, $>$, $>=$

# + [markdown] id="Kd2ebfRUkjre"
# # FIND ALL SOLUTIONS TO $2^n-7=x^2$
#
# Ref: http://www.artofproblemsolving.com/Forum/viewtopic.php?t=66245

# + colab={"base_uri": "https://localhost:8080/"} id="vY7upZWNkoS_" outputId="9f8f8a9d-d151-4507-82cb-60796de01e22"
import satx

satx.engine(32, cnf_path='tmp.cnf')

_2 = satx.constant(2)
n = satx.integer()
x = satx.integer()

assert _2 ** n - 7 == x ** 2

while satx.satisfy('slime'):
    print(n, x)

# + [markdown] id="RbN-rZnek7Dl"
# SOLVE IN POSITIVE INTEGERS THE FOLLOWING EQUATION: $n^3 − 5n + 10 = 2^k$.
#
# Ref: http://www.artofproblemsolving.com/Forum/viewtopic.php?t=103239
#
# tip: avoid the negative signs

# + colab={"base_uri": "https://localhost:8080/"} id="yOQyM4QslOAz" outputId="b4f30395-8651-46fc-ff82-152cf1fd0155"
import satx

satx.engine(16, cnf_path='tmp.cnf')

_2 = satx.constant(2)

n = satx.integer()
k = satx.integer()

assert n ** 3 + 10 == _2 ** k + 5 * n

while satx.satisfy('slime'):
    print(n, k)

# + [markdown] id="AcGfS1eRlT6U"
# # FIND ALL POSITIVE INTEGER SOLUTIONS TO $a^{2}=b^{3}+1$
#
# Ref: http://www.artofproblemsolving.com/Forum/viewtopic.php?t=103239

# + colab={"base_uri": "https://localhost:8080/"} id="V8LEjkg3lYP7" outputId="6f299539-084c-43c1-9fee-8233b24e147a"
import satx

satx.engine(16, cnf_path='tmp.cnf')

a = satx.integer()
b = satx.integer()

assert a ** 2 == b ** 3 + 1

while satx.satisfy('slime'):
    print(a, b)

# + [markdown] id="3EWbG3SMlbOs"
# # FIND ALL POSITIVE INTEGER SOLUTIONS TO  $x,y$: $3^x - 1 == y2^x + 1$
#
# ref: http://www.artofproblemsolving.com/Forum/viewtopic.php?t=31947

# + colab={"base_uri": "https://localhost:8080/"} id="Ci3EZWlYlhV5" outputId="4b0fa28f-8938-4309-efa1-fd64ec0e2094"
import satx

satx.engine(32, cnf_path='tmp.cnf')

_2 = satx.constant(2)
_3 = satx.constant(3)

x = satx.integer()
y = satx.integer()

assert _3 ** x == y * _2 ** x + 1

while satx.satisfy('slime'):
    print(x, y)

# + [markdown] id="aiWphw2k964V"
# # INTEGER FACTORIZATION
# In number theory, integer factorization is the decomposition of a composite number into a product of smaller integers. If these factors are further restricted to prime numbers, the process is called prime factorization.

# + colab={"base_uri": "https://localhost:8080/"} id="7S96pDBk964W" tags=[] outputId="93c578c4-6343-4574-da32-cc3603e20567"
import satx

rsa = 3007

satx.engine(rsa.bit_length(), cnf_path='tmp.cnf')

p = satx.integer()
q = satx.integer()

assert p * q == rsa

while satx.satisfy('slime'):
    print(p, q)

# + [markdown] id="kpXoFzLi2PVw"
# # PALINDROMIC NUMBERS (Bits Level)

# + colab={"base_uri": "https://localhost:8080/"} id="6EU_vqh-1hIG" outputId="f82de897-c78e-4f01-d0a6-6dd5865e4e03"
import numpy as np
import satx

satx.engine(10, cnf_path='tmp.cnf')

x = satx.integer()

# without "copy" for inplace reverse of bits
assert x == x.reverse(copy=True)

while satx.satisfy('slime'):
    print(x, np.binary_repr(x.value, satx.bits()))

# + [markdown] id="9sIHVlpNt1qX"
# # XOR Problem
#
# The XOr, or “exclusive or”, problem is a classic problem in ANN research. It is the problem of using a neural network to predict the outputs of XOr logic gates given two binary inputs. An XOr function should return a true value if the two inputs are not equal and a false value if they are equal.

# + colab={"base_uri": "https://localhost:8080/"} id="AeFgWSlAtu95" outputId="54b06e4e-7e5d-40ab-dec8-1937b6a08f8c"
import satx

x = [[0, 0], [0, 1], [1, 0], [1, 1]]
y = [0, 1, 1, 0]

n, m = len(x), len(x[0])

satx.engine(10, cnf_path='tmp.cnf')

w = satx.matrix(dimensions=(n, m))
b = satx.vector(size=n)

for i in range(n):
    assert y[i] == satx.dot(x[i], w[i]) + b[i]

if satx.satisfy('slime'):
    for i in range(n):
        print(x[i], satx.dot(x[i], w[i]) + b[i])
else:
    print('Infeasible ...')

# + [markdown] id="-BeLNuT8COAO"
# # ABSOLUTE VALUES

# + colab={"base_uri": "https://localhost:8080/"} id="vB2QHUbPCOAP" outputId="d0a90421-6325-4320-8984-7e6185ef74f5"
import satx

satx.engine(4, cnf_path='tmp.cnf')

x = satx.integer()
y = satx.integer()

assert abs(x - y) == 1

assert x != satx.oo()
assert y != satx.oo()

while satx.satisfy('slime'):
    print(x, y, x - y, abs(x - y))

# + [markdown] id="LrPaLRqeOjkg"
# # CENTROID

# + colab={"base_uri": "https://localhost:8080/", "height": 280} id="zeVnsPPqOnPX" outputId="87434b91-c7b1-4c4e-fc8b-18bc20e93558"
import numpy as np
import satx
import matplotlib.pyplot as plt

n = 15

data = np.random.randint(0, 10, size=(n, 2))

opt = 1
while True:
    satx.engine(10, cnf_path='tmp.cnf')

    x = satx.integer()
    y = satx.integer()

    assert sum(abs(xy[0] - x) + abs(xy[1] - y) for xy in data) < opt
    
    assert x != satx.oo()
    assert y != satx.oo()

    if satx.satisfy('slime'):        
        print(x, y)
        a, b = zip(*data)
        plt.plot(a, b, '.')
        plt.plot(x, y, 'x')
        plt.show()
        break
    else:
        opt += 1

# + [markdown] id="oWFt1q0XV-7j"
# # FERMAT'S FACTORIZATION METHOD
#
# Note: when there is a negative number in the model, increment the bits by 1.

# + colab={"base_uri": "https://localhost:8080/"} id="k01dOcjOVk9w" tags=[] outputId="d39152c4-15a5-4d95-d825-40c34688f944"
import satx

rsa = 3007

satx.engine(rsa.bit_length() + 1, cnf_path='tmp.cnf')

p = satx.integer()
q = satx.integer()

assert p ** 2 - q ** 2 == rsa
assert q < p

if satx.satisfy('slime'):
    print(p, q, p + q, p - q)
else:
    print('Is Prime!')

# + [markdown] id="GgE1AgRiYmij"
# # EXPONENTIAL DIOPHANTINE EQUATIONS
#

# + colab={"base_uri": "https://localhost:8080/"} id="XU0I3MnZYu-x" tags=[] outputId="91f586df-131a-4669-9107-86f47365a056"
import satx

satx.engine(10, cnf_path='tmp.cnf')

x = satx.integer()
y = satx.integer()
z = satx.integer()

satx.apply_single([x, y, z], lambda t: t != 0)

assert x ** y == z

while satx.satisfy('slime'):
    print(x, y, z)

# + [markdown] id="EUBndQTWCOAd"
# # ON THE DIOPHANTINE EQUATION $x^2 + c = 3^n$ WITH $x, c, n > 1$

# + colab={"base_uri": "https://localhost:8080/"} id="yTLNkcWACOAd" tags=[] outputId="e3f397de-9eeb-48c5-9ab7-52a209d27a5b"
import satx

n = 32

satx.engine(n.bit_length(), cnf_path='tmp.cnf')

_3 = satx.constant(3)
n = satx.integer()
x = satx.integer()
c = satx.integer()

assert x ** 2 + c == _3 ** n
assert x > 1
assert c > 1
assert n > 1

if satx.satisfy('slime'):
    print(n, x, c)
else:
    print('Infeasible for bit range...')

# + [markdown] id="8EJXiM2FCOAh"
# # FACTORIALS

# + colab={"base_uri": "https://localhost:8080/"} id="iwack4VxCOAh" outputId="1fff8b25-1dd2-4701-e98f-1e0eb4f4a7f6"
import math
import satx

satx.engine(32, cnf_path='tmp.cnf')

x = satx.integer()

satx.factorial(x) == math.factorial(10)

if satx.satisfy('slime'):
    print(x)
else:
    print('Need more bits!')

# + [markdown] id="O4gi4qEGCOAk"
# # $\Sigma$

# + colab={"base_uri": "https://localhost:8080/"} id="MANm7Pu8COAl" outputId="01a54a59-5712-4ba6-8753-48b891aa7473"
import satx

satx.engine(16, cnf_path='tmp.cnf')

x = satx.integer()
n = satx.integer()

satx.sigma(lambda k: k ** 2, 1, n) == x

while satx.satisfy('slime'):
    print(x, n, sum(k ** 2 for k in range(1, n.value + 1)))


# + [markdown] id="VWgIBrvZCOAn"
# # $\Pi$

# + colab={"base_uri": "https://localhost:8080/"} id="TxIWHtjXCOAo" outputId="0a65013f-b102-49a8-e2d9-a6263a5a1dbc"
import functools
import operator
import math
import satx

satx.engine(32, cnf_path='tmp.cnf')

x = satx.integer()
n = satx.integer()

satx.pi(lambda k: k ** 2, 1, n) == x
assert 0 < x <= 2 ** math.log(satx.oo()) # limit the CNF overflow
assert n > 0

while satx.satisfy('slime'):
    print(x, n, functools.reduce(operator.mul, (k ** 2 for k in range(1, n.value + 1))))

# + [markdown] id="dq3QrO15MjGZ"
# # SAT-X VS FIBONACCI NUMBERS | N VS TIME

# + colab={"base_uri": "https://localhost:8080/", "height": 1000} id="hmnhjMXsMm3n" outputId="0e0f8107-d77c-457a-c121-fe7ec430e7b3"
import time
import satx
import matplotlib.pyplot as plt

ns, ts = [], []
for n in range(2, 100):

    satx.engine(n, cnf_path='tmp.cnf')

    x = satx.vector(size=n + 1)

    assert x[0] == 0
    assert x[1] == 1
    for i in range(2, n + 1):
        assert x[i - 1] + x[i - 2] == x[i]

    ini = time.time()
    if satx.satisfy('slime'):
        print(n, x[n])
    else:
        print('Infeasible ...')
    end = time.time()
    ns.append(n)
    ts.append(end - ini)

plt.title('SAT-X vs Fibonacci Numbers | n vs time')
plt.plot(ns, ts)
plt.show()

# + [markdown] id="fkO7OMupWbBy"
# # TENSORS
#
# Tensors object are the most advanced concept behind SAT-X, integers are tensors, work like integers, but their bits act like an multidimensional matrix of lambda functions.
#
# Note: [[*]] for acces to lambda (bit) functions.

# + colab={"base_uri": "https://localhost:8080/"} id="RR7JLifNZo95" outputId="23b1b73c-4785-4a11-a8d0-022fed5229e9"
import satx

satx.engine(10, cnf_path='tmp.cnf')

x = satx.tensor(dimensions=(4))
y = satx.tensor(dimensions=(2, 2))

assert x + y == 10
assert x[[0]](0, 1) == 1
assert y[[0, 0]](0, 1) == 1

while satx.satisfy('slime'):
    print(x, y, x.binary, y.binary)

# + colab={"base_uri": "https://localhost:8080/"} id="upsI_STPaZee" outputId="dbf79ef4-8d6f-4f62-d493-ff774f9778fd"
import numpy as np
import satx

n = 2

satx.engine(4, cnf_path='tmp.cnf')

x = satx.tensor(dimensions=(n, n))
a = satx.integer()
b = satx.integer()

assert sum(x[[i, j]](a ** 2 - b ** 3, a ** 3 - b ** 2) for i in range(n) for j in range(n)) == 0

while satx.satisfy('slime'):
    print(a, b)
    print(np.vectorize(int)(x.binary))
    print()

# + [markdown] id="yfhZFB3BXuNH"
# # RSA FACTORIZATION WITH TENSORS

# + colab={"base_uri": "https://localhost:8080/"} id="67L02LcOWKSV" outputId="1db60e2a-cd23-4fc5-a24e-bf30840f1974"
import satx

rsa = 3007

satx.engine(rsa.bit_length(), cnf_path='tmp.cnf')

p = satx.tensor(dimensions=(satx.bits()))
q = satx.tensor(dimensions=(satx.bits()))

assert p * q == rsa
assert p[[0]](0, 1) == 1
assert q[[0]](0, 1) == 1
assert sum(p[[i]](0, 1) for i in range(satx.bits() // 2 + 1, satx.bits())) == 0
assert sum(q[[i]](0, 1) for i in range(satx.bits() // 2, satx.bits())) == 0

if satx.satisfy('slime'):
    print(p, q)
else:
    print('Is Prime!')

# + [markdown] id="U7_zMGVNXVnh"
# # SAT REFORMULATION WITH TENSORS

# + colab={"base_uri": "https://localhost:8080/"} id="fFW0JlyaXMRO" outputId="9368de74-ae6e-4690-d47c-4e77ae040871"
import functools
import operator
import sys

import satx


n, m, sat = 10, 24, [[9, -5, 10, -6, 3],
                     [6, 8],
                     [8, 4],
                     [-10, 5],
                     [-9, 8],
                     [-9, -3],
                     [-2, 5],
                     [6, 4],
                     [-2, -1],
                     [7, -2],
                     [-9, 4],
                     [-1, -10],
                     [-3, 4],
                     [7, 5],
                     [6, -3],
                     [-10, 7],
                     [-1, 7],
                     [8, -3],
                     [-2, -10],
                     [-1, 5],
                     [-7, 1, 9, -6, 3],
                     [-9, 6],
                     [-8, 10, -5, -4, 2],
                     [-4, -7, 1, -8, 2]]


if __name__ == '__main__':
    
    satx.engine(bits=1, cnf_path='tmp.cnf')
    
    x = satx.tensor(dimensions=(n,))
    
    assert functools.reduce(operator.iand, (functools.reduce(operator.ior, (x[[abs(lit) - 1]](lit < 0, lit > 0) for lit in cls)) for cls in sat)) == 1
    
    if satx.satisfy('slime'):
        print('SAT')
        print(' '.join(map(str, [(i + 1) if b else -(i + 1) for i, b in enumerate(x.binary)])) + ' 0')
    else:
        print('')

# + [markdown] id="9hQcWGrRX1Wg"
# # SUM SUBSET PROBLEM WITH TENSORS

# + colab={"base_uri": "https://localhost:8080/"} id="p5khFp70X6a_" outputId="a6fe42da-a7ee-4745-a09c-2b359bf9f9c5"
import numpy as np
import satx

universe = np.random.randint(1, 2 ** 16, size=100)
t = np.random.randint(min(universe), sum(universe))

satx.engine(t.bit_length(), cnf_path='tmp.cnf')

x = satx.tensor(dimensions=(len(universe)))

assert sum(x[[i]](0, universe[i]) for i in range(len(universe))) == t

if satx.satisfy('slime'):
    sub = [universe[i] for i in range(len(universe)) if x.binary[i]]
    print(t, sum(sub), sub)
else:
    print('Infeasible ...')

# + [markdown] id="lxKWdGrI964h"
# # MULTISET RECONSTRUCTION BY DIFFERENCES
#
# Given a sorted multiset, their differences and one tip (an element and position for only one arbitrary element), is possible recovery the original multiset?

# + colab={"base_uri": "https://localhost:8080/"} id="sDtWaw6l964i" outputId="681dbd6c-d8f6-4d32-b69e-3de1e983d0c7"
import time
import random
import satx


def generator(n, max_val):
    return sorted([random.randint(1, max_val) for _ in range(n)])


def differences(lst):
    return [abs(lst[i] - lst[i - 1]) for i in range(1, len(lst))]


# 100 tests
for n in range(1, 10):

    m = random.randint(1, n ** 2)

    original = generator(n, m)
    diffs = differences(original)

    print('N, M         : {}, {}'.format(n, m))
    print('DIFFERENCES  : {}'.format(diffs))
    print('ORIGINAL     : {}'.format(original))

    # only one tip
    ith = random.choice(range(n))
    tip = original[ith]

    # init timer
    ini = time.time()

    # Empirical bits necessarily to solve the problem.
    satx.engine(sum(diffs).bit_length() + 4, cnf_path='tmp.cnf')

    # Declare a n-vector of integer variables to store the solution.
    x = satx.vector(size=n)

    # The tip is on x at index ith
    assert tip == satx.index(ith, x)

    # The i-th element of the instance is the absolute difference of two consecutive elements
    for i in range(n - 1):
        assert x[i] <= x[i + 1]
        assert satx.index(i, diffs) == x[i + 1] - x[i]

    # Solve the problem for only one solution
    # Turbo parameter is a destructive simplification
    # Solve with all power os SLIME SAT Solver but only for the fist solution.
    if satx.satisfy('slime'):
        o = [abs(x[i + 1] - x[i]) for i in range(n - 1)]
        c = 100 * len(set(map(int, x)).intersection(set(original))) / len(set(original))
        print('SOLVED       : {}'.format(x))
        print('COINCIDENCES : {}%'.format(c))
        if o == diffs:
            print('OK! - {}s'.format(time.time() - ini))
        else:
            print('NOK! - {}s'.format(time.time() - ini))
            raise Exception('ERROR!')
        if c != 100:
            raise Exception('Hypothesis Fail - 100%')

# + [markdown] id="c2MllZ2i964r"
# # DIOPHANTINE EQUATIONS
#
# https://en.wikipedia.org/wiki/Diophantine_equation

# + [markdown] id="DK1DC7aE964s"
# ### Let be $x, y \in \mathbb{N} \vert x^3 - x + 1 = y^2$

# + colab={"base_uri": "https://localhost:8080/"} id="7bgCxLRI964t" outputId="4ca3a6ee-2765-4aca-de04-15c07a5ef656"
import satx

satx.engine(10, cnf_path='tmp.cnf')

x = satx.integer()
y = satx.integer()

assert x ** 3 - x + 1 == y ** 2

assert x != 0
assert y != 0

while satx.satisfy('slime'):
    print('{0} ** 3 - {0} + 1, {1} ** 2'.format(x, y))

# + [markdown] id="tXkkLVGl964w"
# ### Let be $x, y \in \mathbb{Q} \vert x^3 + xy = y^2$

# + colab={"base_uri": "https://localhost:8080/"} id="p84V_ORl964w" outputId="b5bddbb7-b512-4f97-9e5e-1c28218bd450"
import satx

satx.engine(10, cnf_path='tmp.cnf')

x = satx.rational()
y = satx.rational()

assert x ** 3 + x * y == y ** 2
assert x != 0
assert y != 0

while satx.satisfy('slime'):
    print('{0} ** 3 + {0} * {1} == {1} ** 2'.format(x, y))

# + [markdown] id="ijexlhdd9642"
# # Vectors

# + colab={"base_uri": "https://localhost:8080/", "height": 263} id="QNWHLqHS9644" outputId="03e99a57-06b1-4e5b-bbdb-29650a1a4507"
import numpy as np
import satx
import matplotlib.pyplot as plt

dim = 2

satx.engine(5, cnf_path='tmp.cnf')

ps = satx.vector(size=dim, is_rational=True)

assert sum([p ** dim for p in ps]) <= 1

dots = []
while satx.satisfy('slime'):
    dots.append(np.vectorize(float)(ps))

x, y = zip(*dots)
plt.axis('equal')
plt.plot(x, y, 'r.')
plt.show()

# + [markdown] id="C0lkauin9646"
# # NP-COMPLETE PROBLEMS
#
# NP-Complete problem, any of a class of computational problems for which no efficient solution algorithm has been found. Many significant computer - science problems belong to this class—e.g., the traveling salesman problem, satisfiability problems, and graph - covering problems.
#
# https://en.wikipedia.org/wiki/NP-completeness

# + [markdown] id="hJQDg3rb9647"
# # SATISFIABILITY
#
# Study of boolean functions generally is concerned with the set of truth assignments(assignments of 0 or 1 to each of the variables) that make the function true.
#
# https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

# + colab={"base_uri": "https://localhost:8080/"} id="GR62G6M99647" outputId="0148d75e-63a6-4b1f-b023-c17a549a6b10"
import functools
import operator

import satx

n, m, sat = 10, 24, [[9, -5, 10, -6, 3],
                     [6, 8],
                     [8, 4],
                     [-10, 5],
                     [-9, 8],
                     [-9, -3],
                     [-2, 5],
                     [6, 4],
                     [-2, -1],
                     [7, -2],
                     [-9, 4],
                     [-1, -10],
                     [-3, 4],
                     [7, 5],
                     [6, -3],
                     [-10, 7],
                     [-1, 7],
                     [8, -3],
                     [-2, -10],
                     [-1, 5],
                     [-7, 1, 9, -6, 3],
                     [-9, 6],
                     [-8, 10, -5, -4, 2],
                     [-4, -7, 1, -8, 2]]

satx.engine(bits=1, cnf_path='tmp.cnf')
x = satx.tensor(dimensions=(n,))
assert functools.reduce(operator.iand, (functools.reduce(operator.ior, (x[[abs(lit) - 1]](lit < 0, lit > 0) for lit in cls)) for cls in sat)) == 1
if satx.satisfy('slime'):
    print('SAT')
    print(' '.join(map(str, [(i + 1) if b else -(i + 1) for i, b in enumerate(x.binary)])) + ' 0')
else:
    print('UNSAT')

# + [markdown] id="-rrrwc0V9649"
# # k-CLIQUE
#
# Input: Graph $G$, positive integer $k$
#
# Property: $G$ has a set of mutually adjacent nodes.
#
# https://en.wikipedia.org/wiki/Clique_problem

# + colab={"base_uri": "https://localhost:8080/"} id="QQDWim1w9649" outputId="446f9348-07b5-458a-f02a-e4e905df2795"
import satx

# Ths bits of the clique to search
k = 3

# Get the graph, and the dimension for the graph
n, matrix = 5, [(1, 0), (0, 2), (1, 4), (2, 1), (4, 2), (3, 2)]

# Ensure the problem can be represented
satx.engine(bits=k.bit_length(), cnf_path='tmp.cnf')

# Declare an integer of n-bits
bits = satx.integer(bits=n)

# The bits integer have "bits"-active bits, i.e, the clique has "bits"-elements
assert sum(satx.switch(bits, i) for i in range(n)) == k

# This entangles all elements that are joined together
for i in range(n - 1):
    for j in range(i + 1, n):
        if (i, j) not in matrix and (j, i) not in matrix:
            assert satx.switch(bits, i) + satx.switch(bits, j) <= 1

if satx.satisfy('slime'):
    print(k)
    print(' '.join([str(i) for i in range(n) if not bits.binary[i]]))
else:
    print('Infeasible ...')

# + [markdown] id="W9A_lLrn964_"
# # VERTEX COVER
#
# In the mathematical discipline of graph theory, a vertex cover (sometimes node cover) of a graph is a set of vertices that includes at least one endpoint of every edge of the graph. The problem of finding a minimum vertex cover is a classical optimization problem in computer science and is a typical example of an NP-hard optimization problem that has an approximation algorithm. Its decision version, the vertex cover problem, was one of Karp's 21 NP-complete problems and is therefore a classical NP-complete problem in computational complexity theory. Furthermore, the vertex cover problem is fixed-parameter tractable and a central problem in parameterized complexity theory.
#
# https://en.wikipedia.org/wiki/Vertex_cover

# + colab={"base_uri": "https://localhost:8080/"} id="qaxFZxFL965A" outputId="ab6be7fc-2fda-4a19-a5b4-46f756a1b083"
import satx

# Get the graph and dimension, and the bits of the cover.
n, graph, vertex, k = 5, [(1, 0), (0, 2), (1, 4), (2, 1), (4, 2), (3, 2)], [0, 1, 2, 3, 4], 3

# Ensure the problem can be represented
satx.engine(bits=n.bit_length() + 1, cnf_path='tmp.cnf')

# An integer with n-bits to store the indexes for the cover
index = satx.integer(bits=n)

# This entangled the all possible covers
for i, j in graph:
    assert satx.switch(index, vertex.index(i), neg=True) + satx.switch(index, vertex.index(j), neg=True) >= 1

# Ensure the cover has bits k
assert sum(satx.switch(index, vertex.index(i), neg=True) for i in vertex) == k

if satx.satisfy('slime'):
    opt = sum(index.binary)
    print('p bits {}'.format(opt))
    print(' '.join([str(vertex[i]) for i in range(n) if index.binary[i]]))
else:
    print('Infeasible ...')

# + [markdown] id="-Itdoe64965B"
# # MULTIDIMENSIONAL LATIN SQUARES
#
# In combinatorics and in experimental design, a Latin square is an n × n array filled with n different symbols, each occurring exactly once in each row and exactly once in each column.
#
# https://en.wikipedia.org/wiki/Latin_square

# + colab={"base_uri": "https://localhost:8080/"} id="ZobMPYao965C" outputId="ac143817-b05b-4b66-9f94-b5b2afef40cb"
import numpy as np
import satx

n = 6
m = 3

satx.engine(n.bit_length(), cnf_path='tmp.cnf')

Y = satx.vector(size=n ** m)

satx.apply_single(Y, lambda k: k < n)

Y = np.reshape(Y, newshape=(m * [n]))

for i in range(n):
    satx.all_different(Y[i])
    satx.all_different(Y.T[i])
    for j in range(n):
        satx.all_different(Y[i][j])
        satx.all_different(Y.T[i][j])

for idx in satx.hyper_loop(m - 1, n):
    s = Y
    for i in idx:
        s = s[i]
        satx.all_different(s)
        satx.all_different(s.T)

if satx.satisfy('slime'):
    y = np.vectorize(int)(Y).reshape(m * [n])
    print(y)
else:
    print('Infeasible ...')

# + [markdown] id="bbdyVi1o965E"
# # TRAVELLING SALESMAN PROBLEM WITH HESS ALGORITHM (<NAME>)
#
# https://independent.academia.edu/oarr
#
# The travelling salesman problem asks the following question: "Given a list of cities and the distances between each pair of cities, what is the shortest possible route that visits each city and returns to the origin city?" It is an NP-hard problem in combinatorial optimization, important in operations research and theoretical computer science.
#
# https://en.wikipedia.org/wiki/Travelling_salesman_problem
#
# SAT-X include a full implementation of the HESS black-box algorithm for more advanced examples see here https://github.com/maxtuno/hess

# + colab={"base_uri": "https://localhost:8080/", "height": 263} id="3CHTjOaA965E" outputId="57a18fb9-f89b-44ee-fd1c-f2c616bce260"
import satx
import numpy as np
import matplotlib.pyplot as plt

n = 100
data = np.random.logistic(size=(n, 2))
seq = satx.hess_sequence(n, oracle=lambda seq: sum(np.linalg.norm(data[seq[i - 1]] - data[seq[i]]) for i in range(n)), fast=False)
x, y = zip(*[data[i] for i in seq + [seq[0]]])
plt.plot(x, y, 'k-')
plt.plot(x, y, 'r.')
plt.show()

# + id="3f8ACnp_JBHb" outputId="6699b42e-654f-4421-dfa0-330710305041"
import numpy as np
import satx
import matplotlib.pyplot as plt


n = 10

data = np.random.randint(0, 10, size=(n, 2))
matrix = np.zeros(shape=(n, n))
for i in range(n):
    for j in range(n):
        matrix[i][j] = int(np.linalg.norm(data[i] - data[j]))

opt = satx.oo() - 1
while True:
    satx.engine(int(sum(matrix.flatten())).bit_length() + 1, cnf_path='tmp.cnf')
    x, y = satx.matrix_permutation(matrix.flatten(), n)
    assert sum(y) < opt
    if satx.satisfy('slime'):
        opt = sum(y)
        print(opt, x, y)

        a, b = zip(*[data[i.value] for i in x + [x[0]]])
        plt.plot(a, b, 'ro')
        plt.plot(a, b, 'k-')
        plt.show('tsp.png')
        plt.close()

        satx.clear(x)
        satx.clear(y)
    else:
        break

# + [markdown] id="3CaSxvbE965I"
# # MAGIC SQUARE
#
#
# In recreational mathematics and combinatorial design, a magic square is a $n\times n$ square grid (where n is the number of cells on each side) filled with distinct positive integers in the range 
# ${1,2,...,n^{2}}$ such that each cell contains a different integer and the sum of the integers in each row, column and diagonal is equal.
#
# https://en.wikipedia.org/wiki/Magic_square

# + colab={"base_uri": "https://localhost:8080/"} id="AyWeR36j965I" outputId="943a5c1c-1f74-44c4-9bad-46c6ce29f797"
import satx
import numpy as np

n = 3

satx.engine(5, cnf_path='tmp.cnf')

c = satx.integer()

xs = satx.matrix(dimensions=(n, n))

satx.apply_single(satx.flatten(xs), lambda x: x > 0)
satx.all_different(satx.flatten(xs))

for i in range(n):
    assert sum(xs[i][j] for j in range(n)) == c
for j in range(n):
    assert sum(xs[i][j] for i in range(n)) == c

assert sum(xs[i][i] for i in range(n)) == c
assert sum(xs[i][n - 1 - i] for i in range(n)) == c

if satx.satisfy('slime'):
    print(c)
    print(np.vectorize(int)(xs))
else:
    print('Infeasible ...')

# + [markdown] id="lEaH-Epz965K"
# # SCHUR TRIPLES PROBLEM:
#
# Input: list of 3N distinct positive integers
#
# Question: Is there a partition of the list into N triples $(a_i, b_i, c_i)$ such that $a_i+b_i=c_i$
#
# The condition that all numbers must be distinct makes the problem very interesting and McDiarmid calls it a surprisingly troublesome.
#
# https://cstheory.stackexchange.com/questions/16253/list-of-strongly-np-hard-problems-with-numerical-data

# + colab={"base_uri": "https://localhost:8080/"} id="Jd9xBJiE965K" outputId="0d42ee84-3c69-4d06-f8d4-fcecbea9e3fd"
import satx
import numpy as np

bits = 7
size = 3 * 10
triplets = []
while len(triplets) < size:
    a = np.random.randint(1, 2 ** bits)
    b = np.random.randint(1, 2 ** bits)
    if a != b and a not in triplets and b not in triplets and a + b not in triplets:
        triplets += [a, b, a + b]
triplets.sort()
print(triplets)
satx.engine(bits=max(triplets).bit_length(), cnf_path='tmp.cnf')
xs, ys = satx.permutations(triplets, size)
for i in range(0, size, 3):
    assert ys[i] + ys[i + 1] == ys[i + 2]
if satx.satisfy('slime'):
    for i in range(0, size, 3):
        print('{} == {} + {}'.format(ys[i + 2], ys[i], ys[i + 1]))
else:
    print('Infeasible ...')

# + [markdown] id="ehRx6Mud965M"
# # SUBSET SUM PROBLEM
#
# In this problem, there is a given set with some integer elements. And another some value is also provided, we have to find a subset of the given set whose sum is the same as the given sum value.
#
# https://en.wikipedia.org/wiki/Subset_sum_problem

# + colab={"base_uri": "https://localhost:8080/"} id="l1u8ka7t965M" outputId="8f6d0492-cbfa-46c7-8161-b94b559f9caf"
import satx
import numpy as np

universe = np.random.randint(1, 1000, size=32)
t = np.random.randint(min(universe), sum(universe))

print(t, universe)

satx.engine(t.bit_length(), cnf_path='tmp.cnf')

bits, subset = satx.subsets(universe)

assert sum(subset) == t

if satx.satisfy('slime'):
    solution = [universe[i] for i in range(len(universe)) if bits.binary[i]]
    print(sum(solution), solution)
else:
    print('Infeasible ...')

# + [markdown] id="daXn5SYi965Q"
# # PERMUTATION RECONSTRUCTION FROM DIFFERENCES
#
# https://arxiv.org/pdf/1410.6396.pdf

# + colab={"base_uri": "https://localhost:8080/", "height": 280} id="YMKxvACO965Q" outputId="f3675001-a4d0-4add-f12f-316e14736041"
import satx
import numpy as np
import matplotlib.pyplot as plt

def gen_instance(n):
    import random
    y = list(range(1, n + 1))
    random.shuffle(y)
    return [abs(y[i + 1] - y[i]) for i in range(n - 1)]


import time
start = time.time()
times = []
sizes = []
for n in range(1, 30):
    diffs = gen_instance(n)
    ini = time.time()
    satx.engine(n.bit_length() + 1, cnf_path='tmp.cnf')
    x = satx.vector(size=n)
    satx.all_different(x)
    satx.apply_single(x, lambda a: 1 <= a <= n)
    for i in range(n - 1):
        assert satx.index(i, diffs) == satx.one_of([x[i + 1] - x[i], x[i] - x[i + 1]])
    if satx.satisfy('slime'):
        end = time.time() - ini
        xx = [abs(x[i + 1] - x[i]) for i in range(n - 1)]
        if xx == diffs:
            sizes.append(n)
            times.append(end)
        else:
            raise Exception('Error!')
    else:
        raise Exception('Error!')
end = time.time() - start
plt.title('TIME {}(s)'.format(end))
plt.plot(sizes, times, 'k-')
plt.plot(sizes, times, 'r.')
plt.show()
plt.close()

# + [markdown] id="bJwHMwDc965S"
# # HAMILTONIAN CYCLE PROBLEM
#
# In the mathematical field of graph theory, a Hamiltonian path (or traceable path) is a path in an undirected or directed graph that visits each vertex exactly once. A Hamiltonian cycle (or Hamiltonian circuit) is a Hamiltonian path that is a cycle. Determining whether such paths and cycles exist in graphs is the Hamiltonian path problem, which is NP-complete.
#
# https://en.wikipedia.org/wiki/Hamiltonian_path

# + colab={"base_uri": "https://localhost:8080/"} id="UbxWGgHu965S" outputId="c4a43604-2d9d-4565-aecc-a633ab519d85"
import sys

import satx
import numpy as np


n = 10
M = np.random.randint(0, 2, size=(n, n))

print(M)

satx.engine((n ** 2).bit_length(), cnf_path='tmp.cnf')
ids, elements = satx.matrix_permutation((1 - M).flatten(), n)

assert sum(elements) == 0

if satx.satisfy('slime'):
    for i in ids:
        for j in ids:
            sys.stdout.write('{} '.format(M[i.value][j.value]))
        sys.stdout.write('\n') 
    sys.stdout.write('\n')
else:
    print('Infeasible ...')

# + [markdown] id="4a2Y3ykM965U"
# # BIN PACKING PROBLEM
#
# In the bin packing problem, items of different volumes must be packed into a finite number of bins or containers each of a fixed given volume in a way that minimizes the number of bins used. In computational complexity theory, it is a combinatorial NP-hard problem. The decision problem (deciding if items will fit into a specified number of bins) is NP-complete.
#
# https://en.wikipedia.org/wiki/Bin_packing_problem

# + colab={"base_uri": "https://localhost:8080/"} id="udwwcxlG965U" outputId="8e7251d2-eff8-4395-e9c6-a1c9b374ff6c"
import satx
import numpy as np

capacity = 50
size = 50
elements = sorted([np.random.randint(1, capacity // 2 - 1) for _ in range(size)], reverse=True)
print(capacity)
print(elements)
bins = int(np.ceil(sum(elements) / capacity))
while True:
    satx.engine(bits=capacity.bit_length() + 1, cnf_path='tmp.cnf')
    slots = satx.vector(bits=len(elements), size=bins)
    for i in range(len(elements)):
        assert sum(satx.switch(slot, i) for slot in slots) == 1
    for slot in slots:
        assert sum(satx.switch(slot, i) * elements[i] for i in range(len(elements))) <= capacity
    if satx.satisfy('slime'):
        print('Solution for {} bins...'.format(bins))
        for slot in slots:
            print(''.join(['_' if boolean else '#' for boolean in slot.binary]))
        for slot in slots:
            sub = [item for i, item in enumerate(elements) if not slot.binary[i]]
            print(sum(sub), sub)
        break
    else:
        print('No solution for {} bins...'.format(bins))
        bins += 1

# + [markdown] id="oI6JNjwq965W"
# # ZERO-ONE INTEGER PROGRAMMING DEFINITION
#
# Zero-one integer programming (which can also be written as 0-1 integer programming) is a mathematical method of using a series of binary, yes (1) and no (0) answers to arrive at a solution when there are two mutually exclusive options.
#
# https://en.wikipedia.org/wiki/Integer_programming

# + colab={"base_uri": "https://localhost:8080/"} id="UBSuy8E1965W" outputId="b7b186bc-922d-4ebd-f295-e250e3b74fed"
import satx
import numpy as np

n, m = 10, 5
cc = np.random.randint(0, 1000, size=(n, m))
d = np.dot(cc, np.random.randint(0, 2, size=(m,)))
print(cc)
print(d)
satx.engine(bits=int(np.sum(cc)).bit_length(), cnf_path='tmp.cnf')
xs = satx.vector(size=m)
satx.all_binaries(xs)
assert (np.dot(cc, xs) == d).all()
if satx.satisfy('slime'):
    print(xs)
    print('Proof:')
    print(np.dot(cc, xs))
else:
    print('Infeasible...')

# + [markdown] id="Q2UGOuKW965Y"
# # n-QUEENS COMPLETION PROBLEM
#
# The n- Queens Completion problem is a variant, dating to 1850, in which some queens are already placed and the solver is asked to place the rest, if possi- ble. ... The n-Queens problem is to place n chess queens on an n by n chessboard so that no two queens are on the same row, column or diagonal.
#
# https://www.ijcai.org/Proceedings/2018/0794.pdf

# + colab={"base_uri": "https://localhost:8080/"} id="rECfC3zy965Y" outputId="b0dd0557-cb34-448c-8adc-b93014c652f6"
import satx


def completion(n, m, seed):
    import random
    """
    http://www.csplib.org/Problems/prob079/data/queens-gen-fast.py.html
    """
    random.seed(seed)

    d1 = [0 for _ in range(2 * n - 1)]
    d2 = [0 for _ in range(2 * n - 1)]

    valid_rows = [i for i in range(n)]
    valid_cols = [j for j in range(n)]

    def no_attack(r, c):
        return d1[r + c] == 0 and d2[r - c + n - 1] == 0

    pc = []
    queens_left = n

    for attempt in range(n * n):
        i = random.randrange(queens_left)
        j = random.randrange(queens_left)
        r = valid_rows[i]
        c = valid_cols[j]
        if no_attack(r, c):
            pc.append([r, c])
            d1[r + c] = 1
            d2[r - c + n - 1] = 1
            valid_rows[i] = valid_rows[queens_left - 1]
            valid_cols[j] = valid_cols[queens_left - 1]
            queens_left -= 1
            if len(pc) == m:
                return [[x + 1, y + 1] for x, y in pc]

def show(pc):
    table = ''
    for i in range(1, n + 1):
        table += ''
        for j in range(1, n + 1):
            if [i, j] not in pc:
                table += '. '
            else:
                table += 'Q '
        table += '\n'
    print(table)
    print('# seed = {}'.format(seed))
    
n, m, seed = 30, 15, 0
placed_queens = completion(n, m, seed)
show(placed_queens)
satx.engine(bits=n.bit_length() + 1, cnf_path='tmp.cnf')
qs = satx.vector(size=n)
for (a, b) in placed_queens:
    assert qs[a - 1] == b - 1
satx.apply_single(qs, lambda x: x < n)
satx.apply_dual(qs, lambda x, y: x != y)
satx.apply_dual([qs[i] + i for i in range(n)], lambda x, y: x != y)
satx.apply_dual([qs[i] - i for i in range(n)], lambda x, y: x != y)
if satx.satisfy('slime'):
    for i in range(n):
        print(''.join(['Q ' if qs[i] == j else '. ' for j in range(n)]))
    print('')
else:
    print('Infeasible ...')

# + [markdown] id="QJiSiXi_DyFL"
# # PARTITION PROBLEM
#
# n number theory and computer science, the partition problem, or number partitioning, is the task of deciding whether a given multiset $S$ of positive integers can be partitioned into two subsets $S_1$ and $S_2$ such that the sum of the numbers in $S_1$ equals the sum of the numbers in $S_2$.
#
# https://en.wikipedia.org/wiki/Partition_problem

# + colab={"base_uri": "https://localhost:8080/"} id="yZlJB_TdDwyc" outputId="8784d3d9-6301-4ff3-9b05-9bcaa2a65a14"
import numpy as np
import satx

size = 20

data = np.random.randint(1000, size=size)

print(data)

satx.engine(int(sum(data)).bit_length(), cnf_path='tmp.cnf')

T, sub, com = satx.subsets(data, complement=True)

assert sum(sub) == sum(com)

if satx.satisfy('slime'):
    sub_ = [data[i] for i in range(size) if T.binary[i]]
    com_ = [data[i] for i in range(size) if not T.binary[i]]
    print(sum(sub_), sub_)
    print(sum(com_), com_)
else:
    print('Infeasible ...')

# + [markdown] id="zaw48EMAikEp"
# # SUDOKU 
#
# is a logic-based, combinatorial number-placement puzzle. The objective is to fill a 9×9 grid with digits so that each column, each row, and each of the nine 3×3 subgrids that compose the grid (also called "boxes", "blocks", or "regions") contain all of the digits from 1 to 9. The puzzle setter provides a partially completed grid, which for a well-posed puzzle has a single solution.
#
# Completed games are always an example of a Latin square which include an additional constraint on the contents of individual regions. For example, the same single integer may not appear twice in the same row, column, or any of the nine 3×3 subregions of the 9×9 playing board.
#
# https://en.wikipedia.org/wiki/Sudoku

# + colab={"base_uri": "https://localhost:8080/"} id="Xv2NJptiijYi" outputId="35309dc1-72de-4aef-f28b-91b2e5a017aa"
import numpy as np
import satx


def expand_line(line):
    return line[0] + line[5:9].join([line[1:5] * (base - 1)] * base) + line[9:13]


def show(board):
    import string
    line0 = expand_line('╔═══╤═══╦═══╗')
    line1 = expand_line('║ . │ . ║ . ║')
    line2 = expand_line('╟───┼───╫───╢')
    line3 = expand_line('╠═══╪═══╬═══╣')
    line4 = expand_line('╚═══╧═══╩═══╝')

    symbol = ' ' + string.printable.replace(' ', '')
    nums = [[''] + [symbol[n] for n in row] for row in board]
    print(line0)
    for r in range(1, side + 1):
        print("".join(n + s for n, s in zip(nums[r - 1], line1.split('.'))))
        print([line2, line3, line4][(r % side == 0) + (r % base == 0)])


def generate(base):
    # pattern for a baseline valid solution
    def pattern(r, c):
        return (base * (r % base) + r // base + c) % side

    # randomize rows, columns and numbers (of valid base pattern)
    from random import sample

    def shuffle(s):
        return sample(s, len(s))

    rBase = range(base)
    rows = [g * base + r for g in shuffle(rBase) for r in shuffle(rBase)]
    cols = [g * base + c for g in shuffle(rBase) for c in shuffle(rBase)]
    nums = shuffle(range(1, base * base + 1))

    # produce board using randomized baseline pattern
    board = [[nums[pattern(r, c)] for c in cols] for r in rows]

    squares = side * side
    empties = (squares * 3) // 4
    for p in map(int, sample(range(squares), empties)):
        board[p // side][p % side] = 0

    show(board)
    return board


base = 4
side = base * base

puzzle = np.asarray(generate(base))

satx.engine(side.bit_length(), cnf_path='tmp.cnf')

board = np.asarray(satx.matrix(dimensions=(side, side)))
satx.apply_single(board.flatten(), lambda x: 1 <= x <= side)

for i in range(side):
    for j in range(side):
        if puzzle[i][j]:
            assert board[i][j] == puzzle[i][j]

for c, r in zip(board, board.T):
    satx.all_different(c)
    satx.all_different(r)

for i in range(base):
    for j in range(base):
        satx.all_different(board[i * base:(i + 1) * base, j * base:(j + 1) * base].flatten())

if satx.satisfy('slime'):
    show(np.vectorize(int)(board))


# + [markdown] id="rpW3jjf8edtW"
# # MAXIMUM CONSTRAINED PARTITITON
#
# ---
#
#
#
# ---
#
#
#
# http://www.csc.kth.se/~viggo/wwwcompendium/node152.html

# + colab={"base_uri": "https://localhost:8080/"} id="qyLQYD-je1Jq" outputId="115ed459-c444-44e3-f61e-06c7ed59c64c"
import random

import satx

bits = 10
n = 2 * 100

D = [random.randint(1, 2 ** bits) for _ in range(n)]

print('D   : {}'.format(D))

satx.engine(sum(D).bit_length(), cnf_path='tmp.cnf')

bins, sub, com = satx.subsets(D, n // 2, complement=True)

assert sum(sub) == sum(com)

if satx.satisfy('slime'):
    sub = [D[i] for i in range(n) if bins.binary[i]]
    com = [D[i] for i in range(n) if not bins.binary[i]]
    print(sum(sub), len(sub), sub)
    print(sum(com), len(com), com)
    print('\n')
else:
    print('Infeasible ...')

# + [markdown] id="1qFj_5FpCOBt"
# # PARALLEL OPTIMIZATION - MIN-MAX SUM SUBSET CARDINALITY

# + [markdown] id="6YJtctLJwDqo"
# # GRIEWANK FUNCTION
#
# Ref: https://www.sfu.ca/~ssurjano/griewank.html

# + colab={"base_uri": "https://localhost:8080/"} id="cmVv0aqxTm1M" outputId="13ca6f29-d383-4234-cf15-bc953b2c0a0a"
import numpy
import satx


class GriewankFunctionHESS:

    def __init__(self, a, b):
        self.a = a
        self.b = b

    def oracle(self, xs):
        return numpy.sum([(x ** 2) / 4000 for x in xs]) - numpy.prod([numpy.cos(x / numpy.sqrt(i + 1)) for i, x in enumerate(xs)]) + 1

    def f(self, i, j, xs):
        xs[i], xs[j] = self.a + xs[i] / self.b, self.a + xs[j] / self.b
        xs[i:j] = xs[i:j][::-1]

    def g(self, i, j, xs):
        xs[i:j] = xs[i:j][::-1]
        xs[i], xs[j] = self.b * xs[i] - self.a, self.b * xs[j] - self.a

    def log(self, top, opt):
        print(top)

    def run(self, n):
        xs = numpy.random.randint(-600, 600, size=n)
        return satx.hess_abstract(xs, self.oracle, self.f, self.g, self.log, target=0)


n = 100
gf = GriewankFunctionHESS(n ** -2, n ** 2)
print(gf.run(n))

StarcoderdataJupyterScriptsDedupFiltered