Integration

Integration in Minisat SAT solver

Here, we show how cosy is integrated to the Minisat SAT solver. It needs the three following parts:

• The creation of Adapter to allow communication between MiniSAT and cosy.
• The initialisation and configuration of cosy.
• The calls of the APIs of cosy in MinisSAT.

Creation of the adapter.

cosy has it [internal representation](see Internal.md) of variables, literals and clauses. Hence, its integration within MiniSAT needs the implementation of a simple adapter whose declaration is given here include/cosy/LiteralAdapter.h

Here is the implementation of this interface:

namespace Minisat {

class MinisatLiteralAdapter : public cosy::LiteralAdapter<Minisat::Lit>
{
 public:
        MinisatLiteralAdapter() {}
        ~MinisatLiteralAdapter() {}

        virtual Minisat::Lit convert(cosy::Lit l) {
            return mkLit(cosy::varOf(l) - 1, cosy::sign(l));
        }

        virtual cosy::Lit convert(Minisat::Lit lit) {
            return (sign(lit) ? -(var(lit) + 1) : var(lit) + 1);
        }
};
}

The full code of this adapter is available at adapters/MinisatLiteralAdapter.h

Initialisation and Configuration of cosy.

Declare the symmetry controller in the solver header (core/Solver.h)

    std::unique_ptr<cosy::SymmetryController<Lit>> symmetry;

Create the adapter in the main file (core/Main.cc)

        std::unique_ptr<cosy::LiteralAdapter<Minisat::Lit>> adapter
            (new MinisatLiteralAdapter());

Create the symmetry controller with the adapter and the number of variables in the CNF instances as parameters.

        S.symmetry = std::unique_ptr<cosy::SymmetryController<Minisat::Lit>>
            (new cosy::SymmetryController<Minisat::Lit>(S.nVars(), adapter));

Initialize the symmetry controller with the CNF instance and a symmetry generators file.

        std::string symmetry_file = std::string(sym_file);
        std::string cnf_file = std::string(argv[1]);

        if (!S.symmetry->initialize(cnf_file, symmetry_file))
            S.symmetry = nullptr;

Before stating to compute CDCL solver, configure the symmetry controller (file core/Solver.cc)

lbool Solver::solve_()
    ...
    // Set symmetry order
    if (symmetry != nullptr) {
        // symmetry->activateLexLeaderForcing();
        symmetry->order(cosy::OrderType::OCCURENCE, cosy::T_LESS_F);
        symmetry->printInfo();
    }

Call of the cosy library APIs.

cosy API has 4 functions:

• updateNotify - symmetry controller update permutations status on affection action of solver
• updateCancel - symmetry controller update permutations status on cancel action of solver
• isNotLexLeader - solver asks symmetry controller if the current assigment is a possible lex-leader.
• generateEsbp - symmetry controller generate an effective symmetry breaking predicates (esbp) to avoid exploring isomorphic search space.

When LexLeaderForcing is actived, the solver needs to call also:

• canForceLexLeader - solver asks symmetry controller if it can force lex-leader
• generateForceLexLeaderEsbp - symmetry controller create an esbp to force a possible lex-leader assigment.

Let call this API on Minisat source code:

Update Symmetry status on affectation (file core/Solver.cc)

void Solver::uncheckedEnqueue(Lit p, CRef from) {
    ...
    if (symmetry != nullptr)
        symmetry->updateNotify(p, decisionLevel());
}

Update Symmetry status on cancel (file core/Solver.cc)

void Solver::cancelUntil(int level) {
    ...
     assigns [x] = l_Undef;
	 if (symmetry != nullptr)
        symmetry->updateCancel(trail[c]);
}

Generation of ESBP on need (file core/Solver.cc)

CRef Solver::propagate() {
        ...
        num_props++;
        /* Learning of Esbp */
        if (symmetry != nullptr) {
            if (symmetry->isNotLexLeader(p)) {
                /* Generate SBP */
                std::vector<Lit> vsbp = symmetry->generateEsbp();

                // Dirty make a copy of vector
                vec<Lit> sbp;
                for (Lit l : vsbp)
                    sbp.push(l);

                if (sbp.size() == 1) {
                    cancelUntil(0);
                    uncheckedEnqueue(sbp[0]);
                } else {
                    CRef cr = ca.alloc(sbp, true);
                    learnts.push(cr);
                    attachClause(cr);
                }
            }
        }
        ...

Generation of ESBP for the lex-leader forcing (file core/Solver.cc)

CRef Solver::propagate() {
        ...
        ws.shrink(i - j);
        /* Forcing Lex Leader */
        if (confl == CRef_Undef && qhead == trail.size() && symmetry != nullptr) {
	    while (symmetry->canForceLexLeader()) {
		Lit propagate;
		vec<Lit> reason;
                std::vector<Lit> r;

                r = symmetry->generateForceLexLeaderEsbp(&propagate);
                // Copy can be avoided
                for (Lit l : r)
                    reason.push(l);

		if (value(propagate) != l_Undef)
		    continue;
		CRef cr = ca.alloc(reason, true);
		learnts.push(cr);
		attachClause(cr);
 		uncheckedEnqueue(propagate, cr);
	    }
	}
    propagations += num_props;
    simpDB_props -= num_props;

    return confl;
}

The last point is to link your solver with libcosy.