locuslab / satnet Goto Github PK

Bridging deep learning and logical reasoning using a differentiable satisfiability solver.

License: MIT License

Dockerfile 1.54% Shell 0.79% Python 52.96% C++ 23.96% Cuda 20.02% C 0.72%

satnet's Introduction

SATNet •

Bridging deep learning and logical reasoning using a differentiable satisfiability solver.

This repository contains the source code to reproduce the experiments in the ICML 2019 paper SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver by Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter.

What is SATNet

SATNet is a differentiable (smoothed) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems. This (approximate) solver is based upon a fast coordinate descent approach to solving the semidefinite program (SDP) associated with the MAXSAT problem.

How SATNet works

A SATNet layer takes as input the discrete or probabilistic assignments of known MAXSAT variables, and outputs guesses for the assignments of unknown variables via a MAXSAT SDP relaxation with weights S. A schematic depicting the forward pass of this layer is shown below. To obtain the backward pass, we analytically differentiate through the SDP relaxation (see the paper for more details).

Overview of experiments

We show that by integrating SATNet into end-to-end learning systems, we can learn the logical structure of challenging problems in a minimally supervised fashion. In particular, we show that we can:

Learn the parity function using single-bit supervision (a traditionally hard task for deep networks)
Learn how to play 9×9 Sudoku (original and permuted) solely from examples.
Solve a "visual Sudoku" problem that maps images of Sudoku puzzles to their associated logical solutions. (A sample "visual Sudoku" input is shown below.)

Installation

Via pip

pip install satnet

From source

git clone https://github.com/locuslab/SATNet
cd SATNet && python setup.py install

Package Dependencies

conda install -c pytorch tqdm

The package also depends on the nvcc compiler. If it doesn't exist (try nvcc from commandline), you can install it via

conda install -c conda-forge cudatoolkit-dev

Via Docker image

cd docker
sh ./build.sh
sh ./run.sh

Running experiments

Jupyter Notebook and Google Colab

Jupyter notebook and Google Colab

Run them manually

Getting the datasets

The Sudoku dataset and Parity dataset can be downloaded via

wget -cq powei.tw/sudoku.zip && unzip -qq sudoku.zip
wget -cq powei.tw/parity.zip && unzip -qq parity.zip

Sudoku experiments (original, permuted, and visual)

python exps/sudoku.py
python exps/sudoku.py --perm
python exps/sudoku.py --mnist --batchSz=50

Parity experiments

python exps/parity.py --seq=20
python exps/parity.py --seq=40

satnet's People

Contributors

Stargazers

Watchers

satnet's Issues

Getting RuntimeError: CUDA error: invalid argument

Hi,
I was trying to run the SATNet model on a custom project and I'm seeing the following error:

