SAT Solving Experiments in Multi-Domain Logic

Description

\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.

Period	30 Jan 2010
Event title	Contributed talk at 8th International Conference on Applied Informatics (ICAI 2010)
Event type	Conference
Location	HungaryShow on map