Internal

Cosy Internal Datas

All modern SAT solver uses variables, literals and clauses as datas structure. To be interfaced with any CDCL SAT solver cosy has it own representation.

Internal Data

Variables

typedef unsigned int Var;

• 0 means VAR_UNDEF
• start from 1

Literal

typedef unsigned int Var;

• 0 means LIT_UNDEF
• start from 1 for positive literal
• start from -1 for negative literal

Clause

typedef std::vector<Lit> Clause;

• use classic std::vector methods

cosy configuration

Here are the methods to configure cosy:

• activateLexLeaderForcing();
• order(order_type, value_type);

activateLexLeaderForcing();

This method actives the lex leader forcing which is disable on the beginning.

order(order_type, value_type);

This method define the LexLeader.

order_type

• cosy::OrderType::INCREASING 1 2 3 ... n
• cosy::OrderType::CLASS_OCCURENCE pack variables acording to their orbit, sorted their occurence
• cosy::OrderType::OCCURENCE sort according to number of occurence of each variables

value_type

• cosy::T_LESS_F true literal less than false literal
• cosy::F_LESS_T false literal less than true literal