Traceback (most recent call last):
  File "kakuro_solver_satnet.py", line 175, in <module>
    train(
  File "kakuro_solver_satnet.py", line 113, in train
    run(epoch, model, optimizer, dataset, batchSz, device, to_train=True)
  File "kakuro_solver_satnet.py", line 95, in run
    preds = model(b_data.contiguous(), b_is_input.contiguous())
  File "/home/pramod/MS/SEM-1/NSR/NeuroSymbolicReasoning/nsr/lib/python3.8/site-packages/torch/nn/modules/module.py", line 727, in _call_impl
    result = self.forward(*input, **kwargs)
  File "kakuro_solver_satnet.py", line 32, in forward
    out = self.sat(batch, mask)
  File "/home/pramod/MS/SEM-1/NSR/NeuroSymbolicReasoning/nsr/lib/python3.8/site-packages/torch/nn/modules/module.py", line 727, in _call_impl
    result = self.forward(*input, **kwargs)
  File "/home/pramod/MS/SEM-1/NSR/SATNet/satnet/models.py", line 154, in forward
    z = MixingFunc.apply(self.S, z, is_input, self.max_iter, self.eps, self.prox_lam)
  File "/home/pramod/MS/SEM-1/NSR/SATNet/satnet/models.py", line 51, in forward
    satnet_impl.forward(max_iter, eps,
RuntimeError: CUDA error: invalid argument

However, when I try to run the same piece of code using CPU, it works perfectly fine.

My coding environment:

>>> torch.__version__: '1.7.1+cu101'
$ nvcc --version
nvcc: NVIDIA (R) Cuda compiler driver
Copyright (c) 2005-2019 NVIDIA Corporation
Built on Sun_Jul_28_19:07:16_PDT_2019
Cuda compilation tools, release 10.1, V10.1.243

I'm using a GeForce GTX 1650 GPU.

The code I'm using is:

class KakuroSolver(nn.Module):

    def __init__(self, n, m, aux):
        super(KakuroSolver, self).__init__()
        self.sat = satnet.SATNet(n, m, aux)

    def forward(self, batch, mask):
        out = self.sat(batch, mask)
        return out


def get_device(use_gpu=True):
    if torch.cuda.is_available() and use_gpu:
        print(f'GPU available: {torch.cuda.get_device_name()}')
        device = torch.device('cuda')
    else:
        print('No GPU available or forbidden from usage. Using CPU')
        device = torch.device('cpu')
    return device

def run(epoch, model, optimizer, dataset, batchSz, device, to_train):

    loss_final = 0

    loader = torch.utils.data.DataLoader(dataset, batch_size=batchSz, drop_last=True)

    for idx, (data, is_input, label) in enumerate(loader):
        # transfer the data to the designated device.
        b_data = data.to(device)
        b_is_input = is_input.to(device)
        b_label = label.to(device)

        if to_train: optimizer.zero_grad()
        print(b_data.shape, b_is_input.shape)
        preds = model(b_data.contiguous(), b_is_input.contiguous())
        if idx == len(loader) - 1 and epoch == NO_OF_EPOCHS:
            print(preds)
        loss = nn.functional.binary_cross_entropy(preds, b_label)

        if to_train:
            loss.backward()
            optimizer.step()

        loss_final += loss.item()

    loss_final = loss_final/len(loader)
    print('RESULTS: Average loss: {:.4f}'.format(loss_final))

    torch.cuda.empty_cache()


def train(epoch, model, optimizer, dataset, batchSz, device):
    run(epoch, model, optimizer, dataset, batchSz, device, to_train=True)


@torch.no_grad()
def test(epoch, model, optimizer, dataset, batchSz, device):
    run(epoch, model, optimizer, dataset, batchSz, device, to_train=False)


# The code here simulates the generation of vectors I'll finally have
X = torch.randint(2, (195, 2288)).type(torch.int32)
is_input = torch.randint(2, (195, 2288)).type(torch.int32)
y = torch.randint(2, (195, 2288)).type(torch.float64)

X_train, X_test, y_train, y_test, is_input_train, is_input_test =\
    train_test_split(X, y, is_input, test_size=0.2)
train_dataset = torch.utils.data.TensorDataset(X_train, is_input_train, y_train)

solver = KakuroSolver(2288, X.shape[1], 30)

# get ready to train
# fetch the device which will be used to train
use_gpu = False if len(sys.argv) > 1 and sys.argv[1] == '0' else True
device = get_device(use_gpu)

# move the model to the `device`
solver.to(device)

print('Starting the training process...')
optimizer = torch.optim.Adam(solver.parameters(), lr=LEARNING_RATE)
for epoch in range(1, NO_OF_EPOCHS + 1):
    train(
        epoch=epoch,
        model=solver,
        optimizer=optimizer,
        dataset=train_dataset,
        batchSz=BATCH_SIZE,
        device=device
    )

Could you please help me find a solution to this issue?

Training on CPU: "invalid on input"

Hi, I'm trying to run the parity experiment locally on my CPU:

python exps/parity.py --seq=20

But at Epoch 18 I get the error invalid on input:

Epoch 0 Test  Loss 1.3451 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.53it/s]
TESTING SET RESULTS: Average loss: 1.3595 Err: 0.5100
Epoch 1 Train Loss 0.6839 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:05<00:00, 17.56it/s]
Epoch 1 Test  Loss 0.7007 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  5.67it/s]
TESTING SET RESULTS: Average loss: 0.7005 Err: 0.5100
Epoch 2 Train Loss 0.6832 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:04<00:00, 18.22it/s]
Epoch 2 Test  Loss 0.7004 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  5.39it/s]
TESTING SET RESULTS: Average loss: 0.6999 Err: 0.5100
Epoch 3 Train Loss 0.6813 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:05<00:00, 17.29it/s]
Epoch 3 Test  Loss 0.7003 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.58it/s]
TESTING SET RESULTS: Average loss: 0.6994 Err: 0.5100
Epoch 4 Train Loss 0.6814 Err: 0.3900: 100%|██████████████████████████████| 90/90 [00:06<00:00, 14.00it/s]
Epoch 4 Test  Loss 0.7008 Err: 0.5120: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.53it/s]
TESTING SET RESULTS: Average loss: 0.7012 Err: 0.5140
Epoch 5 Train Loss 0.6823 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:06<00:00, 14.10it/s]
Epoch 5 Test  Loss 0.6999 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.49it/s]
TESTING SET RESULTS: Average loss: 0.6996 Err: 0.5100
Epoch 6 Train Loss 0.6763 Err: 0.3800: 100%|██████████████████████████████| 90/90 [00:06<00:00, 14.06it/s]
Epoch 6 Test  Loss 0.7024 Err: 0.5120: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.52it/s]
TESTING SET RESULTS: Average loss: 0.7028 Err: 0.5130
Epoch 7 Train Loss 0.6836 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:06<00:00, 13.74it/s]
Epoch 7 Test  Loss 0.6986 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.26it/s]
TESTING SET RESULTS: Average loss: 0.6986 Err: 0.5100
Epoch 8 Train Loss 0.6854 Err: 0.4100: 100%|██████████████████████████████| 90/90 [00:06<00:00, 13.82it/s]
Epoch 8 Test  Loss 0.6983 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.53it/s]
TESTING SET RESULTS: Average loss: 0.6979 Err: 0.5100
Epoch 9 Train Loss 0.6882 Err: 0.4500: 100%|██████████████████████████████| 90/90 [00:06<00:00, 13.97it/s]
Epoch 9 Test  Loss 0.6986 Err: 0.5060: 100%|████████████████████████████████| 2/2 [00:00<00:00,  4.12it/s]
TESTING SET RESULTS: Average loss: 0.6974 Err: 0.5100
Epoch 10 Train Loss 0.6878 Err: 0.4100: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.93it/s]
Epoch 10 Test  Loss 0.6985 Err: 0.5060: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.57it/s]
TESTING SET RESULTS: Average loss: 0.6970 Err: 0.5100
Epoch 11 Train Loss 0.6875 Err: 0.4100: 100%|█████████████████████████████| 90/90 [00:06<00:00, 14.09it/s]
Epoch 11 Test  Loss 0.6981 Err: 0.5060: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.25it/s]
TESTING SET RESULTS: Average loss: 0.6974 Err: 0.5100
Epoch 12 Train Loss 0.6830 Err: 0.3900: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.90it/s]
Epoch 12 Test  Loss 0.6983 Err: 0.5120: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.35it/s]
TESTING SET RESULTS: Average loss: 0.6988 Err: 0.5130
Epoch 13 Train Loss 0.6857 Err: 0.4100: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.26it/s]
Epoch 13 Test  Loss 0.6980 Err: 0.5060: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.44it/s]
TESTING SET RESULTS: Average loss: 0.6977 Err: 0.5100
Epoch 14 Train Loss 0.6796 Err: 0.4500: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.64it/s]
Epoch 14 Test  Loss 0.6982 Err: 0.4860: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.52it/s]
TESTING SET RESULTS: Average loss: 0.6989 Err: 0.5030
Epoch 15 Train Loss 0.6886 Err: 0.4800: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.89it/s]
Epoch 15 Test  Loss 0.6974 Err: 0.5060: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.44it/s]
TESTING SET RESULTS: Average loss: 0.6960 Err: 0.5100
Epoch 16 Train Loss 0.6856 Err: 0.4500: 100%|█████████████████████████████| 90/90 [00:06<00:00, 13.99it/s]
Epoch 16 Test  Loss 0.6979 Err: 0.5080: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.22it/s]
TESTING SET RESULTS: Average loss: 0.6997 Err: 0.5080
Epoch 17 Train Loss 0.6784 Err: 0.3800: 100%|█████████████████████████████| 90/90 [00:06<00:00, 14.12it/s]
Epoch 17 Test  Loss 0.7000 Err: 0.5120: 100%|███████████████████████████████| 2/2 [00:00<00:00,  4.32it/s]
TESTING SET RESULTS: Average loss: 0.7011 Err: 0.5130
Epoch 18 Train Loss 0.0310 Err: 0.0000:  49%|██████████████▏              | 44/90 [00:03<00:04, 11.23it/s]invalid on input
invalid on input
invalid on input
invalid on input
invalid on input
invalid on input
Epoch 18 Train Loss 0.0234 Err: 0.0000:  51%|██████████████▊              | 46/90 [00:03<00:03, 11.16it/s]invalid on input
invalid on input
invalid on input
[...]

