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 withadd_clause()
, analogous to MiniSat’saddClause()
. Literals are specified as integers, with the magnitude indicating the variable index (with 1based 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 1based 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 viceversa 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 zerobased 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 phasesaving setting.
 dvar (bool):
 Whether this variable will be used as a decision variable.
 Returns:
 The new variable’s index (0based 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 theadd_atmost()
andadd_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()
, theadd_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 1based 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 1based 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 1based 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 viceversa 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 zerobased 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 phasesaving setting.
 dvar (bool):
 Whether this variable will be used as a decision variable.
 Returns:
 The new variable’s index (0based 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 1based 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 0based).
 Args:
 lits:
 A sequence of literals specified as in
add_clause()
.  index (int):
 A 0based 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 viceversa 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 zerobased 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 phasesaving setting.
 dvar (bool):
 Whether this variable will be used as a decision variable.
 Returns:
 The new variable’s index (0based 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 tosolve_subset()
, if they were also satisfied by the model found. Args:
 offset (int):
 Optional offset to be added to the zerobased 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 clauseselector 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 zerobased 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 theadd_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 0based).
 Args:
 lits:
 A sequence of literals specified as in
add_atmost()
.  k (int):
 The [upper] bound to place on these literals.
 index (int):
 A 0based 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 0based 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 1based 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 1based 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 1based 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 0based).
 Args:
 lits:
 A sequence of literals specified as in
add_clause()
.  index (int):
 A 0based 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 viceversa 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 zerobased 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 phasesaving setting.
 dvar (bool):
 Whether this variable will be used as a decision variable.
 Returns:
 The new variable’s index (0based 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 tosolve_subset()
, if they were also satisfied by the model found. Args:
 offset (int):
 Optional offset to be added to the zerobased 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 clauseselector 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 zerobased indexes from MiniSat.
 Returns:
 An array of constraint indexes comprising an UNSAT core.
