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.
git clone git@github.com:ctlab/evoguess-ai.git
cd evoguess-ai
pip install -r requirements.txtRequirement packages:
-
numpy (>=1.21.6)
pip install numpy
-
python-sat (~=1.8.dev4) – PySAT is a toolkit that provides convenient functionality for using SAT oracles.
pip install python-sat
Optional packages:
- tqdm – package for logging the process.
pip install tqdm
EvoGuessAI supports the use of ρ-backdoors to solve SAT in relation to СNF and MaxSAT in relation to WCNF.
ρ-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-ρ).
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.
python3 main_rho.py [-h] [-s [SOLVERNAME]] [-nr [NOFEARUNS]]
[-ni [NOFEAITERS]] [-np [NOFPROCESSES]]
[-bds [BACKDOORSIZE]] [-tl [TIMELIMIT]]
[-cl [CONFLICTLIMIT]] [-rs [RANDOMSEED]]
formula
| Argument full name | Short name | Description |
|---|---|---|
| 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 ρ |
| --nofeaiters | -ni | the number of iterations that the evolutionary algorithm completes in one run |
| --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 |
| --randomseed | -rs | random seed which is used to search for rho-backdoors |
Example:
python3 ./main_rho.py -f ./examples/data/pvs_4_7.cnf -s g3 -nr 40 -np 8 -bds 10 -tl 0 -cl 20000Command above will launch EvoGuessAI in the mode of using ρ-backdoors to solve one of the exemplary CNF (LEC problem for the "pancake" and "selection" sorting 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 task.
Result with comments:
00:00:01 ---------------------- Running on 4 threads ----------------------
00:00:01 -------------------------------------------------------------------
00:00:01 ------------------- Phase 1 (Prepare backdoors) -------------------
00:00:01 Searching: 100%|██████████| 40/40 [03:31<00:00, 5.29s/run, 7009 bds]
# In phase 1 7009 backdoors was found. It was backdoors with maximum rho from every thread.
00:03:33 Deriving: 100%|██████████| 608/608 [00:52<00:00, 11.65bd/s, 844 clauses]
# During deriving process from all backdoor 844 additional clauses was extract to the original CNF.
00:04:25 ---------------------- Prepared 10 backdoors ----------------------
# All backdoors were filtered from useless ones (not carrying new variables).
# 10 backdoors left.
00:04:25 -------------------------------------------------------------------
00:04:25 --------------------- Phase 2 (Solve problem) ---------------------
00:04:25 ------------------- Used 2 backdoors (20 vars) -------------------
00:04:25 Sifting: 100%|██████████| 4/4 [00:04<00:00, 1.06s/task, 4 hard]
# Hard tasks from first two backdoor was used to construct Cortesian product. It's lenght is 4 cubes.
# When solving these 4 cubes with a limit in conflicts, it turned out that all 4 were too difficult.
# Therefore, we add the next backdoor (builds the Cartesian product of the current set of cubes
# and the hard tasks from the next backdoor).
00:04:29 ------------------- Used 3 backdoors (22 vars) -------------------
00:04:29 Sifting: 100%|██████████| 8/8 [00:07<00:00, 1.14task/s, 8 hard]
00:04:36 ------------------- Used 4 backdoors (24 vars) -------------------
00:04:36 Sifting: 100%|██████████| 16/16 [00:15<00:00, 1.03task/s, 16 hard]
00:04:52 ------------------- Used 5 backdoors (26 vars) -------------------
00:04:52 Sifting: 100%|██████████| 32/32 [00:31<00:00, 1.02task/s, 32 hard]
00:05:23 ------------------- Used 6 backdoors (36 vars) -------------------
00:05:23 Sifting: 100%|██████████| 64/64 [01:03<00:00, 1.01task/s, 64 hard]
00:06:27 ------------------- Used 7 backdoors (38 vars) -------------------
00:06:27 Sifting: 100%|██████████| 128/128 [02:22<00:00, 1.11s/task, 125 hard]
00:08:49 ------------------- Used 8 backdoors (39 vars) -------------------
00:08:49 Sifting: 100%|██████████| 250/250 [05:41<00:00, 1.37s/task, 220 hard]
00:14:31 ------------------- Used 9 backdoors (42 vars) -------------------
00:14:31 Sifting: 100%|██████████| 440/440 [11:20<00:00, 1.55s/task, 394 hard]
00:25:51 ------------------- Used 10 backdoors (44 vars) -------------------
00:25:51 -------------- Disable solver budget (last backdoor) --------------
# Since backdoor 10 was the last one, remain hard tasks is solved without limit.
00:25:51 Sifting: 100%|██████████| 788/788 [46:31<00:00, 3.54s/task, 0 hard]
01:12:23 -------------------------------------------------------------------
01:12:23 ---------------------------- Solution ----------------------------
01:12:23 -------------------------- UNSATISFIABLE --------------------------
# EvoguessAI proved that formula is unsatisfiable.
01:12:23 -------------------------------------------------------------------
01:12:23 -------------------- Search time: 213.179 sec. --------------------
01:12:23 -------------------- Derive time: 52.396 sec. --------------------
01:12:23 ------------------- Solving time: 4077.635 sec. -------------------
01:12:23 -------------------------------------------------------------------
01:12:23 ------------------- Summary time: 4343.21 sec. -------------------python3 main_rho_im.py [-h] [-s [SOLVERNAME]] [-nl [NOFEALIMIT]]
[-ng [NOFEAGROUPS]] [-np [NOFPROCESSES]]
[-bds [BACKDOORSIZE]] [-tl [TIMELIMIT]]
[-cl [CONFLICTLIMIT]] [-rs [RANDOMSEED]]
formula
| Argument full name | Short name | Description |
|---|---|---|
| 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) |
| --nofealimit | -nl | the number of found ρ-backdoors after which the algorithm will stop searching. |
| --nofeagroups | -ni | the number of groups with different ρ value that can exist simultaneously. |
| --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 |
| --randomseed | -rs | random seed which is used to search for rho-backdoors |
Example:
python3 ./main_rho_im.py -f /examples/data/pvs_4_7.cnf -s cd195 -nl 500 -ng 5 -bds 10 -cl 20000The study is supported by the Research Center Strong Artificial Intelligence in Industry of ITMO University as part of the plan of the center's program: Development and testing of an experimental prototype of a library of strong AI algorithms in terms of the Boolean satisfiability problem solving through heuristics of working with constraints and variables, searching for probabilistic trapdoors and inverse polynomial trapdoors.
Documentation for the main modes of the EvoguessAI usage is available
in the Markdown file intro.md.
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 is available here and includes installation instructions and base usage manual.