MUST: Minimal Unsatisfiable Subsets Enumeration Tool
143
Initializer Initializer (implemented in main.cpp) parses the command line arguments provided by the user, and creates, sets-up, and runs the Master.
4.2 Explorer
Since there can be up to exponentially many unexplored subsets w.r.t. the number of constraints in C, it is intractable to represent them explicitly. Instead, we
adopt a symbolic representation that was first proposed by Liffiton et al. [22]
and subsequently used in many other works (e.g. [1,20,10]).
Given a set C = {c 1 , c 2 , . . . , c n } of constraints, we introduce a set X =
{x 1 , x 2 , . . . , x n } of Boolean variables, and maintain two Boolean formulas, map
+
and map
− , over X such that each model of map
+
∧ map
− corresponds to an
unexplored subset and vice versa. The formulas are maintained as follows:
• Initially map
+ = map
− = True since all of P(C) are unexplored.
• To mark a satisfiable set N ⊆ C and all its subsets as explored we add to
map
+ the clause
i:ci ∈N x i .
• Symmetrically, to mark an unsatisfiable set N ⊆ C and all its supersets as
explored we add to map
− the clause
i:ci∈N ¬x i .
We use the SAT solver miniSAT [18] to hold and query the formulas map
+ and
map
− . To get an arbitrary element of Unexplored , we can ask miniSAT for a
model of map
+
∧map
− . However, in our algorithms, we need to be able to obtain
two specific kinds of unexplored subsets.
First, given a set N , N ⊆ C, we need to be able to find a maximal unexplored
subset of N . We exploit that miniSAT allows the user to fix values of some
variables and also to set the default polarity of variables, i.e. the default value
assignment to variables in decision points during the solving. To get a maximal
unexplored subset of N , we fix the values of the variables {x i |c i ∈ N } to False,
set the default polarity to True, and ask miniSAT for a model of map
+
∧ map
− .
Second, given an unexplored N , N ⊆ C, we need to find a minimal unexplored
subset B of N (this is used by TOME while constructing a chain of unexplored
subsets). To do this, we fix the values of the variables {x i |c i ∈ N } to False, set
the default polarity to False, and ask miniSAT for a model of map
+ . Note that
we do not include map
− in the query. Intuitively, map
− requires an absence of
constraints and since N satisfies map
− , every subset of N also satisfies map
− .
As for the implementation, we integrate miniSAT via it’s C API and we maintain two instances of the solver. One instance holds the formula map
+
∧ map
−
whereas the other instance holds just map
+ . Both the instances are used incrementally, i.e. the formulas are incrementally build during the whole MUS
enumeration and simplified (internally by miniSAT) when possible. Let us note
that Liffiton et al. also incrementally use miniSAT in their tool
1 . However, they
maintain just the whole conjunction map
+
∧ map
− since a separate maintenance of map
− or map
+ would not bring any speed-up in case of their MUS
enumeration algorithm.
1 https://sun.iwu.edu/%7eliffito/marco/
143
Initializer Initializer (implemented in main.cpp) parses the command line arguments provided by the user, and creates, sets-up, and runs the Master.
4.2 Explorer
Since there can be up to exponentially many unexplored subsets w.r.t. the number of constraints in C, it is intractable to represent them explicitly. Instead, we
adopt a symbolic representation that was first proposed by Liffiton et al. [22]
and subsequently used in many other works (e.g. [1,20,10]).
Given a set C = {c 1 , c 2 , . . . , c n } of constraints, we introduce a set X =
{x 1 , x 2 , . . . , x n } of Boolean variables, and maintain two Boolean formulas, map
+
and map
− , over X such that each model of map
+
∧ map
− corresponds to an
unexplored subset and vice versa. The formulas are maintained as follows:
• Initially map
+ = map
− = True since all of P(C) are unexplored.
• To mark a satisfiable set N ⊆ C and all its subsets as explored we add to
map
+ the clause
i:ci ∈N x i .
• Symmetrically, to mark an unsatisfiable set N ⊆ C and all its supersets as
explored we add to map
− the clause
i:ci∈N ¬x i .
We use the SAT solver miniSAT [18] to hold and query the formulas map
+ and
map
− . To get an arbitrary element of Unexplored , we can ask miniSAT for a
model of map
+
∧map
− . However, in our algorithms, we need to be able to obtain
two specific kinds of unexplored subsets.
First, given a set N , N ⊆ C, we need to be able to find a maximal unexplored
subset of N . We exploit that miniSAT allows the user to fix values of some
variables and also to set the default polarity of variables, i.e. the default value
assignment to variables in decision points during the solving. To get a maximal
unexplored subset of N , we fix the values of the variables {x i |c i ∈ N } to False,
set the default polarity to True, and ask miniSAT for a model of map
+
∧ map
− .
Second, given an unexplored N , N ⊆ C, we need to find a minimal unexplored
subset B of N (this is used by TOME while constructing a chain of unexplored
subsets). To do this, we fix the values of the variables {x i |c i ∈ N } to False, set
the default polarity to False, and ask miniSAT for a model of map
+ . Note that
we do not include map
− in the query. Intuitively, map
− requires an absence of
constraints and since N satisfies map
− , every subset of N also satisfies map
− .
As for the implementation, we integrate miniSAT via it’s C API and we maintain two instances of the solver. One instance holds the formula map
+
∧ map
−
whereas the other instance holds just map
+ . Both the instances are used incrementally, i.e. the formulas are incrementally build during the whole MUS
enumeration and simplified (internally by miniSAT) when possible. Let us note
that Liffiton et al. also incrementally use miniSAT in their tool
1 . However, they
maintain just the whole conjunction map
+
∧ map
− since a separate maintenance of map
− or map
+ would not bring any speed-up in case of their MUS
enumeration algorithm.
1 https://sun.iwu.edu/%7eliffito/marco/