Parallel Learning Portfolio-Based Solvers

From LRDE

Abstract

Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SAT- isfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration- Exploitation using Exponential weight (EXP3)that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results.

Documents

Bibtex (lrde.bib)

@InProceedings{	  menouer.17.iccs,
  author	= {Tarek Menouer and Souheib Baarir},
  title		= {Parallel Learning Portfolio-Based Solvers},
  booktitle	= {Proceedings of the International Conference on
		  Computational Science (ICCS)},
  month		= jun,
  address	= {Zurich, Switzerland},
  pages		= {335--344},
  year		= {2017},
  abstract	= {Exploiting multi-core architectures is a way to tackle the
		  CPU time consumption when solving SAT- isfiability (SAT)
		  problems. Portfolio is one of the main techniques that
		  implements this principle. It consists in making several
		  solvers competing, on the same problem, and the winner will
		  be the first that answers. In this work, we improved this
		  technique by using a learning schema, namely the
		  Exploration- Exploitation using Exponential weight (EXP3),
		  that allows smart resource allocations. Our contribution is
		  adapted to situations where we have to solve a bench of SAT
		  instances issued from one or several sequence of problems.
		  Our experiments show that our approach achieves good
		  results.}
}