SAT Solver
The SAT Solver module provides a bridge to access, in a standard way, multiple solver oracles from Python.
The actual set of solvers written in C/C++ for which a wrapper is already provided are:
Integrated SAT solvers
To bring new solvers to the toolkit, please look at the Solver Developer page for instructions.
- class optilog.solvers.sat.pyisat.PyiSAT(**config)
PyiSAT is a standard interface to access incremental SAT solver oracles from Python.
Not every solver implements every method of the interface. If a method is not implemented, it will throw a NotImplementedError.
Instantiates a new SAT solver. Each parameter passed as a keyword argument will be configured on the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41(seed=1.0) >>> solver.get('seed') 1.0
- new_var()
Creates a new variable and returns its DIMACS id. The returned value will be PyiSAT.max_var() + 1.
- Return type
int
- Returns
The created variable.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.new_var() 1 >>> solver.new_var() 2
- add_clause(clause)
Adds a new clause to this solver.
- Parameters
clause (
List
[int
]) – The clause to be added to the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clause([1,2,3])
- load_cnf(path, return_complete=False)
This method can be used to load CNF formulas directly into the solver.
By default, nothing is returned. If you would like the parsed formula to be returned, pass the argument return_complete=True
- Parameters
path (
str
) – Path to the cnf filereturn_complete (bool) – If true, returns loads the formula into the solver and returns it
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.load_cnf('./path/to/file')
- Return type
- load_wcnf(path, return_complete=False)
This method can be used to load the HARD clauses of the formulas directly into the solver.
By default, only the SOFT clauses of the formula are returned. This is implemented for performance reasons, as many formulas contain a very large set of hard clauses but small set of soft ones. If you would like the entire formula to be returned, pass the argument return_complete=True
- Parameters
path (
str
) – Path to the wcnf filereturn_complete (
bool
) – If false, a formula with only the soft clauses are returned. If true, returns the complete formula.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.load_wcnf('./path/to/file')
- Return type
- add_clauses(clauses)
Adds a set of clauses to this solver.
- Parameters
clauses (
List
[List
[int
]]) – The set of clauses to be added to the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]])
- max_var()
- Return type
int
- Returns
The maximum DIMACS variable id in the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> solver.max_var() 3
- num_clauses()
- Return type
int
- Returns
Returns the number of clauses within the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> solver.num_clauses() 4
Warning
The number of clauses in the solver may not correspond with the number of clauses inserted into the solver. The solver may freely discard redundant clauses or not take into account the number of unitary clauses, among other considerations. The exact behavior is solver dependent.
- set_conf_budget(budget)
Sets the maximum number of conflicts allowed by the budget, used by the methods
solve_limited()
orsolve_hard_limited()
. Asolve()
call will reset all budgets. :type budget:int
:param budget: The budget for the number of conflicts.>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.set_conf_budget(100)
- set_prop_budget(budget)
Sets the maximum number of propagations allowed by the budget, used by the methods
solve_limited()
orsolve_hard_limited()
. Asolve()
call will reset all budgets.- Parameters
budget (
int
) – the budget for the number of propagations.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.set_prop_budget(5000)
- solve(assumptions=None)
Solves the formula with an optional list of assumptions (list of literals that are forced to be true).
- Parameters
assumptions (
Optional
[List
[int
]]) – List of assumptions.- Return type
Optional
[bool
]- Returns
Returns True if all variables are assigned and no contradiction is found. Returns False, if the formula is proven to be unsatisfiable. Otherwise, returns None if all decision variables are assigned and no contradiction is found.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> solver.solve([-1]) True >>> solver.solve([1, 3]) False >>> solver.add_clause([4, 5]) >>> solver.set_decision_var(4, False) >>> solver.set_decision_var(5, False) >>> solver.solve() None >>> solver.model() [-1, 2, -3]
- solve_limited(assumptions=None)
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 (
Optional
[List
[int
]]) – List of assumptions.- Return type
Optional
[bool
]- Returns
Returns the same as method
solve()
and additionally returns None if the budget is exhausted.
- solve_hard_limited(assumptions=None)
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 (
Optional
[List
[int
]]) – List of assumptions.- Return type
Optional
[bool
]- Returns
Returns the same as method
solve()
and additionally returns None if the budget is exhausted.
- propagate(assumptions=None)
Applies unit propagation with an optional list of assumptions.
- Parameters
assumptions (
Optional
[List
[int
]]) – The list of assumptions.- Return type
Tuple
[bool
,List
[int
]]- Returns
Returns True if the solver finds no contradiction, and the list of assigned literals. Returns False if the solver finds a contradiction and an empty list.
- model()
- Return type
List
[int
]- Returns
Returns a model for the decision variables that satisfies the formula.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> solver.solve([-1]) >>> solver.model() [-1, 2, -3]
- is_full_model()
- Return type
bool
- Returns
True if model assigns all the variables. False otherwise.
- core()
If the solver returns False, computes a subset of the assumptions that form a core of unsatisfiability.
- Return type
List
[int
]- Returns
A core of unsatisfiability.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3], [-1,-2], [-1,-3], [-2,-3]]) >>> solver.solve([1,2,3]) False >>> solver.core() [2, 1]
- get_polarity(variable)
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
variable (
int
) – The variable id.- Return type
bool
- Returns
The preferred polarity value for a variable.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> solver.get_polarity(1) False
- set_polarity(variable, polarity)
Forces the solver to set the given polarity when deciding the variable.
- Parameters
variable (
int
) – The variable id.polarity (
bool
) – The preferred value for the variable.
- unset_polarity(variable)
Disables the polarity set by the method
set_polarity()
.- Parameters
variable (
int
) – The variable id.
- value(variable)
- Parameters
variable (
int
) – The variable id.- Return type
Optional
[bool
]- Returns
Returns the value assigned to the given variable. If the variable is unassigned, returns None (meaning undefined).
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]]) >>> v = solver.value(1) >>> print(v) None >>> solver.solve() True >>> solver.model() [-1, 2, -3] >>> solver.value(1), solver.value(2), solver.value(3) (False, True, False)
- interrupt()
Interrupts the resolution process. This interruption will happen at the beginning of the next restart.
- clear_interrupt()
Clears an interruption. The interruption must be cleared before calling
solve
like methods. Not all the solvers force to clear the interruptions.
- num_conflicts()
- Return type
int
- Returns
Returns the number of conflicts detected during the solving process.
- set_decision_var(variable, dec=False)
- Parameters
variable (
int
) – The variable to be set as decision variable.dec (
bool
) – If dec is True, sets the variable as a decision variable. If dec is False the variable is not a decision variable. In a new solver, by default all variables are decision variables.
- trace_proof(file_path)
Dumps the proof of the resolution process ot the specified file_path. This method must be called before executing any of the
solve
like methods. If this method is called after anysolve
like call an exception will arise.- Parameters
file_path (str) – The file path where the proof is going to be written.
Warning
Solver interfaces are not homogeneous so this specification may not be entirely suitable.
- learnt_clauses()
- Return type
List
[List
[int
]]- Returns
Returns the list of learnt clauses, including the learnt unit clauses.
- set_static_heuristic(heuristic)
Sets an static heuristic. The heuristic is described as a list 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
set_polarity()
.- Parameters
heuristic (
List
[int
]) – A list of literals.
- enable_static_heuristic(enable=True)
- Parameters
enable (
bool
) – Enables or disables the static heuristic set by methodset_static_heuristic()
- set_incremental()
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”.
- clone()
Creates a clone of the PyiSAT solver. The new solver will have all the same internal state as the original solver.
- Return type
- static get_config()
- Return type
Dict
[str
,Dict
]- Returns
Returns a dictionary with all the configurable parameters of the solver. Each parameter has defined its type (int, float, bool or categorical), its domain and its default value.
>>> from optilog.solvers.sat import Glucose41 >>> config = Glucose41.get_config() >>> config { 'params': { 'gc-frac': { 'type': 'real' 'domain': [0.001, 3.4e+38], 'default': 0.2, }, 'rinc': { 'type': 'integer' 'domain': [2, 2147483647], 'default': 2, }, 'rnd-init': { 'type': 'bool' 'domain': [True, False], 'default': False, } ........ } }
- set(key, value)
Sets the value for a given parameter.
- Parameters
key (
str
) – Parameter name.value (int or float or bool or str) – Parameter value.
- Raises
KeyError: if
param
is not found inside the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.set('seed', 1.0)
- get(key)
Returns the value assigned to a given parameter name.
- Parameters
key (
str
) – Parameter name.- Return type
Union
[int
,float
,bool
,str
]- Returns
Parameter value.
- Raises
KeyError: if
param
is not found inside the solver.
>>> from optilog.solvers.sat import Glucose41 >>> solver = Glucose41() >>> solver.set('seed', 1.0) >>> solver.get('seed') 1.0