What could be wrong?

Doubt about the paper first equation

Hello folks at CMU Locus Lab! :)
You have some great repositories, currently I use your TCN net and this one seems quite intriguing too. Reading your paper I stumbled upon the first equation
maximize ∑_j V_i 1{s_ij * v_i > 0} and I couldn't quite figure it out: lets say a certain clause is verified one variable and falsified for all the others, the clause should be falsified, but in your equation it's not.

Why not use instead maximize ∑_j ∧_i 1{s_ij * v_i >= 0} ?
(Using logical conjunction instead of disjunction; equality needed for the s_ij=0 cases)

Keep up the great work,
Enrico Bonetti Vieno

P.S.: the notation 1{...} is a step function over a boolean value: 1 if true, 0 otherwise - right?

How to get rules generated for Sudoku Solver?

I was trying to replicate the results in the experiment and was having a hard time finding the rules generated. Is there any method to get the rules generated? It would be really helpful for my research project

Sorry for raising an issue in Github, I didn't know any other way to get in touch with you

Thanks for this awesome project btw, I really love what yall have done

Failed on running Suodku example with CUDA

Thanks for this project and it is awesome! I installed satnet through pip. But when I run the visual-sudoku examples, this error occurs:

Install error in both Colab and Ubuntu22.04

Hi! I try to install your library, but I encounter the error:

In Ubuntu 22.04: satnet_cuda.cu(165): error: identifier "saturate" is undefined. I am using Python3.11, and Pytorch 2.2.2, CUDA 12.2.

In the colab: ModuleNotFoundError: No module named 'satnet._cpp'

Here is the details about the log:

In Ubuntu:

running develop
/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/command/develop.py:40: EasyInstallDeprecationWarning: easy_install command is deprecated.
!!

        ********************************************************************************
        Please avoid running ``setup.py`` and ``easy_install``.
        Instead, use pypa/build, pypa/installer or other
        standards-based tools.

        See https://github.com/pypa/setuptools/issues/917 for details.
        ********************************************************************************

!!
  easy_install.initialize_options(self)
/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/cmd.py:66: SetuptoolsDeprecationWarning: setup.py install is deprecated.
!!

        ********************************************************************************
        Please avoid running ``setup.py`` directly.
        Instead, use pypa/build, pypa/installer or other
        standards-based tools.

        See https://blog.ganssle.io/articles/2021/10/setup-py-deprecated.html for details.
        ********************************************************************************

!!
  self.initialize_options()
running egg_info
creating satnet.egg-info
writing satnet.egg-info/PKG-INFO
writing dependency_links to satnet.egg-info/dependency_links.txt
writing requirements to satnet.egg-info/requires.txt
writing top-level names to satnet.egg-info/top_level.txt
writing manifest file 'satnet.egg-info/SOURCES.txt'
reading manifest file 'satnet.egg-info/SOURCES.txt'
adding license file 'LICENSE'
writing manifest file 'satnet.egg-info/SOURCES.txt'
running build_ext
/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py:415: UserWarning: The detected CUDA version (12.2) has a minor version mismatch with the version that was used to compile PyTorch (12.1). Most likely this shouldn't be a problem.
  warnings.warn(CUDA_MISMATCH_WARN.format(cuda_str_version, torch.version.cuda))
/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py:425: UserWarning: There are no g++ version bounds defined for CUDA version 12.2
  warnings.warn(f'There are no {compiler_name} version bounds defined for CUDA version {cuda_str_version}')
