144
J. Bend´ ık and I. ˇ
Cern´ a
Finally, Explorer provides one more functionality. Given an unexplored subset
N , Explorer can collect minable critical constraints of N . Recall that a constraint
c ∈ N is minable critical for N iff N \ {c} is explored. All the minable critical
constraints can be determined based on the formula map
+
∧map
− . In particular,
if we simplify the formula by fixing the variables {x i |c i ∈ N } to False, then
values of some variables from {x i |c i ∈ N } will be implied to be True. These
implicants correspond to the minable critical constraints. This observation has
been already exploited by Liffiton et al. [22] and they use miniSAT to obtain
the implicants in their tool. However, the miniSAT’s procedure for computing
the implicants is not dedicated solely to this purpose; it is optimized w.r.t. the
overall satisfiability solving process. Therefore, a use of miniSAT for this task
brings an unnecessary overhead. In our tool, we directly compute the implicants
from the formula map
+ instead of using a SAT solver to do it.
4.3 SatSolver
SatSolver (declared in SatSolver.h) is an abstract class stating all the domain
specific functionality that needs to be implemented (in a derived class) to support
a particular constraint domain in our tool. There are three methods that have
to be implemented by every derived class:
– toString(N ) takes as an input a set N , N ⊆ C, and returns a textual
representation of the constraints contained in N (e.g. in the SMT-LIB 2
format if N is a set of SMT constraints). We use this method to output the
identified MUSes.
– solve(N , core = False, extension = False) takes as an input a subset N
of C and returns True iff N is satisfiable and False otherwise. Moreover,
solve takes two optional Boolean parameters, core and extension, with default values set to False. If core is set to True and N is unsatisfiable, solve
also finds an unsat core of N , i.e. an unsatisfiable M such that M ⊆ N .
Similarly, if extension is set to True and N is satisfiable, solve finds an
extension of N , i.e. a satisfiable set M such that N ⊆ M ⊆ C. We use the
unsat cores in our tool to reduce seeds before shrinking. The extensions are
used to further prune the set Unexplored when an unexplored subset is found
to be satisfiable.
– constructor(filepath). Every derived class of SatSolver has to implement
its constructor. The constructor accepts a path filepath to a file that specifies
the input set C of constraints in some domain specific format (e.g. SMTLIB 2 for SMT formulae). We invoke the constructor during the initialisation
phase of our tool and its goal is to parse the input set of constraints and
internally store the constraints for future manipulations. SatSolver is the
only one of the six logical components of our tool that directly works with
particular constraints of C. All the other components work just with a bitvector representation of subsets of C. For example, if C = {c 1 , c 2 , c 3 , c 4 } is a
set of four constraints and K = {c 1 , c 2 }, the bitvector representation of K is
1100. Therefore, whenever another component communicates with SatSolver,
J. Bend´ ık and I. ˇ
Cern´ a
Finally, Explorer provides one more functionality. Given an unexplored subset
N , Explorer can collect minable critical constraints of N . Recall that a constraint
c ∈ N is minable critical for N iff N \ {c} is explored. All the minable critical
constraints can be determined based on the formula map
+
∧map
− . In particular,
if we simplify the formula by fixing the variables {x i |c i ∈ N } to False, then
values of some variables from {x i |c i ∈ N } will be implied to be True. These
implicants correspond to the minable critical constraints. This observation has
been already exploited by Liffiton et al. [22] and they use miniSAT to obtain
the implicants in their tool. However, the miniSAT’s procedure for computing
the implicants is not dedicated solely to this purpose; it is optimized w.r.t. the
overall satisfiability solving process. Therefore, a use of miniSAT for this task
brings an unnecessary overhead. In our tool, we directly compute the implicants
from the formula map
+ instead of using a SAT solver to do it.
4.3 SatSolver
SatSolver (declared in SatSolver.h) is an abstract class stating all the domain
specific functionality that needs to be implemented (in a derived class) to support
a particular constraint domain in our tool. There are three methods that have
to be implemented by every derived class:
– toString(N ) takes as an input a set N , N ⊆ C, and returns a textual
representation of the constraints contained in N (e.g. in the SMT-LIB 2
format if N is a set of SMT constraints). We use this method to output the
identified MUSes.
– solve(N , core = False, extension = False) takes as an input a subset N
of C and returns True iff N is satisfiable and False otherwise. Moreover,
solve takes two optional Boolean parameters, core and extension, with default values set to False. If core is set to True and N is unsatisfiable, solve
also finds an unsat core of N , i.e. an unsatisfiable M such that M ⊆ N .
Similarly, if extension is set to True and N is satisfiable, solve finds an
extension of N , i.e. a satisfiable set M such that N ⊆ M ⊆ C. We use the
unsat cores in our tool to reduce seeds before shrinking. The extensions are
used to further prune the set Unexplored when an unexplored subset is found
to be satisfiable.
– constructor(filepath). Every derived class of SatSolver has to implement
its constructor. The constructor accepts a path filepath to a file that specifies
the input set C of constraints in some domain specific format (e.g. SMTLIB 2 for SMT formulae). We invoke the constructor during the initialisation
phase of our tool and its goal is to parse the input set of constraints and
internally store the constraints for future manipulations. SatSolver is the
only one of the six logical components of our tool that directly works with
particular constraints of C. All the other components work just with a bitvector representation of subsets of C. For example, if C = {c 1 , c 2 , c 3 , c 4 } is a
set of four constraints and K = {c 1 , c 2 }, the bitvector representation of K is
1100. Therefore, whenever another component communicates with SatSolver,