author = {Tudor Jebelean and Gabor Kusper},
title = {{SAT Solving Experiments in Multi-Domain Logic}},
language = {english},
abstract = {{\bf Signed logic} is a generalization of propositional logic, in which literals are of the form $x \in A$, where $x$ is a symbol denoting a variable and $A$ is a constant set. (For instance if the sets are only $\{\rm{True}\}$ and $\{\rm{False}\}$, then one obtains the classical propositional logic.) This is different from multivalued logic because the sets of logical values can be different for different variables and in different clauses. The SAT problem, the resolution method, as well as DPLL generalize in a natural way to signed logic, however there have been no practical attempts of using these for solving such problems directly, rather most of the research concentrated on translating signed logic formulae into propositional formulae, thus making it possible to use the available SAT techniques. We propose generalize signed logic to {\bf multi-domain logic (MDL)} -- in which each variable has its own domain, moreover the variables and the domains change during the solving process. Using this concept we approach the SAT problems in the opposite way, namely by transforming classical propositional SAT problems into MDL problems by {\em clustering} more classical variables into {\em multivariables}. (For instance two classical variables $x, y \in \{0, 1\}$ can {\em merge} into a new {\em multi-variable} $xy \in \{00, 01, 10, 11\}$.) In contrast to classical unit propagation, in this context the simultaneous propagation of several (non-unit) clauses is possible. We generalize the DPLL algorithm to MDL by allowing the domains of these multivariables to change in time: the domain shrinks whenever a new unit clause for the respective variable is generated. Moreover, when the domains of some multivariables are small enough, we merge again these multivariables, thus allowing again a more efficient propagation of information. This last feature is novel, it has not been mentioned in previous descriptions of signed logic solvers. We present systematic experiments using a generalized DPLL algorithm in a preliminary Java implementation (with eager data structures) on some scalable classes of unsatisfiable problems: random 3-literal, pigeon-hole, and application generated (as e. g. from bounded model checking). Our results exhibit a speed-up of two orders of magnitude between different strategies, depending on: the size of multi-variables, preprocessing by appropriate grouping of variables, detection of irrelevant search branches, dynamic re-merging of multi-variables, etc. These results show that it is worth to improve the method and the practical implementation because it has good prospects of being competitive with modern SAT solvers, and in particular could also be more efficient for the direct solving of signed logic problems generated by specific applications.},
year = {2010},
month = {January 30},
note = {Contributed talk at 8th International Conference on Applied Informatics (ICAI 2010)},
conferencename = {8th International Conference on Applied Informatics (ICAI 2010)}