Implementing a Clause Container plugin¶
ClauseContainer defines the interface for a container
that stores clauses, which are fundamental structures in SAT
solvers and related algorithms. The container is responsible
for storing clauses and keeping track of the variables involved
in a problem.
Each variable has a unique positive integer associated (its identifier).
A literal represents a variable and a polarity (a literal), the convention followed is that a positive integer represents a variable, and a negated integer represents its negation.
A clause is defined as a sequence of literals.
Note
A clause is usually considered as a logical OR of literals (called CNF), though this class is totally agnostic of this meaning. In can, for example, be used to represent DNFs.
Class Paramita::ClauseContainer¶
A container of clauses.
The variables used in this container are represented as an integer larger than 0 (its identifier), as in the DIMACS CNF format.
A clause is composed by literals, which are a variable or its negation. A negated variable is represented by negating its identifier.
This interface acts as a clause container, in the sense that we can add new clauses and (optionally) keep track on how many clauses we added. No additional assumptions are made on how the container stores them (or even if they are stored at all). Specializations of this interface might provide additional methods to retrieve clauses, but this is not part of the interface.
#include <ClauseContainer.hpp>
Inherits the following classes: Paramita::Plugin
Let's create a container that holds clauses in CNF in a vector, a CnfFormula.
class CnfFormula : public ClauseContainer {
public:
CnfFormula() = default;
private:
std::vector<Clause> m_clauses;
};
The basic method to add in a container is a method to add new clauses:
function add_clause¶
Add a single clause.
The clause is represented as a sequence of literals. Each literal is represented as an integer, where its absolut value is the identifier of a variable. A positive integer represents the variable and a negative integer its negation.
Parameters:
clauseThe clause to be added to the container.
class CnfFormula : public ClauseContainer {
// ...
public:
void add_clause(const Clause& clause) {
m_clauses.emplace_back(clause.begin(), clause.end());
}
private:
std::vector<Clause> m_clauses;
};
If we had a special way to add more than one clause at the same time, we could
overwrite the add_clauses method:
function add_clauses¶
Add multiple clauses to the container.
The default implementation will call add_clause once per element in the vector.
See also: add_clause
Parameters:
clausesThe clauses to be added to the container.
The container can keep track of how many clauses it is holding at the moment,
and the users can query this by using the num_clauses method.
Note
This is implementation specific (e.g. a container might remove redundant clauses), so the returned value might not be the same as how many clauses were added previously.
function num_clauses¶
Get the number of clauses hold currently by the container.
This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.
Returns:
The number of clauses held by the container.
Exception:
- UnsupportedMethodException This method is optional.
Let's add this method to our formula:
class CnfFormula : public ClauseContainer {
// ...
public:
[[nodiscard]] int num_clauses() const override {
return (int)m_clauses.size();
}
private:
std::vector<Clause> m_clauses;
};
Keeping track of DIMACS variables¶
The container is responsible to keep track of the variables that
are used in the added clauses.
The largest variable seen by the container can be retrieved through
the max_var function. This allows the user to know the upper bound
of variables currently in use. It is also important to note that
gaps may exist between variable identifiers.
Warning
Note that even if internally the container removes clauses, it cannot delete variables as the user might still use them in future clauses.
function max_var¶
Get the largest variable used by the container.
The largest variable is determined by its identifier.
Note:
Note that this does not mean that the container has clauses containing literals for all the variables between 1 and CnfContainerinterface::max_var, there may be gaps.
Warning:
If the container creates variables internally, this method MUST also consider those variables, even if the user did not add them directly. This ensures that the user cannot generate variable clashes when adding new clauses to the container.
Postcondition:
The return value is equal or larger to the absolute value for any literal passed to add_clause, add_clauses, or add_lit.
Returns:
The (positive) integer representing the largest variable.
To keep track of the maximum variable in our example, let's modify add_clause
to update this information, and implement max_var:
class CnfFormula : public ClauseContainer {
// ...
public:
void add_clause(const Clause& clause) {
for (auto lit : clause) {
std::uint64_t var = std::abs(lit);
m_max_var = std::max(m_max_var, var);
}
m_clauses.emplace_back(clause.begin(), clause.end());
}
[[nodiscard]] std::uint64_t max_var() const override {
return m_max_var;
}
private:
std::vector<Clause> m_clauses;
std::uint64_t m_max_var{0};
};
Users might consider variables that have not been seen by the container on
any added clause. To ensure that the container keeps track of the correct
variables, the users can set a minimum variable such that, from that point,
the container must consider it along with the ones seen previously in clauses.
This ensures the correct behaviour in procedures that rely on calling max_var
to generate new variables internally (such as auxiliary variables).
function set_minimum_var¶
Sets the maximum variable known to the container to at least this one.
This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the ClauseContainer::max_var method to determine the next free variable, this method ensures that existing variables cannot be reused.
Postcondition:
The value returned by max_var must be larger or equal than the one provided.
Postcondition:
The value returned by max_var cannot be reduced by this call.
Parameters:
varThe variable to be registered to the container.
Our implementation can easily add this method:
class CnfFormula : public ClauseContainer {
// ...
public:
void set_minimum_var(std::uint64_t var) override {
m_max_var = std::max(m_max_var, var);
}
private:
std::vector<Clause> m_clauses;
std::uint64_t m_max_var{0};
};
IPASIR Compatibility¶
To be compatible with IPASIR1, the containers can also provide the option to add clauses literal by literal.
function add_lit¶
Add a clause literal by literal.
This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).
See BALYO201645 for more details.
Parameters:
litThe next literal for the current clause being added, or 0 to indicate the end of the clause.
Exception:
- UnsupportedMethodException This method is optional.
Next steps¶
We have seen the basic implementation of a clause container plugins.
To enhance our plugins we can:
- Add parameters. A clause container is a
Paramita::Plugintoo. See the plugins page on how to add parameters.
-
Tomáš Balyo, Armin Biere, Markus Iser, and Carsten Sinz. Sat race 2015. Artificial Intelligence, 241:45–65, 2016. URL: https://www.sciencedirect.com/science/article/pii/S0004370216300984, doi:https://doi.org/10.1016/j.artint.2016.08.007. ↩