Research output: Contribution to journal › Conference article › peer-review
Automated generation of simplification rules for SAT and MAXSAT. / Kulikov, Alexander S.
In: Lecture Notes in Computer Science, Vol. 3569, 17.10.2005, p. 430-436.Research output: Contribution to journal › Conference article › peer-review
}
TY - JOUR
T1 - Automated generation of simplification rules for SAT and MAXSAT
AU - Kulikov, Alexander S.
PY - 2005/10/17
Y1 - 2005/10/17
N2 - Currently best known upper bounds for many NP-hard problems are obtained by using divide-and-conquer (splitting) algorithms. Roughly speaking, there are two ways of splitting algorithm improvement: a more involved case analysis and an introduction of a new simplification rule. It is clear that case analysis can be executed by computer, so it was considered as a machine task. Recently, several programs for automated case analysis were implemented. However, designing a new simplification rule is usually considered as a human task. In this paper we show that designing simplification rules can also be automated. We present several new (previously unknown) automatically generated simplification rules for the SAT and MAXSAT problems. The new approach allows not only to generate simplification rules, but also to find good splittings. To illustrate our technique we present a new algorithm for (n, 3)-MAXSAT that uses both splittings and simplification rules based on our approach and has worst-case running time O(1.2721 N L), where N is the number of variables and L is the length of an input formula. This bound improves the previously known bound O(1.3248 N L) of Bansal and Raman.
AB - Currently best known upper bounds for many NP-hard problems are obtained by using divide-and-conquer (splitting) algorithms. Roughly speaking, there are two ways of splitting algorithm improvement: a more involved case analysis and an introduction of a new simplification rule. It is clear that case analysis can be executed by computer, so it was considered as a machine task. Recently, several programs for automated case analysis were implemented. However, designing a new simplification rule is usually considered as a human task. In this paper we show that designing simplification rules can also be automated. We present several new (previously unknown) automatically generated simplification rules for the SAT and MAXSAT problems. The new approach allows not only to generate simplification rules, but also to find good splittings. To illustrate our technique we present a new algorithm for (n, 3)-MAXSAT that uses both splittings and simplification rules based on our approach and has worst-case running time O(1.2721 N L), where N is the number of variables and L is the length of an input formula. This bound improves the previously known bound O(1.3248 N L) of Bansal and Raman.
UR - http://www.scopus.com/inward/record.url?scp=26444575408&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:26444575408
VL - 3569
SP - 430
EP - 436
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
SN - 0302-9743
T2 - 8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005
Y2 - 19 June 2005 through 23 June 2005
ER -
ID: 49824718