As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
One of the most critical components of Branch & Bound (BnB) solvers for Max-SAT is the estimation of the lower bound. At each node of the search tree, they detect inconsistent subsets (IS) of the formula by unit propagation based methods and apply a treatment to them. The currently best performing Max-SAT BnB solvers perform a very little amount of memorization, thus the same IS may be detected and treated several times during the exploration of the search tree. We address in this paper the problem of increasing the learning performed by BnB solvers. We present new sets of clause patterns which produce unit resolvent clauses when they are transformed by max-resolution. We study experimentally the impact of these transformation' memorization in our solver AHMAXSAT and we discuss their effects on the solver behavior.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.