Kochemazov, Stepan; Zaikin, Oleg ALIAS: a modular tool for finding backdoors for SAT. (English) Zbl 06916320 Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10929, 419-427 (2018). Summary: We present ALIAS, a modular tool aimed at finding backdoors for hard SAT instances. Here by a backdoor for a specific SAT solver and SAT formula we mean a set of its variables, all possible instantiations of which lead to construction of a family of subformulas with the total solving time less than that for an original formula. For a particular backdoor, the tool uses the Monte-Carlo algorithm to estimate the runtime of a solver when partitioning an original problem via said backdoor. Thus, the problem of finding a backdoor is viewed as a black-box optimization problem. The tool’s modular structure allows to employ state-of-the-art SAT solvers and black-box optimization heuristics. In practice, for a number of hard SAT instances, the tool made it possible to solve them much faster than using state-of-the-art multithreaded SAT-solvers.For the entire collection see [Zbl 1390.68015]. Cited in 2 Documents MSC: 68Q25 Analysis of algorithms and problem complexity 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Software:Plingeling; abcdSAT; Paramils; ALIAS ; PaInleSS PDF BibTeX XML Cite \textit{S. Kochemazov} and \textit{O. Zaikin}, Lect. Notes Comput. Sci. 10929, 419--427 (2018; Zbl 06916320) Full Text: DOI OpenURL