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 file

  • return_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

CNF

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 file

  • return_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

WCNF

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() or solve_hard_limited(). A solve() 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() or solve_hard_limited(). A solve() 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 any solve 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 method set_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

PyiSAT

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