Classes and methods - marcbenedi/SAT-tfg GitHub Wiki

Disclaimer This page will be replaced by doxygen documentation as soon as possible. Meanwhile it is fully updated.

BDDConverter

     

static BDD convertFormula(Formula const & boolFunc)

Converts the given Formula to a BDD.

BinarySearchStrategy

     

BinarySearchStrategy()

     

void init(const PBMin & problem) override

Initializes the algorithm, must be called before loop() and end(). PBMin problem defines the problem to be solved.

     

void loop(void (Solver::*solve)(std::vector< int32_t > &, const std::vector< std::vector< int32_t > > &, bool &),std::vector< int32_t > & model, int64_t & min, bool &sat, Solver *solver, const PBMin & problem)override

This function executes the binary search algorithm. Must be executed between init() and end()

  • solve : function which takes 3 arguments (model, cnf, sat) and solves the given cnf storing the assignment in model and storing in sat its satisfiability
  • model : a structure where model will be stored
  • min : a int64_t where the minimum value for the cost function will be stored
  • sat : a boolean where the satisfiability of the problem will be stored
  • solver : the solver used to solve this problem
  • problem : the problem to be solved

     

void end() override;

Finishes the execution of this class, in this implementation it does nothing. Must be called after loop()

BoolFunc

This class should not be called by the user because it is designed as an internal class. See Formula for more information.

     

BoolFunc()

     

BoolFunc(const std::string & name)

Builds a Boolean formula of the type NOD_ID identified by name.

     

BoolFunc(NodeType param_type, Formula const & param_child)

     

BoolFunc(NodeType param_type, Formula const & left, Formula const & right)

     

BoolFunc(NodeType param_type, Formula const & left, Formula const & right, int param_value)

     

NodeType getType() const

     

int getValue() const

     

const Formula getChild1() const

     

const Formula getChild2() const

     

void setType(NodeType t)

     

void setValue(int v)

     

void setChild1(Formula const & c)

     

void setChild2(Formula const & c)

Formula

     

static Formula newNot(Formula const & f)

Returns a new Formula which is equivalent to not f. The use of operators is more recommendable than this function.

     

static Formula newAnd(Formula
        const & a, Formula
        const & b)

Returns a new Formula which is equivalent to a and b. The use of operators is more recommendable than this function.

     

static Formula newOr(Formula
        const & a, Formula
        const & b)

Returns a new Formula which is equivalent to a or b. The use of operators is more recommendable than this function.

     

static Formula newXor(Formula
        const & a, Formula
        const & b) ;

Returns a new Formula which is equivalent to a xor b. The use of operators is more recommendable than this function.

     

static Formula newLit(std::string var_name)

Returns a new Formula which represents a Boolean variable identified by var_name

     

void print(int level=0) const

Print the Formula as a tree. Useful for debugging.

     

Formula operator!(Formula const & f)

Returns a new Formula which is equivalent to not f

     

Formula operator~(Formula const & f)

Returns a new Formula which is equivalent to not f

     

Formula operator & (Formula const & a, Formula const & b)

Returns a new Formula which is equivalent to a and b

     

Formula operator * (Formula const & a, Formula const & b)

Returns a new Formula which is equivalent to a and b

     

Formula operator | (Formula const & a, Formula const & b)

Returns a new Formula which is equivalent to a or b

     

Formula operator + (Formula const & a, Formula const & b)

Returns a new Formula which is equivalent to a or b

     

Formula operator ^ (Formula const & a, Formula const & b)

Returns a new Formula which is equivalent to a xor b

     

Formula operator += (const Formula & lhs, const Formula & rhs)

The Formula lhs becomes lhs or rhs

     

Formula operator *= (const Formula & lhs, const Formula & rhs)

The Formula lhs becomes lhs and rhs

     

Formula operator ^= (const Formula & lhs, const Formula & rhs)

The Formula lhs becomes lhs xor rhs

Clause

     

Clause()

     

Clause(int n, ...)

Initializes the class with n literals

  • n : the number of literals in the clause
  • ... : an array of literals of size n

     

void addVar(int v)

     

void print() const

     

std::string picosat() const

Prints the Clause in Picosat format

     

void clear()

     

int getNumVars() const

     

int getVar(int i) const

Returns the variable at position i

Cnf

     

