@techreport{RISC3948,author = {Tudor Jebelean and Gabor Kusper},
title = {{Experiments with Multi-Domain Logic: Variable Merging and Split Strategies}},
language = {English},
abstract = {Multi-Domain Logic (MDL) is a generalization of signed logic, in which
every variable has its own domain.
This aspect increases the efficiency of direct solving of MDL satisfiability,
because the solving process proceeds by reducing the size of the domains
(contradiction appears as an empty domain).
In contrast to the usual approach of translating signed logic satisfiability
into boolean satisfiability, we implement the generalized DPLL directly for
MDL, using a specific version of the techniques used for signed logic.
Moreover, we use a novel techinque -- {\em variable merging}, which
consists in replacing two or more variables by a new one, whose domain is the
cartesian product of the old domains.
This operation is used during the solving process in order to reduce the number of variables.
Moreover, variable merging can be used at the beginning of the solving process
in order to translate a boolean SAT problem into an MDL problem.
This opens the possibility of using MDL solvers as an alternative to boolean
solvers, which is promising because in MDL several boolean constraints can be
propagated simultaneously.
Our experiments with a prototype eager solver show the effects of the initial
merging factor of boolean variables, as well as the effects of different
design decisions on the efficiency of the method.},
number = {10-03},
year = {2010},
month = {February},
keywords = {SAT, signed logic, Multi-Domain Logic},
length = {10},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}