building 'satnet._cpp' extension
creating /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build
creating /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311
creating /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src
Emitting ninja build file /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/build.ninja...
Compiling objects...
Allowing ninja to set a default number of workers... (overridable by setting the environment variable MAX_JOBS=N)
[1/2] c++ -MMD -MF /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cpu.o.d -pthread -B /data/Hypothesis/domain/ns/compiler_compat -DNDEBUG -fwrapv -O2 -Wall -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -I./src -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/torch/csrc/api/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/TH -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/THC -I/data/Hypothesis/domain/ns/include/python3.11 -c -c /data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet_cpu.cpp -o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cpu.o -fopenmp -msse4.1 -Wall -g -DTORCH_API_INCLUDE_EXTENSION_H '-DPYBIND11_COMPILER_TYPE="_gcc"' '-DPYBIND11_STDLIB="_libstdcpp"' '-DPYBIND11_BUILD_ABI="_cxxabi1011"' -DTORCH_EXTENSION_NAME=_cpp -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++17
[2/2] c++ -MMD -MF /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet.o.d -pthread -B /data/Hypothesis/domain/ns/compiler_compat -DNDEBUG -fwrapv -O2 -Wall -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -I./src -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/torch/csrc/api/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/TH -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/THC -I/data/Hypothesis/domain/ns/include/python3.11 -c -c /data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet.cpp -o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet.o -fopenmp -msse4.1 -Wall -g -DTORCH_API_INCLUDE_EXTENSION_H '-DPYBIND11_COMPILER_TYPE="_gcc"' '-DPYBIND11_STDLIB="_libstdcpp"' '-DPYBIND11_BUILD_ABI="_cxxabi1011"' -DTORCH_EXTENSION_NAME=_cpp -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++17
creating build/lib.linux-x86_64-cpython-311
creating build/lib.linux-x86_64-cpython-311/satnet
g++ -pthread -B /data/Hypothesis/domain/ns/compiler_compat -shared -Wl,-rpath,/data/Hypothesis/domain/ns/lib -Wl,-rpath-link,/data/Hypothesis/domain/ns/lib -L/data/Hypothesis/domain/ns/lib -Wl,-rpath,/data/Hypothesis/domain/ns/lib -Wl,-rpath-link,/data/Hypothesis/domain/ns/lib -L/data/Hypothesis/domain/ns/lib /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet.o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cpu.o -L/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/lib -lc10 -ltorch -ltorch_cpu -ltorch_python -o build/lib.linux-x86_64-cpython-311/satnet/_cpp.cpython-311-x86_64-linux-gnu.so
building 'satnet._cuda' extension
Emitting ninja build file /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/build.ninja...
Compiling objects...
Allowing ninja to set a default number of workers... (overridable by setting the environment variable MAX_JOBS=N)
[1/2] /usr/local/cuda-12.2/bin/nvcc --generate-dependencies-with-compile --dependency-output /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cuda.o.d -I./src -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/torch/csrc/api/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/TH -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/THC -I/usr/local/cuda-12.2/include -I/data/Hypothesis/domain/ns/include/python3.11 -c -c /data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet_cuda.cu -o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cuda.o -D__CUDA_NO_HALF_OPERATORS__ -D__CUDA_NO_HALF_CONVERSIONS__ -D__CUDA_NO_BFLOAT16_CONVERSIONS__ -D__CUDA_NO_HALF2_OPERATORS__ --expt-relaxed-constexpr --compiler-options ''"'"'-fPIC'"'"'' -g -restrict -maxrregcount 32 -lineinfo -Xptxas=-v -DTORCH_API_INCLUDE_EXTENSION_H '-DPYBIND11_COMPILER_TYPE="_gcc"' '-DPYBIND11_STDLIB="_libstdcpp"' '-DPYBIND11_BUILD_ABI="_cxxabi1011"' -DTORCH_EXTENSION_NAME=_cuda -D_GLIBCXX_USE_CXX11_ABI=0 -gencode=arch=compute_89,code=compute_89 -gencode=arch=compute_89,code=sm_89 -std=c++17
FAILED: /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cuda.o 
/usr/local/cuda-12.2/bin/nvcc --generate-dependencies-with-compile --dependency-output /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cuda.o.d -I./src -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/torch/csrc/api/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/TH -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/THC -I/usr/local/cuda-12.2/include -I/data/Hypothesis/domain/ns/include/python3.11 -c -c /data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet_cuda.cu -o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet_cuda.o -D__CUDA_NO_HALF_OPERATORS__ -D__CUDA_NO_HALF_CONVERSIONS__ -D__CUDA_NO_BFLOAT16_CONVERSIONS__ -D__CUDA_NO_HALF2_OPERATORS__ --expt-relaxed-constexpr --compiler-options ''"'"'-fPIC'"'"'' -g -restrict -maxrregcount 32 -lineinfo -Xptxas=-v -DTORCH_API_INCLUDE_EXTENSION_H '-DPYBIND11_COMPILER_TYPE="_gcc"' '-DPYBIND11_STDLIB="_libstdcpp"' '-DPYBIND11_BUILD_ABI="_cxxabi1011"' -DTORCH_EXTENSION_NAME=_cuda -D_GLIBCXX_USE_CXX11_ABI=0 -gencode=arch=compute_89,code=compute_89 -gencode=arch=compute_89,code=sm_89 -std=c++17
/data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet_cuda.cu(165): error: identifier "saturate" is undefined
          zi = saturate((zi+1)/2)*2-1;
               ^

