Density condensation of Boolean formulas |
| |
Authors: | Youichi Hanatani Kazuo Iwama |
| |
Institution: | Graduate School of Informatics, Kyoto University, Kyoto 606-8501, Japan |
| |
Abstract: | The following problem is considered: given a Boolean formula f, generate another formula g such that: (i) If f is unsatisfiable then g is also unsatisfiable. (ii) If f is satisfiable then g is also satisfiable and furthermore g is “easier” than f. For the measure of this easiness, we use the density of a formula f which is defined as (the number of satisfying assignments)/2n, where n is the number of Boolean variables of f. In this paper, we mainly consider the case that the input formula f is given as a 3-CNF formula and the output formula g may be any formula using Boolean AND, OR and negation. Two different approaches to this problem are presented: one is to obtain g by reducing the number of variables and the other by increasing the number of variables, both of which are based on existing SAT algorithms. Our performance evaluation shows that, a little surprisingly, better SAT algorithms do not always give us better density-condensation algorithms. |
| |
Keywords: | Boolean formulas Density condensation Computational complexity SAT algorithms |
本文献已被 ScienceDirect 等数据库收录! |
|