文件列表:

.travis.yml (1061, 2023-11-30)
CMake/ (0, 2023-11-30)
CMake/MiniSatConfig.cmake.in (72, 2023-11-30)
CMakeLists.txt (8231, 2023-11-30)
LICENSE (1142, 2023-11-30)
appveyor.yml (885, 2023-11-30)
azure-pipelines.yml (458, 2023-11-30)
conanfile.py (1734, 2023-11-30)
doc/ (0, 2023-11-30)
doc/ReleaseNotes-2.2.0.txt (3430, 2023-11-30)
jobs/ (0, 2023-11-30)
jobs/build.yml (351, 2023-11-30)
jobs/winbuild.yml (325, 2023-11-30)
minisat/ (0, 2023-11-30)
minisat/core/ (0, 2023-11-30)
minisat/core/Dimacs.h (3310, 2023-11-30)
minisat/core/EA.cc (8423, 2023-11-30)
minisat/core/EA.h (1355, 2023-11-30)
minisat/core/Fitness.h (737, 2023-11-30)
minisat/core/Instance.cc (3815, 2023-11-30)
minisat/core/Instance.h (2831, 2023-11-30)
minisat/core/Main.cc (17974, 2023-11-30)
minisat/core/OutOfMemoryException.cc (1417, 2023-11-30)
minisat/core/OutOfMemoryException.h (1763, 2023-11-30)
minisat/core/Solver.cc (43082, 2023-11-30)
minisat/core/Solver.h (22989, 2023-11-30)
minisat/core/SolverTypes.cc (772, 2023-11-30)
minisat/core/SolverTypes.h (16267, 2023-11-30)
minisat/core/ThrowOOMException.cc (1559, 2023-11-30)
minisat/core/ThrowOOMException.h (1748, 2023-11-30)
minisat/mtl/ (0, 2023-11-30)
minisat/mtl/Alg.h (2106, 2023-11-30)
minisat/mtl/Alloc.h (4494, 2023-11-30)
minisat/mtl/Heap.h (4651, 2023-11-30)
minisat/mtl/IntTypes.h (1817, 2023-11-30)
minisat/mtl/Map.h (6690, 2023-11-30)
minisat/mtl/Queue.h (3013, 2023-11-30)
... ...

# Backdoor Tree Search using Metaheuristic Minimization This repository is a fork of [minisat](https://github.com/master-keying/minisat), a SAT solver designed for efficiently solving boolean satisfiability problems. In this fork, the code has been adapted to perform fast search for tree-structured backdoors using a metaheuristic minimization algorithm. This technique is detailed in the paper "Probabilistic Generalization of Backdoor Trees with Application to SAT" by Semenov, A., Chivilikhin, D., Kochemazov, S., and Dzhiblavi, I. published in AAAI. ## Installation To build the code, follow these steps: 1. Clone this repository or download the source code. 2. Open a terminal and navigate to the repository's root directory. 3. Run the following commands: ```sh cmake -B build -DCMAKE_BUILD_TYPE=Release cmake --build build ``` ## Usage After building the code, you can use `./build/minisat` binary to search for backdoors with the specified parameters. Here is an example command: ```sh ./build/minisat original.cnf -ea-seed=42 -ea-num-runs=100 -ea-instance-size=10 -ea-num-iters=1000 -ea-output-path=backdoors_100x10x1000.txt ``` Replace `original.cnf` with the path to your CNF file. ## Parameters - `-ea-num-runs`: Number of backdoors (each EA run produces one "best" backdoor). - `-ea-instance-size`: Size of each backdoor. - `-ea-num-iters`: Number of EA iterations for each backdoor. - `-ea-seed`: Random seed. - `-ea-output-path`: Output file with backdoors. The resulting backdoor(s) will be saved in the specified output file (by default, `backdoors.txt`).

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：