diff --git a/.github/rho_docs_en/basic.md b/.github/rho_docs_en/basic.md index 388369f..2d86680 100644 --- a/.github/rho_docs_en/basic.md +++ b/.github/rho_docs_en/basic.md @@ -136,8 +136,8 @@ the 1+1 evolutionary algorithm. Each run starts from a random point (a random vector of [BACKDOORSIZE] length over the variables of the original formula) defined by seed, after which, the ρ-value for the given backdoor is computed. -ρ-Value in short is the ratio of the number of tasks solved -for a given constraint to the total number of tasks +ρ-Value in short is the ratio of the number of tasks, +for those propagate gives a conflict to the total number of tasks (for detailed information see [Preliminaries](theory.md)). Then, changes are made in the starting vector according to (1+1)EA @@ -146,16 +146,18 @@ in order to maximize the ρ-value. After a certain number of iterations the backdoor with the maximum ρ-value among those found (or several backdoors, if ρ-value is equal). -[//]: # (Этот сегмент нужно будет переписать под вариант, когда бэкдоры -с одной хардтаской учитываются уже в процессе поиска.) +If a backdoor with a single hard task is searched, +unit clauses from it are immediately written to CNF, +and the corresponding variables are excluded from +the set of variables used to search for backdoors. -After searching for backdoors, trivial deriving is started, -which is a process where all backdoors with the same hard task -are recorded as unit clauses. This fills the set of "covered" -variables. Next, useless backdoors that do not expand -the set of variables are weeded out. +[//]: # (After searching for backdoors, trivial deriving is started, + which is a process where all backdoors with the same hard task + are recorded as unit clauses. This fills the set of "covered" + variables. Next, useless backdoors that do not expand + the set of variables are weeded out.) -Next, a full-fledged deriving is started, which includes +Next, a deriving process is started, which includes selection of a backdoor, extraction of easy tasks from it, their subsequent writing as a conjunctive normal form (CNF) and minimisation using the [Espresso tool](https://github.com/Gigantua/Espresso). diff --git a/README_en.md b/README_en.md index 6505199..85bf522 100644 --- a/README_en.md +++ b/README_en.md @@ -7,7 +7,15 @@ # EvoGuessAI -Component for finding decomposition sets and estimating hardness of SAT instances. The search for decomposition sets is realized via the optimization of the special pseudo-Boolean black-box functions that estimate the hardness of the decomposition corresponding to the employed decomposition method and the considered set. To optimize the value of such functions the component uses metaheuristic algorithms, in particular, the evolutionary ones. +A component for finding decomposition sets and using them to solve SAT instances. +The search for decomposition sets is performed by optimising special +pseudo-boolean black-box functions that evaluate either the ρ-value +in the case of using EvoguessAI in ρ-backdoors mode, or the decomposition +hardness corresponding to the decomposition method used +and the set under consideration in the case of IBS mode. +The component uses metaheuristic algorithms, in particular +evolutionary algorithms, to optimise the values of such functions. + ## Installation @@ -16,61 +24,79 @@ git clone git@github.com:ctlab/evoguess-ai.git cd evoguess-ai pip install -r requirements.txt ``` -To use EvoGuessAI in MPI mode, you also need to install: -```shell script -pip install -r requirements-mpi.txt -``` +[//]: # (To use EvoGuessAI in MPI mode, you also need to install:) -### How to MPI use +[//]: # () +[//]: # (```shell script) -The EvoGuessAI can be run in MPI mode as follows: +[//]: # (pip install -r requirements-mpi.txt) -```shell script -mpiexec -n -perhost python3 -m mpi4py.futures main.py -``` +[//]: # (```) -where **perhost** is MPI workers processes on one node, and **workers** is a total MPI workers processes on all dedicated nodes. +### Dependences -## ρ-Backdoors module +Requirement packages: +1. [numpy](https://numpy.org/) (>=1.21.6) + > pip install numpy -EvoGuessAI supports the use of ρ-backdoors to solve SAT in relation to СNF and MaxSAT in relation to WCNF. +2. [python-sat](https://pysathq.github.io/) (>=1.8.dev4) – PySAT is a toolkit +that provides extremely convenient functionality for using SAT oracles. + > pip install python-sat -ρ-Backdoor, in short, is a backdoor that allows you to decompose the original CNF into two subsets of subtasks. The first will consist of subtasks that the SAT oracle solves for a certain limitation by some measure (most often, time or number of conflicts), the second of all other subtasks. The proportion of the first subset is (ρ), the second is (1-ρ). +Optional packages: +1. [tqdm](https://tqdm.github.io/) – package for logging the process. + > pip install tqdm -In practice (and in EvoGuessAI), such backdoors are sought to maximize ρ. Accordingly, each backdoor will generate a small number of complex subtasks (also called _hard tasks_). However, we can use the hard tasks received from different backdoors together. +## ρ-Backdoors mode -EvoGuessAI is able to build backdoors while maximizing the ρ value. Then the iterative process of filtering out hard tasks is started. At each iteration, the Cartesian product of hard tasks from different ρ-backdoors is built and then it is filtered to find new hard tasks. At some point, all the hard tasks begin to be solved for the set limit to some extent. If the ρ-backdoors for building Cartesian products end earlier, then the restriction is disabled and all remaining tasks are completed as usual. +EvoGuessAI supports the use of ρ-backdoors to solve SAT in relation to +СNF and MaxSAT in relation to WCNF. -### Requirements +ρ-Backdoor, in short, is a backdoor that allows you to decompose +the original CNF into two subsets of subtasks. The first will consist of +subtasks that the SAT oracle solves for a certain limitation +by some measure (most often, time or number of conflicts), +the second of all other subtasks. +The proportion of the first subset is (ρ), the second is (1-ρ). -Optional: -1. tqdm – package for logging the process. -```shell -pip install tqdm -``` +In practice (and in EvoGuessAI), such backdoors are sought to maximize ρ. +Accordingly, each backdoor will generate a small number of complex +subtasks (also called _hard tasks_). However, we can use the hard tasks +received from different backdoors together. -[//]: # (Требуемые пакеты, опциональные и обязательные, и тд) +EvoGuessAI is able to build backdoors while maximizing the ρ value. +Then the iterative process of filtering out hard tasks is started. +At each iteration, the Cartesian product of hard tasks from different +ρ-backdoors is built and then it is filtered to find new hard tasks. +At some point, all the hard tasks begin to be solved for +some limit (in time or conflicts). If the ρ-backdoors for +building Cartesian products end earlier, then the limit +is disabled and all remaining tasks are completed as usual. -[//]: # () -[//]: # ((заглушка для tqdm надо доделать, желательно)) -### ρ-Backdoor's module documentation +### Usage + +``` +python3 main_rho.py [-h] + [-s [SOLVERNAME]] [-nr [NOFEARUNS]] + [-np [NOFPROCESSES]] [-bds [BACKDOORSIZE]] + [-tl [TIMELIMIT]] [-cl [CONFLICTLIMIT]] + formula +``` -In the [Markdown](https://en.wikipedia.org/wiki/Markdown) file -[`intro.md`](rho_docs_en/intro.md). ### ρ-Backdoor's module command line parameters | Argument full name | Short name | Description | -|--------------------|------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| --formula | -f | file with input formula (CNF or WCNF format), is a required parameter | -| --solvername | -s | short name of the SAT solver used as the SAT oracle. Available names: g3 -- Glucose 3; cd, cd 15, cd19 -- different versions of Cadical (see PySAT docs) | -| --nofearuns | -nr | the number of runs of the evolutionary algorithm for searching for ρ-backdoors. Each launch can result in the generation of several ρ-backdoors if they have the same ρ | -| --nofprocesses | -np | the number of available processes for multithreading | -| --backdoorsize | -bds | the size of the ρ-backdoors being searched | -| --timelimit | -tl | time limit for the SAT oracle when solving hard tasks | -| --conflictlimit | -cl | limit on the number of conflicts for the SAT oracle when solving hard tasks. At startup, only one of the options for restrictions is selected (the maximum set), respectively, either a time limit or a number of conflicts should be set | +|------------------|---------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| formula | | file with input formula (CNF or WCNF format), is a positional parameter | +| --solvername | -s | short name of the SAT solver used as the SAT oracle. Available names: g3 -- Glucose 3; cd, cd 15, cd19 -- different versions of Cadical (see PySAT docs) | +| --nofearuns | -nr | the number of runs of the evolutionary algorithm for searching for ρ-backdoors. Each launch can result in the generation of several ρ-backdoors if they have the same ρ | +| --nofprocesses | -np | the number of available processes for multithreading | +| --backdoorsize | -bds | the size of the ρ-backdoors being searched | +| --timelimit | -tl | time limit for the SAT oracle when solving hard tasks | +| --conflictlimit | -cl | limit on the number of conflicts for the SAT oracle when solving hard tasks. At startup, only one of the options for restrictions is selected (the maximum set), respectively, either a time limit or a number of conflicts should be set | [//]: # (Мб стоит сид убать в адвансед параметры, всетаки это не особо "осознанный" параметр в плане изменения) @@ -82,10 +108,7 @@ In the [Markdown](https://en.wikipedia.org/wiki/Markdown) file [//]: # () [//]: # (Можно добавить (в документции) доп параметры для advanced использования, которые будут уже не в командной строке, а внутри main_p. К примеру параметр перезапуска екзекьютора) -Template: -```shell -python3 ./main_rho.py -f [options] -``` + Example: ```shell python3 ./main_rho.py -f ./examples/data/lec_sort_PvS_8_3.cnf -s g3 -nr 40 -np 8 -bds 10 -tl 0 -cl 20000 @@ -96,11 +119,11 @@ Command above will launch EvoGuessAI in the mode of using algorithms for eight 3-bit numbers). 8 processes will be used in the solution. The evolutionary algorithm will be run 40 times, while looking for ρ-backdoors of length 10. Hard tasks -will be solved with a limit of 20,000 conflicts per hard task. +will be solved with a limit of 20,000 conflicts per task. Result with comments: -[//]: # (сделать такой формат примера, чтобы комментарии выделялись визуально) +[//]: # (TODO нужен нормальный пример) ```shell 00:00:01 ---------------------- Running on 4 threads ---------------------- 00:00:01 ------------------------------------------------------------------- @@ -163,87 +186,144 @@ Result with comments: ``` -[//]: # (Нужен эффективный пример) +[//]: # (## IBS mode) + -[//]: # (Показать примеры работы прям тут с пояснениями и все такое) +[//]: # (### How to MPI use) [//]: # () -[//]: # (Нужно добавить функционал, чтобы если у нас бэкдор с одной хардтаской, то сразу добавляем юниты к кнф через солвер.екстенд) +[//]: # (The EvoGuessAI can be run in MPI mode as follows:) -[//]: # (и бэкдор тогда не доабвляем) +[//]: # () +[//]: # (```shell script) + +[//]: # (mpiexec -n -perhost python3 -m mpi4py.futures main.py) + +[//]: # (```) [//]: # () -[//]: # (И вообще все сложнее, потому что эти переменные могут быть в бэкдорах, найденных до этого. И ещё из пространтсва поиска надо удалять юниты. А для этого надо чтобы в принципе пространство поиска динамически менялось) +[//]: # (where **perhost** is MPI workers processes on one node, ) + +[//]: # (and **workers** is a total MPI workers processes on all dedicated nodes.) + + +[//]: # (## Usage examples) [//]: # () -[//]: # (solver._solver.add_clause([l for l in hard task]) (только надо ещё проверить что _solver существует)) +[//]: # (An example of [probabilistic backdoors searching](https://github.com/aimclub/evoguess-ai/blob/master/examples/pvs_search_example.py) to solve the equivalence checking problem of two Boolean schemes that implement different algorithms, using the example of PvS 7x4 encoding (Pancake vs Selection sort).) [//]: # () -[//]: # (Ещё хорошая идея после поиска бэкдоров убивать все солверы и потом их пересоздавать, чтобы чистился кэш) -[//]: # (Ещё нужно сделать, чтобы бэкдоры искались с константным решателем с быстрым пропагейтом, а вот потом уже решение шло на выбранном пользователем решателе) - -## Usage examples - -An example of [probabilistic backdoors searching](https://github.com/aimclub/evoguess-ai/blob/master/examples/pvs_search_example.py) to solve the equivalence checking problem of two Boolean schemes that implement different algorithms, using the example of PvS 7x4 encoding (Pancake vs Selection sort). - -```python -root_path = WorkPath('examples') -data_path = root_path.to_path('data') -cnf_file = data_path.to_file('pvs_4_7.cnf', 'sort') -logs_path = root_path.to_path('logs', 'pvs_4_7') - -problem = SatProblem( - encoding=CNF(from_file=cnf_file), - solver=PySatSolver(sat_name='g3'), -) -solution = Optimize( - problem=problem, - space=BackdoorSet( - by_vector=[], - variables=rho_subset( - problem, - Range(start=1, length=1213), - of_size=200 - ) - ), - executor=ProcessExecutor(max_workers=16), - sampling=Const(size=8192, split_into=2048), - function=RhoFunction( - penalty_power=2 ** 20, - measure=Propagations(), - ), - algorithm=Elitism( - elites_count=2, - population_size=6, - mutation=Doer(), - crossover=TwoPoint(), - selection=Roulette(), - min_update_size=6 - ), - limitation=WallTime(from_string='02:00:00'), - comparator=MinValueMaxSize(), - logger=OptimizeLogger(logs_path), -).launch() -``` +[//]: # (```python) -Further, the corresponding problem of checking the equivalence of two Boolean schemes using the example of PvS 7x4 encoding can be [solved using the found backdoors](https://github.com/aimclub/evoguess-ai/blob/master/examples/pvs_solve_example.py) as follows: - -```python -root_path = WorkPath('examples') -data_path = root_path.to_path('data') -cnf_file = data_path.to_file('pvs_4_7.cnf', 'sort') -logs_path = root_path.to_path('logs', 'pvs_4_7_comb') -estimation = Combine( - problem=SatProblem( - encoding=CNF(from_file=cnf_file), - solver=PySatSolver(sat_name='g3'), - ), - logger=OptimizeLogger(logs_path), - executor=ProcessExecutor(max_workers=16) -).launch(*backdoors) -``` +[//]: # (root_path = WorkPath('examples')) + +[//]: # (data_path = root_path.to_path('data')) + +[//]: # (cnf_file = data_path.to_file('pvs_4_7.cnf', 'sort')) + +[//]: # (logs_path = root_path.to_path('logs', 'pvs_4_7')) + +[//]: # () +[//]: # (problem = SatProblem() + +[//]: # ( encoding=CNF(from_file=cnf_file),) + +[//]: # ( solver=PySatSolver(sat_name='g3'),) + +[//]: # ()) + +[//]: # (solution = Optimize() + +[//]: # ( problem=problem,) + +[//]: # ( space=BackdoorSet() + +[//]: # ( by_vector=[],) + +[//]: # ( variables=rho_subset() + +[//]: # ( problem,) + +[//]: # ( Range(start=1, length=1213),) + +[//]: # ( of_size=200) + +[//]: # ( )) -Other [examples](https://github.com/aimclub/evoguess-ai/tree/master/examples) can be found in the corresponding project directory. +[//]: # ( ),) + +[//]: # ( executor=ProcessExecutor(max_workers=16),) + +[//]: # ( sampling=Const(size=8192, split_into=2048),) + +[//]: # ( function=RhoFunction() + +[//]: # ( penalty_power=2 ** 20,) + +[//]: # ( measure=Propagations(),) + +[//]: # ( ),) + +[//]: # ( algorithm=Elitism() + +[//]: # ( elites_count=2,) + +[//]: # ( population_size=6,) + +[//]: # ( mutation=Doer(),) + +[//]: # ( crossover=TwoPoint(),) + +[//]: # ( selection=Roulette(),) + +[//]: # ( min_update_size=6) + +[//]: # ( ),) + +[//]: # ( limitation=WallTime(from_string='02:00:00'),) + +[//]: # ( comparator=MinValueMaxSize(),) + +[//]: # ( logger=OptimizeLogger(logs_path),) + +[//]: # ().launch()) + +[//]: # (```) + +[//]: # () +[//]: # (Further, the corresponding problem of checking the equivalence of two Boolean schemes using the example of PvS 7x4 encoding can be [solved using the found backdoors](https://github.com/aimclub/evoguess-ai/blob/master/examples/pvs_solve_example.py) as follows:) + +[//]: # () +[//]: # (```python) + +[//]: # (root_path = WorkPath('examples')) + +[//]: # (data_path = root_path.to_path('data')) + +[//]: # (cnf_file = data_path.to_file('pvs_4_7.cnf', 'sort')) + +[//]: # (logs_path = root_path.to_path('logs', 'pvs_4_7_comb')) + +[//]: # (estimation = Combine() + +[//]: # ( problem=SatProblem() + +[//]: # ( encoding=CNF(from_file=cnf_file),) + +[//]: # ( solver=PySatSolver(sat_name='g3'),) + +[//]: # ( ),) + +[//]: # ( logger=OptimizeLogger(logs_path),) + +[//]: # ( executor=ProcessExecutor(max_workers=16)) + +[//]: # ().launch(*backdoors)) + +[//]: # (```) + +[//]: # () +[//]: # (Other [examples](https://github.com/aimclub/evoguess-ai/tree/master/examples) can be found in the corresponding project directory.) ## Supported by @@ -252,4 +332,13 @@ of [ITMO University](https://en.itmo.ru/) as part of the plan of the center's pr ## Documentation -Documentation is available [here](https://evoguess-ai.readthedocs.io/) and includes installation instructions and base usage manual. +Documentation for the main modes of the EvoguessAI usage is available +in the [Markdown](https://en.wikipedia.org/wiki/Markdown) file [`intro.md`](rho_docs_en/intro.md). + +## Low-level usage + +Also EvoguessAI supports its use at low level and as a library. +In this mode the user can use his own implementations of classes and functions. +Documentation for this mode of use is available +[here](https://evoguess-ai.readthedocs.io/) and includes installation +instructions and base usage manual.