Implementing a Weighted Clause Container plugin¶

Sometimes (e.g. for MaxSAT) it is useful to associate a weight to a clause. Paramita also offers an interface to store such weighted clauses: WClauseContainer.

A weighted clause container extends the idea of a regular clause container by storing clauses together with a positive integer weight, or a special weight called TOP_WEIGHT, typically used to represent hard clauses.

Similarly to ClauseContainer, this class is agnostic to the semantics of the clause and the weights. It only acts as a container for them.

Class Paramita::WClauseContainer¶

A container of weighted clauses. A clause is a multiset of literals.

#include <WClauseContainer.hpp>

Inherits the following classes: Paramita::Plugin

Let's create the weighted counterpart of the CnfFormula we implemented as a clause container: a WcnfFormula.

class WcnfFormula : public WClauseContainer {
  public:
    WcnfFormula() = default;
};

The basic method to add in a container is a method to add new clauses. We have two variants, one that accepts a clause and a weight and one that only receives a clause, in which case we consider the weight to be TOP_WEIGHT.

function add_clause¶

Add a single clause with the specified weight.

virtual Paramita::WClauseContainer::add_clause (
    const Clause & clause,
    Weight weight
) = 0

Parameters:

clause The clause to be added to the container.
weight The associated weight for this clause.

class WcnfFormula : public WClauseContainer {
  public:
    void add_clause(const Clause &clause, Weight weight) override {
        Clause copy{clause.begin(), clause.end()};
        try {
            m_soft.emplace_back(std::get<std::uint64_t>(weight), copy);
        } catch (const std::bad_variant_access &) {
            // Weight was not an integer, so it is a hard clause.
            m_hard.emplace_back(copy);
        }
    }

    void add_clause(const Clause &clause) override {
        m_hard.emplace_back(clause.begin(), clause.end());
    }
  private:
    std::vector<std::tuple<std::uint64_t, Clause>> m_soft;
    std::vector<Clause> m_hard;
};

Again, we have a way to add multiple clauses at once:

function add_clauses¶

Add multiple clauses to the container.

virtual Paramita::WClauseContainer::add_clauses (
    const std::vector< Clause > & clauses,
    Weight weight
)

Parameters:

clauses The clauses to be added to the container.
weight The associated weight for the clauses.

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.

In the weighted container, this is not an absolute count, but is aggregated over the different weights.

Important

This is implementation specific (e.g. a container might remove redundant clauses), so the returned value might not correspond to the number of added 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 in the container.

virtual std::uint64_t Paramita::WClauseContainer::max_var () const = 0

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 assigned to 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 WcnfFormula : public WClauseContainer {
  public:
    void add_clause(const Clause &clause, Weight weight) override {
        for (auto lit : clause) {
            std::uint64_t var = std::abs(lit);
            m_max_var = std::max(m_max_var, var);
        }

        Clause copy{clause.begin(), clause.end()};
        try {
            m_soft.emplace_back(std::get<std::uint64_t>(weight), copy);
        } catch (const std::bad_variant_access &) {
            // Weight was not an integer, so it is a hard clause.
            m_hard.emplace_back(copy);
        }
    }

    void add_clause(const Clause &clause) override {
        for (auto lit : clause) {
            std::uint64_t var = std::abs(lit);
            m_max_var = std::max(m_max_var, var);
        }

        m_hard.emplace_back(clause.begin(), clause.end());
    }
  private:
    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.

virtual Paramita::WClauseContainer::set_minimum_var (
    std::uint64_t var
) = 0

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 WClauseContainer::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:

var The variable to be registered to the container.

Our implementation can easily add this method:

class WcnfFormula : public WClauseContainer {
    // ...
  public:
    void set_minimum_var(std::uint64_t var) override {
        m_max_var = std::max(m_max_var, var);
    }
  private:
    std::uint64_t m_max_var{0};
};

IPAMIR Compatibility¶

To be compatible with IPAMIR¹, the containers can also provide the option to add clauses literal by literal.

function add_lit¶

Add a clause literal by literal.

virtual Paramita::WClauseContainer::add_lit (
    Literal lit
)

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).

Postcondition:

After add_lit(0), the clause is added with the weight specified previously with add_weight.

See ipamir2022 and BALYO201645 for more details.

Parameters:

lit The next literal for the current clause being added, or 0 to indicate the end of the clause.

Exception:

UnsupportedMethodException This method is optional.

function add_weight¶

Changes the weight for the next clause that is added literal by literal.

virtual Paramita::WClauseContainer::add_weight (
    Weight weight
)

See also: add_lit

Parameters:

weight The weight for the next clause.

Exception:

UnsupportedMethodException This method is optional.

Next steps¶

We have seen the basic implementation of a weighted clause container plugin.

To enhance our plugin we can:

Add parameters. A weighted clause container is a Paramita::Configurable too. See the plugins page on how to add parameters.

Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental Maximum Satisfiability. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), 14:1–14:19. Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.14, doi:10.4230/LIPIcs.SAT.2022.14. ↩