iSAT Interface

In order to connect another solver to the module you have to implement the iSAT interface. iSAT is a proposed standard interface for SAT solvers, covering their most important methods.

The main objective of this interface is to provide SAT solvers developers a quick and easy way of connecting their work to the Python environment. Since solver developers mainly work with C/C++, this interface is in C++.

This interface contains a significant set of methods, but not all must be implemented. Some of the methods may not be implementable by particular SAT solver. A method not implemented will throw a NotImplementedException by default. It is up to the developer to choose what methods they need to implement.

iSAT class

class iSAT

Public Functions

virtual int newVar()

Creates a new variable and returns its DIMACS id.

Returns

The returned value will be iSAT.getMaxVar() + 1.

virtual bool addClause(const std::vector<int> &literals)

Adds a new clause to this solver.

Parameters

literals – The clause to be added to the solver.

Returns

Wether or not the clause has been added to the solver. The clause may not be added for multiple reasons (may be repeated, redundant, etc.).

virtual unsigned int getMaxVar()

Returns

Returns the maximum DIMACS variable id in the solver.

virtual unsigned int getNumClauses()

Returns

Returns the number of clauses within the solver.

virtual void setConflictsBudget(long long budget)

Sets the maximum number of conflicts allowed by the budget, used by the methods solveLimited or solveHardLimited. A solve call will reset all budgets. A call with budget 0 or 1 will reset the configuration budget. The configuration budget is kept in between calls to solveLimited or solveHardLimited and is not automatically reset. Meaning that if you want to run your each solve_limited call with a limit of 1000, you will have to manually reapply the budget in between calls.

Parameters

budget – the budget for the number of conflicts.

virtual void setPropagationBudget(long long budget)

Sets the maximum number of propagations allowed by the budget, used by the methods solveLimited or solveHardLimited. A solve call will reset all budgets. A call with budget 0 or 1 will reset the configuration budget. The configuration budget is kept in between calls to solveLimited or solveHardLimited and is not automatically reset. Meaning that if you want to run your each solve_limited call with a limit of 1000, you will have to manually reapply the budget in between calls.

Parameters

budget – the budget for the number of propagations.

virtual E_STATE solve(const std::vector<int> &assumptions)

Parameters

assumptions – Vector of assumptions.

Returns

Returns SAT if all variables are assigned and no contradiction is found. Returns UNSAT, if the formula is proven to be unsatisfiable. Otherwise, returns UNKNOWN if all decision variables are assigned and no contradiction is found.

virtual bool propagate(const std::vector<int> &assumptions, std::vector<int> &propagated)

Applies unit propagation with an optional vector of assumptions.

Parameters

• assumptions – The vector of assumptions.

• propagated – The vector used to store the propagations

Returns

Returns SAT if the solver finds no contradiction, and the vector of assigned literals. Returns UNSAT if the solver finds a contradiction and an empty vector.

virtual void core(std::vector<int> &conflict)

If the solver returns False, computes a subset of the assumptions that form a core of unsatisfiability. Otherwise must return an empty vector or an exception.

Parameters

conflict – Vector used to store the core

virtual void getModel(std::vector<int> &model)

Returns

Returns a model for the decision variables that satisfies the formula.

virtual E_STATE solveLimit(const std::vector<int> &assumptions)

Stops the solving process if the budget is already exhausted at the beginning of the next restart.

If no budget has been set, this call is equivalent to the solve method.

Parameters

assumptions – Vector of assumptions.

Returns

Returns the same as method solve and additionally returns UNKNOWN if the budget is exhausted.

virtual void setIncremental()

Enables the incremental mode in solvers of the Glucose family. This mode enables changes in the LBD heuristic that may help improve performance in incremental sat solving. For more details see “Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction”.

virtual E_STATE getPolarity(int var)

Returns the preferred value for the given variable when the solver makes a decision. This value may be updated during the resolution process by phase saving policies. The default preferred value depends on the solver implementation.

Parameters

var – The variable id

Returns

The preferred polarity value for a variable

virtual void unsetVarPolarity(int var)

Disables the polarity set by the method setPolarity.

Parameters

var – The variable id

virtual void setVarPolarity(int var, bool polarity)

Forces the solver to set the given polarity when deciding the variable.

