author = {Tudor Jebelean and Gabor Kusper},
title = {{Multi-Domain Logic and its Applications to SAT}},
booktitle = {{SYNASC 2008}},
language = {English},
abstract = {We describe a new formalism and special proof methods for a novel generalization of propositional logic, which is especially suitable for solving the satisfiability problem (SAT). A Multi--Domain Logic (MDL) formula is quantifier--free and contains only atoms of the form $x \in A$, where $x$ is a variable and $A$ is a constant set. For formulae in conjunctive normal form, we are interested in finding solutions (assignments to variables which satisfy all clauses). Classical propositional logic corresponds to the special case when each set is either $\{\true\}$ or $\{\false\}$. The union of all the sets occurring for a certain variable can be seen as "the domain" of that variable, thus MDL is also a generalization of multi-valued logic, but with different domains for variables. The most distinctive feature is, however, the indication of the sub-domain in each clause. The notions of resolution, subsumption, as well as the basic steps of the DPLL method generalize in an elegant and straightforward way. As a novel MDL specific technique, {\em variable clustering} consists in creating a new variable ranging over the cartesian product of the domains of several "clustered" variables. This allows the transformation of classical SAT problems in MDL problems with less literals, and in which the propagation of information can be performed more efficiently than classical unit propagation. The basic idea of MDL originates from the earlier work of the second author on "hyper-unit" propagation (that is simultaneous propagation of several unit clauses) and on the representation and propagation of "k-literals" (generalized literals containing information on several propositional variables). Preliminary experiments with a prototype Java implementation exhibit speed--ups of up to 30 times.},
pages = {3--8},
publisher = {IEEE Society Press},
isbn_issn = {978-0-7695-3523-4},
year = {2008},
editor = {V. Negru et. al.},
refereed = {yes},
keywords = {Multi-Domain Logic, SAT, signed logic},
length = {6},
conferencename = {International Simposium on Symbolic and Numeric Scientific Computation}