Adding a `PbToCnfEncoder` to Paramita: the naive pairwise encoder¶

In this tutorial we will add the pairwise encoder to Paramita by extending the C++ PbToCnfEncoder class.

The pairwise encoding enforces an At-Most-One rule by ensuring that no two variables can be true simultaneously. Given a set of \(n\) boolean variables, it creates a binary clause for every unique pair of variables, forcing at least one of them to be false:

\[\neg x_i \lor \neg x_j, \text{ for all } 1 \leq i < j \leq n\]

Project setup¶

As in the cubing example using Propagators, we will use cmake to compile our PairwiseEncoder plugin. The project structure that we will follow is this one:

pairwise/
├── cmake
│   ├── Finddoctest.cmake
│   ├── ParamitaInterfaces.cmake
│   └── plugin.cmake
├── CMakeLists.txt
├── encoder.cpp
├── encoder.hpp
└── test_pairwise.cpp

cmake/ contains all the required CMakeLists files, which are provided by Paramita. You can find them here.
CMakeLists.txt is the cmake file that we will use to compile the plugin.
encoder.cpp and encoder.hpp contain the implementation and headers of our plugin.

Setting up CMake¶

The specification of the CMakeLists.txt file is shown below:

cmake_minimum_required(VERSION 3.16..3.30)

project(PairwiseEncoding
    VERSION "1.0"
    LANGUAGES CXX
)
set(TARGET_NAME pairwise-encoder)

list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_LIST_DIR}/cmake")
include(plugin)

# Extension definition
# ====================
# Declare the binding
add_library(${TARGET_NAME}
    SHARED  # compile as an *.so
    encoder.cpp
    encoder.hpp
)
set_target_properties(${TARGET_NAME}
    PROPERTIES
    LINKER_LANGUAGE CXX
    POSITION_INDEPENDENT_CODE ON
)

target_link_libraries(${TARGET_NAME}
    PUBLIC
    Paramita::interfaces
)

# Testing
# =======
if (PARAMITA_TEST_PLUGINS)
    set(TEST_TARGET "test-${TARGET_NAME}")

    # Create test target
    add_executable(${TEST_TARGET} test_pairwise.cpp)
    target_link_libraries(${TEST_TARGET}
            PRIVATE
            ${TARGET_NAME}
    )
    ParamitaInterfaces_discover_tests(${TEST_TARGET})
endif ()

# How to install
install(
    TARGETS ${TARGET_NAME}
    LIBRARY DESTINATION pb-to-cnf-encoders
)

For more information you can check the Setting up CMake section of the cubing Plugin tutorial.

Implementing the encoder¶

We will just need to implement the encode method of the PbToCnfEncoder C++ interface. The header definition in encoder.hpp is the following:

#pragma once

#include <paramita/Exceptions.hpp>
#include <paramita/sat/PbToCnfEncoder.hpp>

using namespace Paramita;

class PARAMITA_EXPORT PairwiseEncoder : public PbToCnfEncoder {
public:
    PairwiseEncoder() {};
    ~PairwiseEncoder() override {};
    PairwiseEncoder(const PairwiseEncoder &) = delete;
    PairwiseEncoder &operator=(const PairwiseEncoder &) = delete;
    PairwiseEncoder(PairwiseEncoder &&) = delete;
    PairwiseEncoder &operator=(PairwiseEncoder &&) = delete;

    Context encode(
        const PbConstraint &constraint, ClauseContainer &container,
        Context context
    ) override;
};

And the implementation in encoder.cpp is this one:

#include "encoder.hpp"
#include <paramita/Exceptions.hpp>

#include <algorithm>

using namespace Paramita;

PbToCnfEncoder::Context PairwiseEncoder::encode(
    const PbConstraint &constraint, ClauseContainer &container, Context context
) {

    if (context) {
        throw UnsupportedMethodException(
            "Unsupported context. This is a non-incremental encoder."
        );
    }

    if (constraint.op != PbConstraint::LTE || constraint.bound != 1) {
        throw UnsupportedMethodException("Only '<= 1' is supported");
    }

    if (constraint.weights.has_value()) {
        std::vector<int64_t> weights = constraint.weights.value();
        if (!std::all_of(weights.begin(), weights.end(), [](int i) {
                return i == 1;
            })) {
            throw UnsupportedMethodException("Only unweighted is supported");
        }
    }

    for (int i = 0; i < (int)constraint.lits.size() - 1; ++i) {
        for (int j = i + 1; j < (int)constraint.lits.size(); ++j) {
            container.add_clause({-constraint.lits[i], -constraint.lits[j]});
        }
    }

    return {}; // Empty context
};

PB_TO_CNF_ENCODER_C_INTERFACE(PairwiseEncoder, "", "", "", "", "");

First, we ensure we have an empty context, as the pairwise encoding in non-incremental (Context is only used in incremental encoders).
Then, we ensure that the user provided us with a \(\leq 1\) Pseudo-Boolen constraint, as this is the only one that we will support.
We also ensure that we have no weights (so all weights are 1) or that the user specified explicitly all weights set to 1.
We then have the specific implementation for the encoder, and we add each of the resulting clauses to the container.
Finally, we return an empty Context.

Note

Notice that we have to call the PB_TO_CNF_ENCODER_C_INTERFACE(PairwiseEncoder); macro to register this implementation as a Paramita plugin.

Compiling the plugin¶

As we did with the CubingEngine compilation, we will compile the extension manually to generate an .so file that we can load in Python using the Propagator.dynamic_load(...) static method:

cmake -S . -B build/ -DCMAKE_BUILD_TYPE=Release -DPARAMITA_SKIP_LINTS=ON -DPARAMITA_TEST_PLUGINS=OFF

cmake --build build/

This would generate the build/libpairwise-encoder.so file, which we can then load in python using the PbToCnfEncoder.dynamic_load("build/libpairwise-encoder.so") method.

Adding a PbToCnfEncoder to Paramita: the naive pairwise encoder¶