Generating cubes with propagators¶
In this tutorial, we will use Propagators to generate cubes that could be exploited by a Cube-and-Conquer approach.
First, we will discuss the Cube-and-Conquer problem. Then, we will implement a Python version for our cubing approach. Finally, we will implement the C++ equivalent version, and see how to use it in our Python code.
The Cube-and-Conquer solving approach¶
Cube-and-Conquer1 is a solving approach that consists in splitting the SAT problem into sub-problems that can be solved in parallel. To this end, we need to generate cubes (i.e., conjunction of literals) that can be set as assumptions. The idea is that these sub-problems tend to be easier for the current SAT solvers.
As explained in the cited paper, cubes are partial assignments, corresponding to initial parts of the path from the root to leaves in the splitting (branching) tree, and the task is to "cut off" these paths at the right place.
In the following implementations, we propose to use the inner heuristic of a SAT solver to generate these paths, and enforce its "cut-off" by using Propagators2, a class implementing some callbacks that can modify the internal search process of SAT solvers.
Python implementation¶
First, we will create a subclass of paramita.solvers.Propagator, which we will call CubingEngine.
This class will receive as parameters the desired maximum depth for cubes and a blocking variable that we can use to deactivate the clauses that this propagator introduces.
Then, we will record the generated cubes in the self.cubes_ variable, and we will replicate the solver's trail data structure through the self.decision_level, self.trail and self.trlim data structures:
from paramita.solvers import SatSolver, Propagator
class CubingEngine(Propagator):
def __init__(self, depth: int, blocking_var: int) -> None:
super().__init__()
self.depth = depth
self.blocking_var = blocking_var
self.cubes_: list[list[int]] = []
self._solver = None
self.decision_level = 0
self.trail: list[int] = []
self.trlim: list[int] = []
We also create the setup_observemethod, an auxiliary method that is outside of the Propagator interface that we will use to store the SAT solver in a variable and observe all the variables in the formula:
def setup_observe(self, solver):
self._solver = solver
# Observe all the variables
vars = [i + 1 for i in range(self._solver.max_var())]
for v in vars:
self._solver.add_observed_var(v)
self._solver.add_observed_var(self.blocking_var)
Next, we implement the Propagator interface methods on_assignment, on_new_decision_level and on_backtrack, that we use to reproduce the trail data structure in the SAT solver.
The only difference is that in the on_assignment method, we only store the assigned literals that belong to decision variables and that are different from the blocking variable.
def on_assignment(self, lits) -> None:
for lit in lits:
if self._solver.is_decision(lit) and abs(lit) != self.blocking_var:
# We only consider the literals that are decided
self.trail.append(lit)
def on_new_decision_level(self) -> None:
self.decision_level += 1
self.trlim.append(len(self.trail))
def on_backtrack(self, to):
# undoing the assignments
while len(self.trlim) > to:
while len(self.trail) > self.trlim[-1]:
self.trail.pop()
self.trlim.pop()
# updating decision level
self.decision_level = to
Whenever the size of the trail is greater or equals than the required depth, we notify that we have an external clause through the has_external_clause method, and add the clause to the solver in the get_external_clause method.
The only detail is that we block each clause using self.blocking_var to allow its deactivation in case we use the SAT solver incrementally.
def has_external_clause(self):
return len(self.trail) >= self.depth
def get_external_clause(self):
if len(self.trail) >= self.depth:
self.cubes_.append(list(self.trail))
clause = [self.blocking_var] + [-lit for lit in self.trail]
return clause
return []
Finally, if the SAT solver finds a model, we just return True in the check_found_model method and end the cubing procedure (as the formula has already been solved).
Using the Python CubingEngine¶
Prerequisites
You need a SAT solver compiled as a Paramita extension. Start by fetching Cadical 2.2.1 from the Paramita Plugins repository using the CLI helper:
For more information you can check the Building an external Plugin section.
To use this propagator, we first load a SAT solver with support for propagators (for example, CaDiCaL 2.2.1). We load a CNF instance to the SAT solver and parse the desired depth:
import sys
from paramita.io import load_cnf
s = SatSolver.from_name("Cadical221")
load_cnf(sys.argv[1], s)
print("Instance loaded")
depth = int(sys.argv[2])
print("Num vars:", s.max_var(), flush=True)
print("Num clauses:", s.num_clauses(), flush=True)
Then, we initialize the CubingEngine and conect it to the SAT solver as follows:
blocking_var = s.max_var() + 1
prop = CubingEngine(depth=depth, blocking_var=blocking_var)
s.connect_external_propagator(prop)
prop.setup_observe(s)
Finally, we solve the problem by setting -blocking_var as assumptions, and retrieve the generated cubes from the propagator:
is_sat = s.solve([-blocking_var])
print("Is sat:", is_sat, flush=True)
print(f"Num cubes: {len(prop.cubes_)}", flush=True)
We are done!
This is the full source code for the Python implementation and usage of CubingEngine:
from paramita.solvers import SatSolver, Propagator
class CubingEngine(Propagator):
def __init__(self, depth: int, blocking_var: int) -> None:
super().__init__()
self.depth = depth
self.blocking_var = blocking_var
self.cubes_: list[list[int]] = []
self._solver = None
self.decision_level = 0
self.trail: list[int] = []
self.trlim: list[int] = []
def setup_observe(self, solver):
self._solver = solver
# Observe all the variables
vars = [i + 1 for i in range(self._solver.max_var())]
for v in vars:
self._solver.add_observed_var(v)
self._solver.add_observed_var(self.blocking_var)
def on_assignment(self, lits) -> None:
for lit in lits:
if self._solver.is_decision(lit) and abs(lit) != self.blocking_var:
# We only consider the literals that are decided
self.trail.append(lit)
def on_new_decision_level(self) -> None:
self.decision_level += 1
self.trlim.append(len(self.trail))
def on_backtrack(self, to):
# undoing the assignments
while len(self.trlim) > to:
while len(self.trail) > self.trlim[-1]:
self.trail.pop()
self.trlim.pop()
# updating decision level
self.decision_level = to
def has_external_clause(self):
return len(self.trail) >= self.depth
def get_external_clause(self):
if len(self.trail) >= self.depth:
self.cubes_.append(list(self.trail))
clause = [self.blocking_var] + [-lit for lit in self.trail]
return clause
return []
def check_found_model(self, model) -> bool:
return True
def main():
import sys
from paramita.io import load_cnf
s = SatSolver.from_name("Cadical221")
load_cnf(sys.argv[1], s)
print("Instance loaded")
depth = int(sys.argv[2])
print("Num vars:", s.max_var(), flush=True)
print("Num clauses:", s.num_clauses(), flush=True)
blocking_var = s.max_var() + 1
prop = CubingEngine(depth=depth, blocking_var=blocking_var)
s.connect_external_propagator(prop)
prop.setup_observe(s)
is_sat = s.solve([-blocking_var])
print("Is sat:", is_sat, flush=True)
print(f"Num cubes: {len(prop.cubes_)}", flush=True)
if __name__ == "__main__":
main()
C++ implementation¶
In this section we will show how to implement an equivalent version of the Python CubingEngine in C++.
Project setup¶
We will use cmake to compile our CubingEngine C++ plugin.
The project structure that we will use is the following:
cubing-cpp/
├── cmake
│ ├── Finddoctest.cmake
│ ├── ParamitaInterfaces.cmake
│ └── plugin.cmake
├── CMakeLists.txt
├── cubing.py
├── propagator.cpp
└── propagator.hpp
cmake/contains all the required CMakeLists files, which are provided by Paramita. You can find them here.CMakeLists.txtis thecmakefile that we will use to compile the plugin.cubing.pywill contain the Python code that will run the plugin.propagator.cppandpropagator.hppcontain the implementation and headers of our plugin.
Setting up CMake¶
Paramita already provides a set of cmake files to develop plugins in C++.
In our case, we will need to download the plugin.cmake, ParamitaInterfaces.cmake and Finddoctest.cmake files from the git+https://codeberg.org/paramita/paramita-plugins.git repository.
We will add those to the cmake/ folder.
Then, we will create the following CMakeLists.txt:
cmake_minimum_required(VERSION 3.16..3.30)
project(CubingEngineCpp
VERSION "1.0"
LANGUAGES CXX
)
set(TARGET_NAME cubing-engine-cpp)
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
propagator.hpp
propagator.cpp
)
set_target_properties(${TARGET_NAME}
PROPERTIES
LINKER_LANGUAGE CXX
POSITION_INDEPENDENT_CODE ON
)
target_link_libraries(${TARGET_NAME}
PUBLIC
Paramita::interfaces
)
Essentially, we define the project name and TARGET_NAME, and include the plugin cmake file, which is located at the ${CMAKE_CURRENT_LIST_DIR}/cmake folder.
Then, we just add the ${TARGET_NAME} library as a shared library, including the propagator.hpp and propagator.cpp files.
We also specify the LINKER_LANGUAGE to CXX and activate POSITION_INDEPENDENT_CODE.
Finally, we link against Paramita::interfaces.
Implementing the C++ CubingEngine¶
As we did in the Python version, we need to create a subclass of paramita.solvers.Propagator, as we do in propagator.hpp, and implement all the Propagator interface required methods:
#pragma once
#include <memory>
#include <vector>
#include <string>
#include <unordered_map>
#include <variant>
#include <iostream>
#include <paramita/plugin/ParameterSpace.hpp>
#include <paramita/sat/Propagator.hpp>
#include <paramita/sat/SatSolver.hpp>
using namespace Paramita;
class CubingEngineCpp : public Propagator
{
public:
void on_assignment(const std::vector<int> &lits) override
{
for (const auto &lit : lits)
{
if (solver->is_decision(lit) && std::abs(lit) != blocking_var)
{
trail.push_back(lit);
}
}
}
void on_new_decision_level() override
{
decision_level++;
trlim.push_back(trail.size());
}
void on_backtrack(std::size_t new_level) override
{
while (trlim.size() > new_level)
{
while (trail.size() > trlim[trlim.size() - 1])
{
trail.pop_back();
}
trlim.pop_back();
}
decision_level = new_level;
}
bool check_found_model(const std::vector<int> &model) override { return true; };
bool has_external_clause() override
{
return trail.size() >= depth;
}
std::vector<int> get_external_clause() override
{
if (trail.size() >= depth)
{
m_cubes_.push_back(trail);
std::vector<int> clause;
clause.push_back(blocking_var);
for (const auto &lit : trail)
{
clause.push_back(-lit);
}
return clause;
}
return {};
}
ParameterSpace get_parameter_space() override
{
return ParameterSpace({{"depth", IntegerParameter(3, {1, 1000})},
{"blocking_var", IntegerParameter(0, {1, 100000000})},
{"solver", SatSolverParameter()}});
}
void set(const std::string &name, const ParameterType &value) override
{
if (name == "depth")
{
depth = std::get<int>(value);
}
else if (name == "blocking_var")
{
blocking_var = std::get<int>(value);
}
else if (name == "solver")
{
solver = std::get<std::shared_ptr<SatSolver>>(value);
}
else
{
throw std::runtime_error("Unknown parameter.");
}
}
std::vector<std::string> get_out_data_keys() const override
{
return {"cubes_"};
};
OutData::Value get_out_data(const std::string &key) const override
{
if (key == "cubes_")
{
return OutData::to_value(m_cubes_);
}
return nullptr;
}
private:
int depth = 3;
int blocking_var = 0;
std::shared_ptr<SatSolver> solver;
std::vector<std::vector<int>> m_cubes_;
int decision_level = 0;
std::vector<int> trail;
std::vector<int> trlim;
};
In this case, we included all the implementation in the header file.
However, we need to specify the EXTERNAL_PROPAGATOR_C_INTERFACE macro in propagator.cpp to register the CubingEngineCpp class as a Paramita plugin:
Compiling the C++ CubingEngine plugin¶
For this example, we will compile the extension manually, so we generate a .so that we will load in Python using the Propagator.dynamic_load(...) static method.
Note
We assume that all these commands are executed within the project's root.
First, we will geneare the required cmake files:
cmake -S . -B build/ -DCMAKE_BUILD_TYPE=Release -DPARAMITA_SKIP_LINTS=ON -DPARAMITA_TEST_PLUGINS=OFF
This is the meaning of the passed flags:
-DCMAKE_BUILD_TYPE=Release: Sets the build type to Release.-DPARAMITA_SKIP_LINTS=ON: Skips linting, as in Paramita warnings are treated as errors.-DPARAMITA_TEST_PLUGINS=OFF: We don't have tests, so we skip Paramita's testing pipeline.
The expected output of this command would be similar to this:
-- The CXX compiler identification is GNU 12.2.0
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
CMake Warning at cmake/ParamitaInterfaces.cmake:19 (message):
Using the default tag for paramita interfaces
(d3069cb24a7444f76e6c2bfaa2c020766d666414)
Call Stack (most recent call first):
cmake/plugin.cmake:33 (include)
CMakeLists.txt:10 (include)
-- Fetching paramita-interfaces@d3069cb24a7444f76e6c2bfaa2c020766d666414 from git repository
-- Configuring done
-- Generating done
-- Build files have been written to: /workspaces/paramita/examples/cubing/cubing-cpp/build
Finally, we compile the plugin:
This would generate the file build/libcubing-engine-cpp.so.
For this example, we won't execute the install step, as this is not required when using the dynamic_load method.
For other compilation alternatives and options check the Building an external Plugin section.
Using the C++ CubingEngine¶
Prerequisites
You need a SAT solver compiled as a Paramita extension. Start by fetching Cadical 2.2.1 from the Paramita Plugins repository using the CLI helper:
For more information you can check the Building an external Plugin section.
Once we have built the C++ extension, we can implement the cubing.py file, which will be very similar to the one that we have seen in the Python version:
import sys
from paramita.solvers import SatSolver, Propagator
from paramita.io import load_cnf
def main():
s = SatSolver.from_name("Cadical221")
load_cnf(sys.argv[1], s)
print("Instance loaded")
depth = int(sys.argv[2])
print("Num vars:", s.max_var(), flush=True)
print("Num clauses:", s.num_clauses(), flush=True)
blocking_var = s.max_var() + 1
prop = Propagator.dynamic_load("build/libcubing-engine-cpp.so")
prop.set("depth", depth)
prop.set("blocking_var", blocking_var)
prop.set("solver", s)
s.connect_external_propagator(prop)
vars = [i + 1 for i in range(s.max_var())]
for v in vars:
s.add_observed_var(v)
s.add_observed_var(blocking_var)
is_sat = s.solve([-blocking_var])
print("Is sat:", is_sat, flush=True)
print(f"Num cubes: {len(prop.cubes_)}", flush=True)
if __name__ == "__main__":
main()
In this case, we load the CubingEngineCpp through the dynamic_load function using its path (if compiled following the instructions and executed in the project's root, this corresponds to build/libcubing-engine-cpp.so).
Then, we have to observe the variables and setup de SAT solver, instead of doing that in the setup_observe method that we implemented in the Python version.
The output cubes can be accessed in the same way through the prop.cubes_ attribute.
-
Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: guiding cdcl sat solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing, 50–65. Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. ↩
-
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), 8:1–8:13. Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.8, doi:10.4230/LIPIcs.SAT.2023.8. ↩