Satex Black Box

The Satex BlackBox module provide utilities to run solvers from the SAT solver competitions with SAT Heritage and then parse the result.

class optilog.blackbox.SatexBlackBox(solver, constraints=None)
Parameters

  • solver (str) – Name of the solver to insantiate. See the method available_solvers

  • constraints (Optional[ExecutionConstraints]) – Defines the execution constraints for the Configuration Process

static available_solvers(pattern=None)

SatexBlackBox accesses the SAT solvers used by satex This method returns a list of available solvers that match the given pattern.

Parameters

pattern (Optional[str]) – Pattern for available solvers

Return type

List[str]

Returns

List of strings with the names of available solvers

>>> from optilog.blackbox import SatexBlackBox
>>>
>>> SatexBlackBox.available_solvers('kissat*')
['kissat-sc2020-default:2020', 'kissat-sc2020-sat:2020', 'kissat-sc2020-unsat:2020',
'kissat-mab:2021', 'kissat-sat_crvr_gb:2021', 'kissat-sc2021:2021', 'kissat_bonus:2021',
'kissat_cf:2021', 'kissat_gb:2021']
property is_sat: bool

Whether the solver has determined the instance is satisfiable or not. Accessible after the execution has finished.

property sat: str

Result of the status line of the solver. Accessible after the execution has finished.

property model: List[int]

Parsed model as list of integers of the instance Accessible after the execution has finished.

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.

classmethod get_config()
Return type

Dict[str, Dict[str, str]]

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.

property parsed

Dictionary with all the parsed elements from the execution. Accessible after the execution has finished.

set(key, value, check_domain=True)

Sets the value for a given parameter.

Parameters

  • key (str) – Parameter name.

  • value – Parameter value.

  • value – int or float or bool or str

Raises

KeyError: if param is not found inside the blackbox.

classmethod set_default(value, check_domain=True)

Sets the value for a given parameter in the default configuration

Parameters

  • key (str) – Parameter name.

  • value – Parameter value.

  • value – int or float or bool or str

Raises

KeyError: if param is not found inside the blackbox.

run(instance, constraints=None, stdout=BlackBoxRedirection.Default, stderr=BlackBoxRedirection.Stdout)

Executes the SAT solver and stores the output out of the call

Note that this call will launch a docker container and may pull a docker image. Startup may not be instantaneous.

Parameters

  • instance (Union[str, CNF]) – Path to the CNF instance to execute. It may also be a CNF object, in which case it will be written to a memory file without going through disk. Note that this might would result in faster loading times but higher memory consumption.

  • constraints (Optional[ExecutionConstraints]) – Defines the execution constraints for the Configuration Process. If it is None, the default constraints of the constructor will be used. Otherwise, these new constraints will be used.

  • stdout (Union[str, BlackBoxRedirection]) – Where to redirect stdout. If it is a string, the output will be redirected to the specified path.

  • stderr (Union[str, BlackBoxRedirection]) – Where to redirect stderr. If it is a string, the output will be redirected to the specified path.

First of all we will check out the available kissat solvers:

1>>> from optilog.blackbox import SatexBlackBox
2>>>
3>>> print(SatexBlackBox.available_solvers('kissat*'))
4['kissat-sc2020-default:2020', 'kissat-sc2020-sat:2020', 'kissat-sc2020-unsat:2020',
5'kissat-mab:2021', 'kissat-sat_crvr_gb:2021', 'kissat-sc2021:2021', 'kissat_bonus:2021',
6'kissat_cf:2021', 'kissat_gb:2021']

Then, we can create a new SAT solver and solve a CNF instance:

 1>>> from optilog.blackbox import SatexBlackBox, ExecutionConstraints, DockerEnforcer
 2>>>
 3>>> bb = SatexBlackBox(
 4>>>     'kissat-mab:2021',
 5>>>     constraints=ExecutionConstraints(
 6>>>          h_wall_time=100,
 7>>>          h_real_memory='100M',
 8>>>          enforcer=DockerEnforcer()
 9>>>     ))
10>>>
11>>> bb.run('/path/to/instance')
12>>>
13>>> print(bb.sat)
14SATISFIABLE
15>>> print(bb.is_sat)
16True
17>>> print(bb.model)
18[1, 2, 3, 4, ..., 99, -100]

We can do the exact same thing with a CNF formula:

 1>>> from optilog.blackbox import SatexBlackBox
 2>>> from optilog.formulas import CNF
 3>>> c = CNF()
 4>>> c.add_clause([1, 2, 3])
 5>>> c.add_clause([-1])
 6>>> c.add_clause([-3])
 7>>>
 8>>>
 9>>> bb = SatexBlackBox('kissat-mab:2021')
10>>>
11>>> bb.run(c)
12>>>
13>>> print(bb.sat)
14SATISFIABLE
15>>> print(bb.is_sat)
16True
17>>> print(bb.model)
18[-1, 2, -3]