Clause getClause(int i) const

     

int getClauseNumber() const

     

int getNumVars() const

     

void addClause(Clause const & clause)

     

void addCnf(Cnf const & param)

     

void addUnsat()

Adds the empty clause to the Cnf

     

void print() const

     

std::string picosat() const

String representing the Cnf in Picosat format

     

void clear()

CnfConverter

     

static Cnf tseitin(Formula const & boolFunc)

Generates a cnf equisatisfiable with the boolfunc using the tesitin transformation

  • boolFunc : a Formula

Returns a Cnf equisatisfiable with the boolFunc

     

static Cnf convertToCnf(const BDD & bdd)

Converts the BDD into a CNF

  • bdd : a BDD

Returns a Cnf equisatisfiable with the bdd

GeneralTimeoutSolver

     

GeneralTimeoutSolver(int seconds, SearchStrategy *p_searchStrategy, const PBMin & p_pbmin)

Creates an object

  • seconds : maximum timeout
  • p_searchStrategy : search strategy used to find the minimum value for the cost function
  • p_pbmin : problem to be solved

     

virtual bool run(std::vector< int32_t > & model, int64_t & min) override

Solves the problem

  • model : vector where the model will be stored
  • min : int where the minimum value for the cost function will be stored

Retruns true if the problem is satisfiable. False otherwise

LinearSearchStrategy

     

LinearSearchStrategy()

     

void init(const PBMin & p) override

Initializes the algorithm. Must be called before loop and end.

  • problem : a PBMin problem which defines the problem to be solved

     

void loop(void (Solver::*solve)(std::vector< int32_t > &, const std::vector< std::vector< int32_t > > &, bool &),std::vector< int32_t > & model, int64_t & min, bool &sat, Solver *solver, const PBMin & problem)override

This function executes the linear search algorithm. Must be executed between init and end.

  • solve : function which takes 3 arguments (model, cnf, sat) and solves the given cnf storing the assignment in model and storing in sat its satisfiability
  • model : a structure where model will be stored
  • min : a int64_t where the minimum value for the cost function will be stored
  • sat : a boolean where the satisfiability of the problem will be stored
  • solver : the solver used to solve this problem
  • problem : the problem to be solved

     

void end() override

Finishes the execution of this class, in this implementation it does nothing. Must be called after loop.

MixCNFConverter

     

Cnf getResult()

Must be called after convert. Returns equisatisfiable CNF.

     

void clear()

Clears the class variables.

     

void convert(Formula const & f)

Converts the given Boolean formula to a CNF which can be get with getResult. The method applies different methods depending on the formula characteristics.

  • f : Formula to be converted

     

void setValueCover(int i)

If the number of minterms of the function is LEQ than i/10000 the function will be converted using a different method

  • i : between 0 and 10000

     

bool worthToConvert(BDD const & bdd)
  • bdd : A BDD Return true if the bdd's primes cover enough 1's.

PBConstraint

     

PBConstraint(const PBFormula & formula, int64_t k)

Constructs a pseudo-Boolean constraint of the type formula <= k

  • formula
  • k

     

PBFormula getPBFormula() const

     

int64_t getK()

     

void encode(std::vector< std::vector< int32_t > > & cnf, int32_t & firstFreshVariable)

Encodes the PBConstraint to a cnf

  • cnf : where the encoding will be stored
  • firstFreshVariable : needed for PBLib, has to be greater than the last id used

     

void setK(int64_t p_k)

PBFormula

     

PBFormula(const std::vector< int64_t > & weights, const std::vector< int32_t > & literals)

Constructs a pseudo-Boolean formula of the type weights[0]literals[0] + ... + weights[n-1]literals[n-1]

  • weights
  • literals

     

std::vector< int64_t > getWeights() const

     

std::vector< int32_t > getLiterals() const

     

void addPair(int64_t weight, int32_t literal)

PBMin

     

PBMin(std::vector<PBConstraint> p_constraints, PBFormula p_costFunction)

Constructs a pseudo-Boolean minimization problem with

  • p_constraints
  • p_costFunction

     

std::vector<PBConstraint> getConstraints() const

     

PBFormula getCostFunction() const

     

int32_t getFirstFreshVariable() const

Returns the biggest literal+1

     

int64_t getCostFunctionMax() const

