minisolvers.py

A Python API for the MiniSat and MiniCard constraint solvers.

Classes:

MinisatSolver

Solve CNF instances using MiniSat.

MinicardSolver

Solve CNF+ (CNF plus cardinality constraints) using MiniCard.

MinisatSubsetSolver

Solve arbitrary subsets of CNF instances and find SAT subsets / UNSAT cores.

MinicardSubsetSolver

Solve arbitrary subsets of CNF+ instances and find SAT subsets / UNSAT cores.

Solver

An abstract base class for the other classes.

SubsetMixin

A mixin class adding ‘subset’ functionality to Solver subclasses.

Source code is hosted on GitHub: https://github.com/liffiton/PyMiniSolvers/

class minisolvers.MinisatSolver

Bases: minisolvers.Solver

A Python analog to MiniSat’s Solver class.

>>> S = MinisatSolver()

Create variables using new_var(). Add clauses as sequences of literals with add_clause(), analogous to MiniSat’s addClause(). Literals are specified as integers, with the magnitude indicating the variable index (with 1-based counting) and the sign indicating True/False. For example, to add clauses (x0), (!x1), (!x0 + x1 + !x2), and (x2 + x3):

>>> for i in range(4):
...     S.new_var()  # doctest: +ELLIPSIS
0
1
2
3
>>> for clause in [1], [-2], [-1, 2, -3], [3, 4]:
...     S.add_clause(clause)  # doctest: +ELLIPSIS
True
True
True
True

The solve() method returns True or False just like MiniSat’s.

>>> S.solve()
True

Models are returned as arrays of Booleans, indexed by var. So the following represents x0=True, x1=False, x2=False, x3=True.

>>> list(S.get_model())
[1, 0, 0, 1]

The add_clause() method may return False if a conflict is detected when adding the clause, even without search.

>>> S.add_clause([-4])
False
>>> S.solve()
False

add_clause(lits)

Add a clause to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is (!x0 + x1 + !x2)

Returns:

A boolean value returned from MiniSat’s addClause() function, indicating success (True) or conflict (False).

block_model()

Block the current model from the solver.

check_complete(positive_lits=None, negative_lits=None)

Check whether a given complete assignment satisfies the current set of clauses. For efficiency, it may be given just the positive literals or just the negative literals.

Args:

positive_lits, negative_lits:

Optional sequences (exactly one must be specified) containing literals as integers, specified as in add_clause(). If positive literals are given, the assignment will be completed assuming all other variables are negative, and vice-versa if negative literals are given.

Returns:

True if the assignment satisfies the current clauses, False otherwise.

get_model(start=0, end=-1)

Get the current model from the solver, optionally retrieving only a slice.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

Returns:

An array of booleans indexed to each variable (from 0). If a start index was given, the returned list starts at that index (i.e., get_model(10)[0] is index 10 from the solver’s model.

get_model_trues(start=0, end=-1, offset=0)

Get variables assigned true in the current model from the solver.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

offset (int):

Optional offset to be added to the zero-based variable numbers from MiniSat.

Returns:

An array of true variables in the solver’s current model. If a start index was given, the variables are indexed from that value.

get_stats()

Returns a dictionary of solver statistics.

implies(assumptions=None)

Get literals known to be implied by the current formula. (I.e., all assignments made at level 0.)

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

An array of literals implied by the current formula (and optionally the given assumptions).

model_value(i)

Get the value of a given variable in the current model.

nclauses()

Get the number of clauses or constraints added to the solver.

new_var(polarity=None, dvar=True)

Create a new variable in the solver.

Args:

polarity (bool):

The default polarity for this variable. True = variable’s default is True, etc. Note that this is the reverse of the ‘user polarity’ in MiniSat, where True indicates the sign is True. The default, None, creates the variable using Minisat’s default, which assigns a variable False at first, but then may change that based on the phase-saving setting.

dvar (bool):

Whether this variable will be used as a decision variable.

Returns:

The new variable’s index (0-based counting).

nvars()

Get the number of variables created in the solver.

set_phase_saving(ps)

Set the level of phase saving (0=none, 1=limited, 2=full (default)).

set_rnd_init_act(val)

Set whether variables are intialized with a random initial activity. (default: False)

set_rnd_pol(val)

Set whether random polarities are used for decisions (overridden if vars are created with a user polarity other than None)

set_rnd_seed(seed)

Set the solver’s random seed to the given double value. Cannot be 0.0.

simplify()

Call Solver.simplify().

solve(assumptions=None)

Solve the current set of clauses, optionally with a set of assumptions.

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

True if the clauses (and assumptions) are satisfiable, False otherwise.

class minisolvers.MinicardSolver

Bases: minisolvers.Solver

A Python analog to MiniCard’s Solver class.

>>> S = MinicardSolver()

This has the same interface as MinisatSolver, with the addition of the add_atmost() and add_atleast() methods.

>>> for i in range(4):
...     S.new_var()  # doctest: +ELLIPSIS
0
1
2
3
>>> for clause in [1], [-2], [3, 4]:
...    S.add_clause(clause)
True
True
True

To add an AtMost constraint, specify the set of literals and the bound. For example, to add AtMost({x0, !x1, x2}, 2):

>>> S.add_atmost([1,-2,3], 2)
True

>>> S.solve()
True

>>> list(S.get_model())
[1, 0, 0, 1]

>>> S.add_atleast([1,2,3,4], 2)
True

>>> S.solve()
True

As with add_clause(), the add_atmost() method may return False if a conflict is detected when adding the constraint, even without search.

>>> S.add_atmost([1,-3,4], 2)
False
>>> S.solve()
False

add_atmost(lits, k)

Add an AtMost constraint to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is {!x0, x1, !x2}

k (int):

The [upper] bound to place on these literals.

Returns:

A boolean value returned from MiniCard’s addAtMost() function, indicating success (True) or conflict (False).

add_atleast(lits, k)

Convenience function to add an AtLeast constraint. Translates the AtLeast into an equivalent AtMost. See add_atmost().

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is {!x0, x1, !x2}

k (int):

The [lower] bound to place on these literals.

Returns:

A boolean value returned from MiniCard’s addAtMost() function, indicating success (True) or conflict (False).

add_clause(lits)

Add a clause to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is (!x0 + x1 + !x2)

Returns:

A boolean value returned from MiniSat’s addClause() function, indicating success (True) or conflict (False).

block_model()

Block the current model from the solver.

check_complete(positive_lits=None, negative_lits=None)

Check whether a given complete assignment satisfies the current set of clauses. For efficiency, it may be given just the positive literals or just the negative literals.

Args:

positive_lits, negative_lits:

Optional sequences (exactly one must be specified) containing literals as integers, specified as in add_clause(). If positive literals are given, the assignment will be completed assuming all other variables are negative, and vice-versa if negative literals are given.

Returns:

True if the assignment satisfies the current clauses, False otherwise.

get_model(start=0, end=-1)

Get the current model from the solver, optionally retrieving only a slice.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

Returns:

An array of booleans indexed to each variable (from 0). If a start index was given, the returned list starts at that index (i.e., get_model(10)[0] is index 10 from the solver’s model.

get_model_trues(start=0, end=-1, offset=0)

Get variables assigned true in the current model from the solver.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

offset (int):

Optional offset to be added to the zero-based variable numbers from MiniSat.

Returns:

An array of true variables in the solver’s current model. If a start index was given, the variables are indexed from that value.

get_stats()

Returns a dictionary of solver statistics.

implies(assumptions=None)

Get literals known to be implied by the current formula. (I.e., all assignments made at level 0.)

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

An array of literals implied by the current formula (and optionally the given assumptions).

model_value(i)

Get the value of a given variable in the current model.

nclauses()

Get the number of clauses or constraints added to the solver.

new_var(polarity=None, dvar=True)

Create a new variable in the solver.

Args:

polarity (bool):

The default polarity for this variable. True = variable’s default is True, etc. Note that this is the reverse of the ‘user polarity’ in MiniSat, where True indicates the sign is True. The default, None, creates the variable using Minisat’s default, which assigns a variable False at first, but then may change that based on the phase-saving setting.

dvar (bool):

Whether this variable will be used as a decision variable.

Returns:

The new variable’s index (0-based counting).

nvars()

Get the number of variables created in the solver.

set_phase_saving(ps)

Set the level of phase saving (0=none, 1=limited, 2=full (default)).

set_rnd_init_act(val)

Set whether variables are intialized with a random initial activity. (default: False)

set_rnd_pol(val)

Set whether random polarities are used for decisions (overridden if vars are created with a user polarity other than None)

set_rnd_seed(seed)

Set the solver’s random seed to the given double value. Cannot be 0.0.

simplify()

Call Solver.simplify().

solve(assumptions=None)

Solve the current set of clauses, optionally with a set of assumptions.

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

True if the clauses (and assumptions) are satisfiable, False otherwise.

class minisolvers.MinisatSubsetSolver

Bases: minisolvers.SubsetMixin, minisolvers.MinisatSolver

A class for reasoning about subsets of constraints within MiniSat.

>>> S = MinisatSubsetSolver()

It must be told explicitly how many of its variables are “real” and how many are relaxation variables for constraints.

>>> S.set_varcounts(vars = 4, constraints = 5)

And variables must be created for both the “real” variables and the relaxation variables.

>>> for i in range(4+5):
...     _ = S.new_var()

“Soft” clauses are added with add_clause_instrumented(), which has no return value, as it is impossible for these clauses to produce a conflict.

>>> for i, clause in enumerate([[1], [-2], [-1, 2, 3], [-3], [-1]]):
...     S.add_clause_instrumented(clause, i)

Any subset of the constraints can be tested for satisfiability. Subsets are specified as sequences of soft clause indexes.

>>> S.solve_subset([0,1,2])
True

Extra assumptions can be passed to solve_subset():

>>> S.solve_subset([0,1,2], extra_assumps=[-3])
False
>>> S.solve_subset([0,1,2], extra_assumps=[3])
True

If a subset is found to be satisfiable, a potentially larger satisfied subset can be found. Satisfiable subsets are returned as array objects.

>>> satset = S.sat_subset()
>>> sorted(satset)
[0, 1, 2]

If a subset is found to be unsatisfiable, an UNSAT core can be found. Cores are returned as array objects.

>>> S.solve_subset([0,1,2,3])
False

>>> core = S.unsat_core()
>>> sorted(core)
[0, 1, 2, 3]

add_clause(lits)

Add a clause to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is (!x0 + x1 + !x2)

Returns:

A boolean value returned from MiniSat’s addClause() function, indicating success (True) or conflict (False).

add_clause_instrumented(lits, index)

Add a “soft” clause with a relaxation variable (the relaxation var. is based on the index, which is assumed to be 0-based).

Args:

lits:

A sequence of literals specified as in add_clause().

index (int):

A 0-based index into the set of soft constraints. The clause will be given a relaxation variable based on this index, and it will be used to specify the clause in subsets for solve_subset(), etc.

block_model()

Block the current model from the solver.

check_complete(positive_lits=None, negative_lits=None)

Check whether a given complete assignment satisfies the current set of clauses. For efficiency, it may be given just the positive literals or just the negative literals.

Args:

positive_lits, negative_lits:

Optional sequences (exactly one must be specified) containing literals as integers, specified as in add_clause(). If positive literals are given, the assignment will be completed assuming all other variables are negative, and vice-versa if negative literals are given.

Returns:

True if the assignment satisfies the current clauses, False otherwise.

get_model(start=0, end=-1)

Get the current model from the solver, optionally retrieving only a slice.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

Returns:

An array of booleans indexed to each variable (from 0). If a start index was given, the returned list starts at that index (i.e., get_model(10)[0] is index 10 from the solver’s model.

get_model_trues(start=0, end=-1, offset=0)

Get variables assigned true in the current model from the solver.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

offset (int):

Optional offset to be added to the zero-based variable numbers from MiniSat.

Returns:

An array of true variables in the solver’s current model. If a start index was given, the variables are indexed from that value.

get_stats()

Returns a dictionary of solver statistics.

implies(assumptions=None)

Get literals known to be implied by the current formula. (I.e., all assignments made at level 0.)

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

An array of literals implied by the current formula (and optionally the given assumptions).

model_value(i)

Get the value of a given variable in the current model.

nclauses()

Get the number of clauses or constraints added to the solver.

new_var(polarity=None, dvar=True)

Create a new variable in the solver.

Args:

polarity (bool):

The default polarity for this variable. True = variable’s default is True, etc. Note that this is the reverse of the ‘user polarity’ in MiniSat, where True indicates the sign is True. The default, None, creates the variable using Minisat’s default, which assigns a variable False at first, but then may change that based on the phase-saving setting.

dvar (bool):

Whether this variable will be used as a decision variable.

Returns:

The new variable’s index (0-based counting).

nvars()

Get the number of variables created in the solver.

sat_subset(offset=0)

Get the set of clauses satisfied in the last check performed by solve_subset(). Assumes the last such check was SAT. This may contain additional soft constraints not in the subset that was given to solve_subset(), if they were also satisfied by the model found.

Args:

offset (int):

Optional offset to be added to the zero-based indexes from MiniSat.

Returns:

An array of constraint indexes comprising a satisfiable subset.

set_phase_saving(ps)

Set the level of phase saving (0=none, 1=limited, 2=full (default)).

set_rnd_init_act(val)

Set whether variables are intialized with a random initial activity. (default: False)

set_rnd_pol(val)

Set whether random polarities are used for decisions (overridden if vars are created with a user polarity other than None)

set_rnd_seed(seed)

Set the solver’s random seed to the given double value. Cannot be 0.0.

set_varcounts(vars, constraints)

Record how many of the solver’s variables and clauses are “original,” as opposed to clause-selector variables, etc.

simplify()

Call Solver.simplify().

solve(assumptions=None)

Solve the current set of clauses, optionally with a set of assumptions.

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

True if the clauses (and assumptions) are satisfiable, False otherwise.

solve_subset(subset, extra_assumps=None)

Solve a subset of the constraints containing all “hard” clauses (those added with the regular add_clause() method) and the specified subset of soft constraints.

Args:

subset:

A sequence of the indexes of any soft constraints to be included.

extra_assumps:

An optional sequence of extra literals to use when solving.

Returns:

True if the given subset is satisfiable, False otherwise.

unsat_core(offset=0)

Get an UNSAT core from the last check performed by solve_subset(). Assumes the last such check was UNSAT.

Args:

offset (int):

Optional offset to be added to the zero-based indexes from MiniSat.

Returns:

An array of constraint indexes comprising an UNSAT core.

class minisolvers.MinicardSubsetSolver

Bases: minisolvers.SubsetMixin, minisolvers.MinicardSolver

A class for reasoning about subsets of constraints within MiniCard.

This has the same interface as MinisatSubsetSolver, with the addition of the add_atmost() method.

>>> S = MinicardSubsetSolver()
>>> S.set_varcounts(vars = 4, constraints = 5)
>>> for i in range(4+5):
...     _  = S.new_var()
>>> for i, clause in enumerate([[1], [-2], [3], [4]]):
...     S.add_clause_instrumented(clause, i)

AtMost and AtLeast constraints can be instrumented as well as clauses.

>>> S.add_atmost_instrumented([1,-2,3], 2, 4)

>>> S.solve_subset([0,1,4])
True
>>> S.solve_subset([0,1,2,3,4])
False

>>> core = S.unsat_core()
>>> sorted(core)
[0, 1, 2, 4]

add_atmost_instrumented(lits, k, index)

Add a “soft” ATMost constraint with a relaxation variable (the relaxation variable is based on the index, which is assumed to be 0-based).

Args:

lits:

A sequence of literals specified as in add_atmost().

k (int):

The [upper] bound to place on these literals.

index (int):

A 0-based index into the set of soft constraints. The clause will be given a relaxation variable based on this index, and it will be used to specify the clause in subsets for solve_subset(), etc.

add_atleast_instrumented(lits, k, index)

Convenience function to add a soft AtLeast constraint. Translates the AtLeast into an equivalent AtMost. See add_atmost_instrumented().

Args:

lits:

A sequence of literals specified as in add_atmost().

k (int):

The [lower] bound to place on these literals.

index (int):

A 0-based index into the set of soft constraints. The clause will be given a relaxation variable based on this index, and it will be used to specify the clause in subsets for solve_subset(), etc.

add_atleast(lits, k)

Convenience function to add an AtLeast constraint. Translates the AtLeast into an equivalent AtMost. See add_atmost().

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is {!x0, x1, !x2}

k (int):

The [lower] bound to place on these literals.

Returns:

A boolean value returned from MiniCard’s addAtMost() function, indicating success (True) or conflict (False).

add_atmost(lits, k)

Add an AtMost constraint to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is {!x0, x1, !x2}

k (int):

The [upper] bound to place on these literals.

Returns:

A boolean value returned from MiniCard’s addAtMost() function, indicating success (True) or conflict (False).

add_clause(lits)

Add a clause to the solver.

Args:

lits:

A sequence of literals as integers. Each integer specifies a variable with 1-based counting and a sign via the sign of the integer. Ex.: [-1, 2, -3] is (!x0 + x1 + !x2)

Returns:

A boolean value returned from MiniSat’s addClause() function, indicating success (True) or conflict (False).

add_clause_instrumented(lits, index)

Add a “soft” clause with a relaxation variable (the relaxation var. is based on the index, which is assumed to be 0-based).

Args:

lits:

A sequence of literals specified as in add_clause().

index (int):

A 0-based index into the set of soft constraints. The clause will be given a relaxation variable based on this index, and it will be used to specify the clause in subsets for solve_subset(), etc.

block_model()

Block the current model from the solver.

check_complete(positive_lits=None, negative_lits=None)

Check whether a given complete assignment satisfies the current set of clauses. For efficiency, it may be given just the positive literals or just the negative literals.

Args:

positive_lits, negative_lits:

Optional sequences (exactly one must be specified) containing literals as integers, specified as in add_clause(). If positive literals are given, the assignment will be completed assuming all other variables are negative, and vice-versa if negative literals are given.

Returns:

True if the assignment satisfies the current clauses, False otherwise.

get_model(start=0, end=-1)

Get the current model from the solver, optionally retrieving only a slice.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

Returns:

An array of booleans indexed to each variable (from 0). If a start index was given, the returned list starts at that index (i.e., get_model(10)[0] is index 10 from the solver’s model.

get_model_trues(start=0, end=-1, offset=0)

Get variables assigned true in the current model from the solver.

Args:

start, end (int):

Optional start and end indices, interpreted as in range().

offset (int):

Optional offset to be added to the zero-based variable numbers from MiniSat.

Returns:

An array of true variables in the solver’s current model. If a start index was given, the variables are indexed from that value.

get_stats()

Returns a dictionary of solver statistics.

implies(assumptions=None)

Get literals known to be implied by the current formula. (I.e., all assignments made at level 0.)

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

An array of literals implied by the current formula (and optionally the given assumptions).

model_value(i)

Get the value of a given variable in the current model.

nclauses()

Get the number of clauses or constraints added to the solver.

new_var(polarity=None, dvar=True)

Create a new variable in the solver.

Args:

polarity (bool):

The default polarity for this variable. True = variable’s default is True, etc. Note that this is the reverse of the ‘user polarity’ in MiniSat, where True indicates the sign is True. The default, None, creates the variable using Minisat’s default, which assigns a variable False at first, but then may change that based on the phase-saving setting.

dvar (bool):

Whether this variable will be used as a decision variable.

Returns:

The new variable’s index (0-based counting).

nvars()

Get the number of variables created in the solver.

sat_subset(offset=0)

Get the set of clauses satisfied in the last check performed by solve_subset(). Assumes the last such check was SAT. This may contain additional soft constraints not in the subset that was given to solve_subset(), if they were also satisfied by the model found.

Args:

offset (int):

Optional offset to be added to the zero-based indexes from MiniSat.

Returns:

An array of constraint indexes comprising a satisfiable subset.

set_phase_saving(ps)

Set the level of phase saving (0=none, 1=limited, 2=full (default)).

set_rnd_init_act(val)

Set whether variables are intialized with a random initial activity. (default: False)

set_rnd_pol(val)

Set whether random polarities are used for decisions (overridden if vars are created with a user polarity other than None)

set_rnd_seed(seed)

Set the solver’s random seed to the given double value. Cannot be 0.0.

set_varcounts(vars, constraints)

Record how many of the solver’s variables and clauses are “original,” as opposed to clause-selector variables, etc.

simplify()

Call Solver.simplify().

solve(assumptions=None)

Solve the current set of clauses, optionally with a set of assumptions.

Args:

assumptions:

An optional sequence of literals as integers, specified as in add_clause().

Returns:

True if the clauses (and assumptions) are satisfiable, False otherwise.

solve_subset(subset, extra_assumps=None)

Solve a subset of the constraints containing all “hard” clauses (those added with the regular add_clause() method) and the specified subset of soft constraints.

Args:

subset:

A sequence of the indexes of any soft constraints to be included.

extra_assumps:

An optional sequence of extra literals to use when solving.

Returns:

True if the given subset is satisfiable, False otherwise.

unsat_core(offset=0)

Get an UNSAT core from the last check performed by solve_subset(). Assumes the last such check was UNSAT.

Args:

offset (int):

Optional offset to be added to the zero-based indexes from MiniSat.

Returns:

An array of constraint indexes comprising an UNSAT core.