1 error detected in the compilation of "/data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet_cuda.cu".
[2/2] c++ -MMD -MF /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet.o.d -pthread -B /data/Hypothesis/domain/ns/compiler_compat -DNDEBUG -fwrapv -O2 -Wall -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -O2 -isystem /data/Hypothesis/domain/ns/include -fPIC -I./src -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/torch/csrc/api/include -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/TH -I/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/include/THC -I/usr/local/cuda-12.2/include -I/data/Hypothesis/domain/ns/include/python3.11 -c -c /data/Hypothesis/lemma/NeuralSymbolic/SATNet/src/satnet.cpp -o /data/Hypothesis/lemma/NeuralSymbolic/SATNet/build/temp.linux-x86_64-cpython-311/src/satnet.o -DMIX_USE_GPU -g -DTORCH_API_INCLUDE_EXTENSION_H '-DPYBIND11_COMPILER_TYPE="_gcc"' '-DPYBIND11_STDLIB="_libstdcpp"' '-DPYBIND11_BUILD_ABI="_cxxabi1011"' -DTORCH_EXTENSION_NAME=_cuda -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++17
ninja: build stopped: subcommand failed.
Traceback (most recent call last):
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py", line 2096, in _run_ninja_build
    subprocess.run(
  File "/data/Hypothesis/domain/ns/lib/python3.11/subprocess.py", line 571, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['ninja', '-v']' returned non-zero exit status 1.

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/data/Hypothesis/lemma/NeuralSymbolic/SATNet/setup.py", line 48, in <module>
    setup(
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/__init__.py", line 103, in setup
    return distutils.core.setup(**attrs)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/core.py", line 185, in setup
    return run_commands(dist)
           ^^^^^^^^^^^^^^^^^^
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/core.py", line 201, in run_commands
    dist.run_commands()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/dist.py", line 969, in run_commands
    self.run_command(cmd)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/dist.py", line 989, in run_command
    super().run_command(command)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/dist.py", line 988, in run_command
    cmd_obj.run()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/command/develop.py", line 34, in run
    self.install_for_development()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/command/develop.py", line 109, in install_for_development
    self.run_command('build_ext')
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/cmd.py", line 318, in run_command
    self.distribution.run_command(command)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/dist.py", line 989, in run_command
    super().run_command(command)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/dist.py", line 988, in run_command
    cmd_obj.run()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/command/build_ext.py", line 88, in run
    _build_ext.run(self)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/command/build_ext.py", line 345, in run
    self.build_extensions()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py", line 871, in build_extensions
    build_ext.build_extensions(self)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/command/build_ext.py", line 467, in build_extensions
    self._build_extensions_serial()
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/command/build_ext.py", line 493, in _build_extensions_serial
    self.build_extension(ext)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/command/build_ext.py", line 249, in build_extension
    _build_ext.build_extension(self, ext)
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/setuptools/_distutils/command/build_ext.py", line 548, in build_extension
    objects = self.compiler.compile(
              ^^^^^^^^^^^^^^^^^^^^^^
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py", line 684, in unix_wrap_ninja_compile
    _write_ninja_file_and_compile_objects(
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py", line 1774, in _write_ninja_file_and_compile_objects
    _run_ninja_build(
  File "/data/Hypothesis/domain/ns/lib/python3.11/site-packages/torch/utils/cpp_extension.py", line 2112, in _run_ninja_build
    raise RuntimeError(message) from e
RuntimeError: Error compiling objects for extension

In Colab:

---------------------------------------------------------------------------
ModuleNotFoundError                       Traceback (most recent call last)
[<ipython-input-4-f115df1ae491>](https://localhost:8080/#) in <cell line: 1>()
----> 1 import satnet
      2 print('SATNet document\n', satnet.SATNet.__doc__)

1 frames
[/content/SATNet/satnet/models.py](https://localhost:8080/#) in <module>
      4 import torch.optim as optim
      5 
----> 6 import satnet._cpp
      7 if torch.cuda.is_available(): import satnet._cuda
      8 

ModuleNotFoundError: No module named 'satnet._cpp'

---------------------------------------------------------------------------
NOTE: If your import is failing due to a missing package, you can
manually install dependencies using either !pip or !apt.

To view examples of installing some common dependencies, click the
"Open Examples" button below.
---------------------------------------------------------------------------

different sign on the gradients dS, dz and line6 in algorithm 3

Hi Dr. Po-Wei Wang

many thanks for opensourcing this greate work. When I read through your code. I have noticed there are a few differnce between the code and the paper:

at src/satnet_cpu.cpp in function mix_kernel, for the backward pass, you use g = -(I-v_i v_i') (g+v_0 dz[i]), but I checked that based on the paper's algorithm 3 this should be dg=-P*(g - v_o dz[i]) with a minus sign? please correct me if im wrong.
in the paper, for dl/dS and dl/zi, in both equation 11 and 12, there are minus signs. but in the code it becomes: dS = U W + V Phi and dzi = v0'Phi si. please can you tell me why the signs are reversed?

many thanks for you help!
sichao y

Missing satnet.h file in the pip repo

Hello.

Firstly I tried to install this package from pip. I got error saying no such file called satnet.h

There is a similar issue in the issues and then I double-checked the files from pip repo.

In the src of satnet of pip repo, it does missing the header file but in this scr of github version, there is the header file.

Therefore, could you update the pip repo so nobody

will be confused later

Bests

Question about matrix S

Hi, your work is so brilliant！
However, I doubt about the value of S. It seems that the learnt S is not a ternary matrix right? If S is not ternary, then how can we say that it is the 'rule' learnt by the network?
Thanks!

How is the CNN in your paper only achieved 0.04% accuracy?

I read your paper and I can't believe that a CNN with a sequence of 10 convolutional layers (each with 512 3×3 filters) can only achieve 0.04% accuracy on 9x9 sudoku with on average 36 known cells. Because, by accident, I tried to use the exact same structure to solve 9x9 sudoku with at most 32 given cells with 100% accuracy. I think you didn't train that network well to saturate its performance as the training acc in your paper was about 70%. You can actually train it to 100%.

Someone also did similar things before:
https://github.com/Kyubyong/sudoku
https://www.kaggle.com/bryanpark/sudoku

B.T.W. Sudoku with on average 36 known cells is actually almost trivial to solve. However, with a minimal number of known cells (17), it becomes much harder. I tried your network on 9x9 Sudoku with 17 known cells and it didn't work.
FYI: This paper https://arxiv.org/pdf/1711.08028.pdf (you also mentioned in your paper) achieved like 96% Acc. Thus, I don't think you can say "our test accuracy is qualitatively similar to the results obtained in Palm et al. (2017)" in your paper.

Can't execute code on Google Colab

Hi!
I've been trying to run the code provided on Google Colab but it produces an error when running the code cell under "The 9x9 Sudoku Experiment". The error occurs in PyTorch, and I've tried downgrading to versions < 1.3.1 but there is another dependency that requires one to use version 1.3.1.

Here is the full stack trace:

`---------------------------------------------------------------------------
RuntimeError Traceback (most recent call last)
in ()
10 test_logger = FigLogger(fig, axes[1], 'Testing')
11
---> 12 test(args.boardSz, 0, sudoku_model, optimizer, test_logger, sudoku_test, args.batchSz)
13 plt.pause(0.01)
14 for epoch in range(1, args.nEpoch+1):

6 frames
/usr/local/lib/python3.6/dist-packages/torch/autograd/grad_mode.py in decorate_no_grad(*args, **kwargs)
47 def decorate_no_grad(*args, **kwargs):
48 with self:
---> 49 return func(*args, **kwargs)
50 return decorate_no_grad
51

/content/SATNet/exps/sudoku.py in test(args, epoch, model, optimizer, logger, dataset, batchSz, unperm)
270 @torch.no_grad()
271 def test(args, epoch, model, optimizer, logger, dataset, batchSz, unperm=None):
--> 272 run(args, epoch, model, optimizer, logger, dataset, batchSz, False, unperm)
273
274 @torch.no_grad()

/content/SATNet/exps/sudoku.py in run(boardSz, epoch, model, optimizer, logger, dataset, batchSz, to_train, unperm)
251 optimizer.step()
252
--> 253 err = computeErr(preds.data, boardSz, unperm)/batchSz
254 tloader.set_description('Epoch {} {} Loss {:.4f} Err: {:.4f}'.format(epoch, ('Train' if to_train else 'Test '), loss.item(), err))
255 loss_final += loss.item()

/usr/local/lib/python3.6/dist-packages/torch/autograd/grad_mode.py in decorate_no_grad(*args, **kwargs)
47 def decorate_no_grad(*args, **kwargs):
48 with self:
---> 49 return func(*args, **kwargs)
50 return decorate_no_grad
51

/content/SATNet/exps/sudoku.py in computeErr(pred_flat, n, unperm)
292 for j in range(nsq):
293 # Check the jth row and column.
--> 294 boardCorrect[invalidGroups(I[:,j,:])] = 0
295 boardCorrect[invalidGroups(I[:,:,j])] = 0
296

/content/SATNet/exps/sudoku.py in invalidGroups(x)
287 valid *= (x.max(1)[0] == nsq-1)
288 valid *= (x.sum(1) == s)
--> 289 return 1-valid
290
291 boardCorrect = torch.ones(batchSz).type_as(pred)

/usr/local/lib/python3.6/dist-packages/torch/tensor.py in rsub(self, other)
344
345 def rsub(self, other):
--> 346 return _C._VariableFunctions.rsub(self, other)
347
348 def rdiv(self, other):

RuntimeError: Subtraction, the - operator, with a bool tensor is not supported. If you are trying to invert a mask, use the ~ or logical_not() operator instead.`

Unable to install satnet through pip due to compilation error

Hello,

I was trying to install satnet using pip, but I ran into some difficulty. It appears that the compiler is unable to locate the necessary header files, even though the ./src directory is included in include_dirs, and is even visible in the -I compilation flag.

I am currently using the provided Docker environment within WSL, but I have encountered the same problem when using Ubuntu as well.

Luckily, I was finally able to set up the package by cloning the repository and installing the package locally instead.

In any case, do you have any insight into what might be causing this issue? I have attached the output I'm getting.

Thank you.

work@docker-desktop:/data$ pip install satnet
Defaulting to user installation because normal site-packages is not writeable
Collecting satnet
  Using cached satnet-0.1.4.tar.gz (10 kB)
Requirement already satisfied: torch>=1.3 in /opt/conda/lib/python3.9/site-packages (from satnet) (1.13.0)
Requirement already satisfied: typing_extensions in /opt/conda/lib/python3.9/site-packages (from torch>=1.3->satnet) (4.4.0)
Building wheels for collected packages: satnet
  Building wheel for satnet (setup.py) ... error
  ERROR: Command errored out with exit status 1:
   command: /opt/conda/bin/python -u -c 'import io, os, sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"'; __file__='"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"';f = getattr(tokenize, '"'"'open'"'"', open)(__file__) if os.path.exists(__file__) else io.StringIO('"'"'from setuptools import setup; setup()'"'"');code = f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' bdist_wheel -d /tmp/pip-wheel-wvjy7sui
       cwd: /tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/
  Complete output (20 lines):
  running bdist_wheel
  /opt/conda/lib/python3.9/site-packages/torch/utils/cpp_extension.py:476: UserWarning: Attempted to use ninja as the BuildExtension backend but we could not find ninja.. Falling back to using the slow distutils backend.
    warnings.warn(msg.format('we could not find ninja.'))
  running build
  running build_py
  creating build
  creating build/lib.linux-x86_64-3.9
  creating build/lib.linux-x86_64-3.9/satnet
  copying satnet/models.py -> build/lib.linux-x86_64-3.9/satnet
  copying satnet/__init__.py -> build/lib.linux-x86_64-3.9/satnet
  running build_ext
  building 'satnet._cpp' extension
  creating build/temp.linux-x86_64-3.9
  creating build/temp.linux-x86_64-3.9/src
  gcc -pthread -B /opt/conda/compiler_compat -Wno-unused-result -Wsign-compare -DNDEBUG -O2 -Wall -fPIC -O2 -isystem /opt/conda/include -I/opt/conda/include -fPIC -O2 -isystem /opt/conda/include -fPIC -I./src -I/opt/conda/lib/python3.9/site-packages/torch/include -I/opt/conda/lib/python3.9/site-packages/torch/include/torch/csrc/api/include -I/opt/conda/lib/python3.9/site-packages/torch/include/TH -I/opt/conda/lib/python3.9/site-packages/torch/include/THC -I/opt/conda/include/python3.9 -c src/satnet.cpp -o build/temp.linux-x86_64-3.9/src/satnet.o -fopenmp -msse4.1 -Wall -g -DTORCH_API_INCLUDE_EXTENSION_H -DPYBIND11_COMPILER_TYPE=\"_gcc\" -DPYBIND11_STDLIB=\"_libstdcpp\" -DPYBIND11_BUILD_ABI=\"_cxxabi1011\" -DTORCH_EXTENSION_NAME=_cpp -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++14
  src/satnet.cpp:28:10: fatal error: satnet.h: No such file or directory
   #include "satnet.h"
            ^~~~~~~~~~
  compilation terminated.
  error: command '/usr/bin/gcc' failed with exit code 1
  ----------------------------------------
  ERROR: Failed building wheel for satnet
  Running setup.py clean for satnet
Failed to build satnet
Installing collected packages: satnet
    Running setup.py install for satnet ... error
    ERROR: Command errored out with exit status 1:
     command: /opt/conda/bin/python -u -c 'import io, os, sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"'; __file__='"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"';f = getattr(tokenize, '"'"'open'"'"', open)(__file__) if os.path.exists(__file__) else io.StringIO('"'"'from setuptools import setup; setup()'"'"');code = f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /tmp/pip-record-98iunexk/install-record.txt --single-version-externally-managed --user --prefix= --compile --install-headers /home/work/.local/include/python3.9/satnet
         cwd: /tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/
    Complete output (22 lines):
    running install
    /opt/conda/lib/python3.9/site-packages/setuptools/command/install.py:34: SetuptoolsDeprecationWarning: setup.py install is deprecated. Use build and pip and other standards-based tools.
      warnings.warn(
    running build
    running build_py
    creating build
    creating build/lib.linux-x86_64-3.9
    creating build/lib.linux-x86_64-3.9/satnet
    copying satnet/models.py -> build/lib.linux-x86_64-3.9/satnet
    copying satnet/__init__.py -> build/lib.linux-x86_64-3.9/satnet
    running build_ext
    /opt/conda/lib/python3.9/site-packages/torch/utils/cpp_extension.py:476: UserWarning: Attempted to use ninja as the BuildExtension backend but we could not find ninja.. Falling back to using the slow distutils backend.
      warnings.warn(msg.format('we could not find ninja.'))
    building 'satnet._cpp' extension
    creating build/temp.linux-x86_64-3.9
    creating build/temp.linux-x86_64-3.9/src
    gcc -pthread -B /opt/conda/compiler_compat -Wno-unused-result -Wsign-compare -DNDEBUG -O2 -Wall -fPIC -O2 -isystem /opt/conda/include -I/opt/conda/include -fPIC -O2 -isystem /opt/conda/include -fPIC -I./src -I/opt/conda/lib/python3.9/site-packages/torch/include -I/opt/conda/lib/python3.9/site-packages/torch/include/torch/csrc/api/include -I/opt/conda/lib/python3.9/site-packages/torch/include/TH -I/opt/conda/lib/python3.9/site-packages/torch/include/THC -I/opt/conda/include/python3.9 -c src/satnet.cpp -o build/temp.linux-x86_64-3.9/src/satnet.o -fopenmp -msse4.1 -Wall -g -DTORCH_API_INCLUDE_EXTENSION_H -DPYBIND11_COMPILER_TYPE=\"_gcc\" -DPYBIND11_STDLIB=\"_libstdcpp\" -DPYBIND11_BUILD_ABI=\"_cxxabi1011\" -DTORCH_EXTENSION_NAME=_cpp -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++14
    src/satnet.cpp:28:10: fatal error: satnet.h: No such file or directory
     #include "satnet.h"
              ^~~~~~~~~~
    compilation terminated.
    error: command '/usr/bin/gcc' failed with exit code 1
    ----------------------------------------
ERROR: Command errored out with exit status 1: /opt/conda/bin/python -u -c 'import io, os, sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"'; __file__='"'"'/tmp/pip-install-yw2gliog/satnet_0e8bceaba4ac4719931aac6e4b35b01d/setup.py'"'"';f = getattr(tokenize, '"'"'open'"'"', open)(__file__) if os.path.exists(__file__) else io.StringIO('"'"'from setuptools import setup; setup()'"'"');code = f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /tmp/pip-record-98iunexk/install-record.txt --single-version-externally-managed --user --prefix= --compile --install-headers /home/work/.local/include/python3.9/satnet Check the logs for full command output.

Objective function in equation 2

Hi,

Thanks for your fantastic work! I have a question related to the objective function in relaxation of maxsat. Why we want to minimize <S^T S, V^T V>? I treated the problem as MIN-UNSAT but still couldn't figure out.

Thanks in advance!

Setup error with macOS Catalina 10.15.2

running install
running bdist_egg
running egg_info
creating satnet.egg-info
writing satnet.egg-info/PKG-INFO
writing dependency_links to satnet.egg-info/dependency_links.txt
writing requirements to satnet.egg-info/requires.txt
writing top-level names to satnet.egg-info/top_level.txt
writing manifest file 'satnet.egg-info/SOURCES.txt'
reading manifest file 'satnet.egg-info/SOURCES.txt'
writing manifest file 'satnet.egg-info/SOURCES.txt'
installing library code to build/bdist.macosx-10.7-x86_64/egg
running install_lib
running build_py
running build_ext
/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/lib/python3.6/site-packages/torch/utils/cpp_extension.py:172: UserWarning:

                           !! WARNING !!

!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
Your compiler (g++) is not compatible with the compiler Pytorch was
built with for this platform, which is clang++ on darwin. Please
use clang++ to to compile your extension. Alternatively, you may
compile PyTorch from source using g++, and then you can also use
g++ to compile your extension.

See https://github.com/pytorch/pytorch/blob/master/CONTRIBUTING.md for help
with compiling PyTorch from source.
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

                          !! WARNING !!

platform=sys.platform))
building 'satnet._cpp' extension
gcc -Wno-unused-result -Wsign-compare -Wunreachable-code -DNDEBUG -g -fwrapv -O3 -Wall -Wstrict-prototypes -I/Users/yangchen/opt/miniconda3/envs/PPO-PyTorch/include -arch x86_64 -I/Users/yangchen/opt/miniconda3/envs/PPO-PyTorch/include -arch x86_64 -I./src -I/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/lib/python3.6/site-packages/torch/include -I/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/lib/python3.6/site-packages/torch/include/torch/csrc/api/include -I/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/lib/python3.6/site-packages/torch/include/TH -I/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/lib/python3.6/site-packages/torch/include/THC -I/Users/yangchen/opt/miniconda3/envs/RL-Pytorch/include/python3.6m -c src/satnet.cpp -o build/temp.macosx-10.7-x86_64-3.6/src/satnet.o -fopenmp -msse4.1 -Wall -g -DTORCH_API_INCLUDE_EXTENSION_H -DTORCH_EXTENSION_NAME=_cpp -D_GLIBCXX_USE_CXX11_ABI=0 -std=c++11
clang: error: unsupported option '-fopenmp'
error: command 'gcc' failed with exit status 1

Instructions to fine-tune the hyper-parameters?

Hello,

Thank you for your work. It all looks very interesting.

So I installed your code and try running it on more sudoku puzzles. In terms of the number of non-empty cells, I noticed that your sudoku training data is with a mean of 36. When I tried a mean of 26, the sudoku acc dramatically drops to 0.66% on test set (aka, only got 66 right out of 10000). I trained on 10000 such sudoku puzzles with your default parameters. Is there any advice for me to fine-tune the parameters when there are fewer cells with filled digits?

Thank you in advance for any help you might be able to give me.

Unable to replicate the success on N-Queen instances

I tried adapting the code in sudoku.py for solving N-Queens problem. I formulated the problem as follows: Input instances consists of N-1 out of N queens placed on the board, with input mask placed over all the positions where queens are placed. The output is the corresponding placement of all N queens.

I am using Adam optimizer and binary cross entropy loss and I tried several values for rank and auxiliary variables but could not get any good results on test set (accuracy<40%) while I am able to get 100% accuracy for ranks as low as 10 for 10-queens problem.

I started out with m queens placed but algorithm did not perform well possibly due to multiple possible solution hence moved to the n-1 version. Moreover I tried placing mask over all the rows where queens were already placed, thus making the problem much easier than earlier however even here I was not able to get performance better than 70% on test set.

I did a sanity check on my training code by training on sudoku dataset with m=600 and aux=300 as mentioned in the default params of sudoku.py and was able to get 90+ accuracy within 20 epochs.

This leaves only two things which I may be doing wrong: choice of m and aux, or training data.

Can you suggest any help with the choice of m and aux?

Also n-queens (when n-1 queens are already placed) is much easier problem than sudoku so shouldn't it be solvable with much less data points. 10-queens has 724 solution and from each solution I can get 10 data points. This gives sufficient training data I believe. So any leads here would also be appreciated.

Question about the S matrix

Hi,

Thanks for your exciting work! I also read your previous paper about the mixing method. However, it uses a weighted matrix C instead of the S matrix (or C = S^T S). I was wondering if we can backpropagate the gradient using the implicit differentiation theorem like SATNet if we use the matrix C (as the learnable parameter) instead of the matrix S. Or if we can just use auto diff to propagate the gradient as well?

Thank you!