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
or1
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
or1
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. ReturnsUNSAT
, if the formula is proven to be unsatisfiable. Otherwise, returnsUNKNOWN
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. ReturnsUNSAT
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 theGlucose
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 thesolve
like methods. If this method is called after anysolve
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 keyworddelete
. 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

virtual int newVar()
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.