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

Minisat 2.2.0

Glucose 3.0

Glucose 4.1

Lingeling 2018

Cadical 1.0.3

Cadical 1.5.2

PicoSAT 965

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 (Union[str, Path]) – Path to the cnf file
return_complete (bool) – If true, returns loads the formula into the solver and returns it

Return type

CNF

>>> from optilog.solvers.sat import Glucose41
>>> solver = Glucose41()
>>> solver.load_cnf('./path/to/file')

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 (Union[str, Path]) – 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.

Return type

WCNF

>>> from optilog.solvers.sat import Glucose41
>>> solver = Glucose41()
>>> solver.load_wcnf('./path/to/file')

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. A call with budget 0 or 1 will reset the configuration budget. The configuration budget is kept in between calls to solve_limited() or solve_hard_limited() 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 (int) – 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. A call with budget 0 or 1 will reset the configuration budget. The configuration budget is kept in between calls to solve_limited() or solve_hard_limited() 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 (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, remove_assumptions=True)

Applies unit propagation with an optional list of assumptions.

Parameters

assumptions (Optional[List[int]]) – The list of assumptions.
remove_assumptions (bool) – If True, the assumptions are removed from the list of propagated literals.

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. Only clauses of size > 1 are guaranteed.

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. :rtype: PyiSAT :return: Cloned solver

get_trail(level)

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

Parameters: level (int) – Trail level
Return type: List[int]
Returns: Solver’s trail

unsat_state()

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

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