Returns the maximum possible value of the cost function

     

int64_t getCostFunctionMin() const

Returns the minimum possible value of the cost function

SatSolver

     

static void solve(Cnf cnf)

Calls the command picosat with the cnf as input

  • cnf : The CNF to be solved

     

static std::string solve2(Cnf cnf)

Calls the command picosat with the cnf as input and returns the result.

  • cnf : The CNF to be solved Returns the output from picosat.

SearchStrategy

     

virtual void init(const PBMin & problem) = 0

This function should be the first one called

  • problem : The problem to be solved

     

virtual void loop(void (Solver::*solve)(std::vector< int32_t > &, const std::vector< std::vector< int32_t > > &, bool &),std::vector< int32_t > & model, int64_t & min, bool &sat, Solver *solver, const PBMin &problem) = 0

This function should be called after init

  • solve : Function from the Solver class which solves a cnf
  • model : Place where the model will be stored
  • min : Place where the minimum value for the cost function will be stored
  • sat : Boolean where the satisfiability of the problem will be stored
  • solver
  • problem

     

virtual void end() = 0

This function should be called after loop

SimpleTimeoutSolver

     

SimpleTimeoutSolver(int seconds, SearchStrategy *p_searchStrategy, const PBMin & p_pbmin)

Constructs a Solver with a timeout for each call at the sat solver

  • seconds : timeout. The minimum value is 1
  • p_searchStrategy : the SearchStrategy used for finding the minimum value for the cost function
  • p_pbmin : the pseudo-Boolean minimization problem

     

virtual void solver(std::vector< int32_t > & model, const std::vector< std::vector< int32_t > > & cnf, bool & sat) override

Function called by the SearchStrategy to solve the CNF

  • model : where the model will be stored
  • cnf : the cnf of the problem
  • sat : where the satisfiability of the problem will be stored

Solver

     

Solver(SearchStrategy *p_searchStrategy, const PBMin & p_pbmin)

Constructs a Solver

  • p_searchStrategy : the SearchStrategy used for finding the minimum value for the cost function
  • p_pbmin : the pseudo-Boolean minimization problem

     

virtual bool run(std::vector< int32_t > & model, int64_t & min)

Function called by the user to start the problem solving

  • model : where the model will be stored
  • min : where the minimum value for the cost function will be stored Return true if satisfiable, otherwise false

     

virtual void solver(std::vector< int32_t > & model, const std::vector< std::vector< int32_t > > & cnf, bool & sat)

Function called by the SearchStrategy which calls a SAT solver (minisat)

  • model : where the model will be stored
  • cnf : the CNF for the SAT Solver
  • sat : where the satisfiability of the CNF will be stored

     

virtual bool hasTimeoutOccurred()

If the timeout has occurred, the solution may not be optimal. Returns true if the timeout has occurred, false otherwise.

VarsManager

     

static VarsManager* getInstance()

This class follows the singleton pattern. There must be only one instance of this class. Returns the current existing instance or creates a new one.

     

int newId(const std::string & name  = "")

Given a variable name, returns the integer representing it. If the name already exists it returns the same integer. If no name is provided a new id is returned and the name is not stored. (This is used for variables created by transformation like Tseitin)

  • name : A string assoiated with the variable Returns an integer used for representing the variable.

     

void freeId(int id)

The integer representing a variable is released It will be added to a recyclable queue where the variables will be assigned again when newId is called.

  • id

     

int getLastId()

     

void setLastId(int n)

     

void storeCuddWithId(int cudd, int id)

Relates the two ids

  • cudd : the id from Cudd library
  • id : the id from this library

     

int getIdFromCudd(int cudd)

Given the Cudd id returns the id from this library

  • cudd : the id from Cudd library Returns an id from this library

     

int getCuddFromId(int id)

Given the id from this library returns the Cudd id

  • id : id from this library Return the id from Cudd library

     

BDD bddVar()

To get a new BDD var from the Cudd library Returns a BDD var

     

BDD bddVar(int i)

To get a new BDD var from the Cudd library identified by i

  • i Returns a BDD var identified by i

     

DdManager* getCuddMgr()

Returns a pointer to DdManager from the Cudd library

     

int getNumIds()

     

void clearInstance()

Deletes all the information stored in the class

⚠️ **GitHub.com Fallback** ⚠️