virtual void traceProof(const char *path)

Dumps the proof of the resolution process to the specified path. This method must be called before executing any of the solve like methods. If this method is called after any solve like call an exception will arise.

Warning: Solver interfaces are not homogeneous so this specification may not be entirely suitable.

Parameters

path – The file path where the proof is going to be written.

virtual void interrupt()

Interrupts the resolution process. This interruption will happen at the beginning of the next restart.

virtual void clearInterrupt()

Clears an interruption. The interruption must be cleared before calling solve like methods. Not all the solvers force to clear the interruptions.

virtual E_STATE getValue(int variable)

Parameters

variable – The variable id.

Returns

Returns the value assigned to the given variable. If the variable is unassigned, returns UNKNOWN (meaning undefined).

virtual void setDecisionVariable(int var, bool b)

Parameters

• var – The variable to be set as decision variable.

• dec – If dec is True, sets the variable as a decision variable. If dec is False the variable is not a decision variable. By default all variables are decision variables.

virtual bool isFullModel()

Returns

Returns True if model assigns all the variables.

virtual long getNumConflicts()

Clears an interruption. The interruption must be cleared before calling solve like methods. Not all the solvers force to clear the interruptions.

virtual void getLearntClauses(std::vector<std::vector<int>> &learntClauses)

Returns

Returns the vector of learnt clauses. Only clauses of size > 1 are guaranteed.

virtual void getTrail(int level, std::vector<int> &trail)

Obtain the literals of the solver’s trail on the specified decision level.

Parameters

• level – Trail level

• trail – Output trail

virtual void getUnits(std::vector<int> &units)

Obtain all the literals in unit clauses (in original and learnt clauses).

Parameters

units – Output literals

virtual E_STATE solveHardLimited(const std::vector<int> &assumptions)

Stops the solving process if the budget is already exhausted.

If no budget has been set, this call is equivalent to the solve method.

Parameters

assumptions – Vector of assumptions.

Returns

Returns the same as method solve and additionally returns UNKNOWN if the budget is exhausted.

virtual void setStaticHeuristic(std::vector<int> *heuristic)

Sets an static heuristic. The heuristic is described as a vector of pairs of variables and values.

If all the variables in the heuristic have been decided, the solver applies the regular procedure.

If an heuristic is active then its polarities take precedence over the ones assigned by the method setPolarity.

Warning: Notice the vector is passed by reference and becomes the callee responsibility to deallocate when a new heuristic is set. The vector is allocated with the keyword new, therefore it has to be deallocated with the keyword delete.

Parameters

heuristic – A list of literals.

virtual void enableStaticHeuristic(bool enable)

Parameters

enable – Enables or disables the static heuristic set by method setStaticHeuristic

virtual void getActivities(std::vector<double> &activities)

Parameters

activities – Vector to store the activities of the variables in order

virtual iSAT *clone()

Clones the solver, including the loaded clauses and internal state

Parameters

solver – Solver to clone

virtual bool unsatState()

Returns

Returns True if the solver is in an unsat state. An unsat state means that the current formula is unsatisfiable.

virtual void set(const char *key, int value)

Sets the value for a given parameter.

Parameters

• key – Parameter name.

• value – Parameter value.

virtual void set(const char *key, double value)

Sets the value for a given parameter.

Parameters

• key – Parameter name.

• value – Parameter value.

virtual void set(const char *key, bool value)

Sets the value for a given parameter.

Parameters

• key – Parameter name.

• value – Parameter value.

virtual void set(const char *key, char *value)

Sets the value for a given parameter.

Parameters

• key – Parameter name.

• value – Parameter value.

virtual void get(const char *key, Parameter &value)

Sets the value for a given parameter.

Parameters

• key – Parameter name.

• value – Parameter value used to the return value.

virtual int getVersion()

Returns the version of the interface. This number describes information of the available methods

Note

Ctrl+C signals (SIGINT) are captured and handled by OptiLog in the main thread. If that happens while executing a SAT solver, OptiLog will stop the current execution context and raise a Python Exception. No further methods will be called on the SAT solver after that point.

Solver states and Variables values

enum E_STATE

Values:

enumerator UNSAT

enumerator SAT

enumerator UNKNOWN