-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
international sat competition 2024 version
- Loading branch information
Showing
2,712 changed files
with
512,506 additions
and
2,354 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,4 +1,105 @@ | ||
| *.o | ||
| *.cnf | ||
| *.log | ||
| parameters.sh | ||
| outputs | ||
| inputs | ||
| painless-mcomsps | ||
| mapleCOMSPS/build/ | ||
| mapleCOMSPS/m4ri-20140914/ | ||
| painless | ||
| docs/ | ||
| doxygen/html | ||
| doxygen/latex | ||
| doxygen/markdowns | ||
| .html | ||
| *.uri | ||
| get_sat22_inputs.sh | ||
| .vscode/ | ||
| *.gdb | ||
| *.output | ||
| *.swp | ||
| *.a | ||
| *.cpp_old | ||
| *.h_old | ||
| *.ignore | ||
| *.o | ||
| hostfile | ||
| openMPI | ||
| *.out | ||
| *.pb.* | ||
|
|
||
| libs/m4ri-20140914/Makefile | ||
| libs/m4ri-20140914/config.status | ||
| libs/m4ri-20140914/libm4ri.la | ||
| libs/m4ri-20140914/libtool | ||
| libs/m4ri-20140914/m4ri/m4ri_config.h | ||
| libs/m4ri-20140914/autom4te.cache | ||
| libs/m4ri-20140914/configure~ | ||
| libs/m4ri-20140914/m4ri/config.h.in~ | ||
| libs/m4ri-20200125/Makefile | ||
| libs/m4ri-20200125/Makefile.in | ||
| libs/m4ri-20200125/aclocal.m4 | ||
| libs/m4ri-20200125/autom4te.cache/ | ||
| libs/m4ri-20200125/bench/Makefile | ||
| libs/m4ri-20200125/bench/Makefile.in | ||
| libs/m4ri-20200125/compile | ||
| libs/m4ri-20200125/config.guess | ||
| libs/m4ri-20200125/config.sub | ||
| libs/m4ri-20200125/configure | ||
| libs/m4ri-20200125/depcomp | ||
| libs/m4ri-20200125/install-sh | ||
| libs/m4ri-20200125/ltmain.sh | ||
| libs/m4ri-20200125/m4/libtool.m4 | ||
| libs/m4ri-20200125/m4/ltoptions.m4 | ||
| libs/m4ri-20200125/m4/ltsugar.m4 | ||
| libs/m4ri-20200125/m4/ltversion.m4 | ||
| libs/m4ri-20200125/m4/lt~obsolete.m4 | ||
| libs/m4ri-20200125/m4ri.pc | ||
| libs/m4ri-20200125/m4ri/brilliantrussian.lo | ||
| libs/m4ri-20200125/m4ri/config.h | ||
| libs/m4ri-20200125/m4ri/config.h.in | ||
| libs/m4ri-20200125/m4ri/debug_dump.lo | ||
| libs/m4ri-20200125/m4ri/djb.lo | ||
| libs/m4ri-20200125/m4ri/echelonform.lo | ||
| libs/m4ri-20200125/m4ri/graycode.lo | ||
| libs/m4ri-20200125/m4ri/io.lo | ||
| libs/m4ri-20200125/m4ri/m4ri_config.h | ||
| libs/m4ri-20200125/m4ri/misc.lo | ||
| libs/m4ri-20200125/m4ri/mmc.lo | ||
| libs/m4ri-20200125/m4ri/mp.lo | ||
| libs/m4ri-20200125/m4ri/mzd.lo | ||
| libs/m4ri-20200125/m4ri/mzp.lo | ||
| libs/m4ri-20200125/m4ri/ple.lo | ||
| libs/m4ri-20200125/m4ri/ple_russian.lo | ||
| libs/m4ri-20200125/m4ri/solve.lo | ||
| libs/m4ri-20200125/m4ri/stamp-h1 | ||
| libs/m4ri-20200125/m4ri/strassen.lo | ||
| libs/m4ri-20200125/m4ri/triangular.lo | ||
| libs/m4ri-20200125/m4ri/triangular_russian.lo | ||
| libs/m4ri-20200125/missing | ||
| libs/m4ri-20200125/test-driver | ||
| libs/m4ri-20200125/tests/Makefile | ||
| libs/m4ri-20200125/tests/Makefile.in | ||
| libs/m4ri-20200125/tests/.* | ||
| libs/m4ri-20200125/.libs | ||
| libs/m4ri-20200125/bench/.deps | ||
| libs/m4ri-20200125/m4ri/.deps | ||
| libs/m4ri-20200125/m4ri/.dirstamp | ||
|
|
||
| solvers/kissat_mab/build/ | ||
| solvers/kissat_mab/makefile | ||
| solvers/GASPIKISSAT/build/ | ||
| solvers/GASPIKISSAT/makefile | ||
| solvers/yalsat/cflags.h | ||
| solvers/yalsat/config.h | ||
| solvers/yalsat/makefile | ||
| solvers/yalsat/yalsat | ||
|
|
||
| solvers/mapleCOMSPS/build | ||
|
|
||
| *.csv | ||
|
|
||
| build/ | ||
| *.la | ||
| config.status | ||
| libtool |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,28 +1,48 @@ | ||
| all: | ||
| ################################################## | ||
| ### MapleCOMSPS ### | ||
| ### m4ri ### | ||
| ################################################## | ||
| if [ -d mapleCOMSPS/m4ri-20140914 ]; then : ; \ | ||
| else cd mapleCOMSPS && tar zxvf m4ri-20140914.tar.gz && \ | ||
| cd m4ri-20140914 && ./configure; fi | ||
| + $(MAKE) -C mapleCOMSPS/m4ri-20140914 | ||
| + $(MAKE) -C mapleCOMSPS | ||
| cd libs/m4ri-20200125 && autoreconf --install && ./configure --enable-thread-safe | ||
| + $(MAKE) -C libs/m4ri-20200125 | ||
|
|
||
| ################################################## | ||
| ### kissat_mab ### | ||
| ################################################## | ||
| cd solvers/kissat_mab && bash ./configure --compact | ||
| + $(MAKE) -C solvers/kissat_mab | ||
|
|
||
| ################################################## | ||
| ### PaInleSS ### | ||
| ### GASPIKISSAT ### | ||
| ################################################## | ||
| + $(MAKE) -C painless-src | ||
| mv painless-src/painless painless-mcomsps | ||
| cd solvers/GASPIKISSAT && bash ./configure --compact --quiet | ||
| + $(MAKE) -C solvers/GASPIKISSAT | ||
|
|
||
| ################################################## | ||
| ### yalsat ### | ||
| ################################################## | ||
| cd solvers/yalsat && bash ./configure.sh | ||
| + $(MAKE) -C solvers/yalsat | ||
|
|
||
| clean: | ||
| ################################################## | ||
| ### MapleCOMSPS ### | ||
| ### MapleCOMSPS ### | ||
| ################################################## | ||
| rm -rf mapleCOMSPS/m4ri-20140914 | ||
| + $(MAKE) -C mapleCOMSPS clean | ||
| + $(MAKE) -C solvers/mapleCOMSPS r | ||
|
|
||
|
|
||
| ################################################## | ||
| ### PaInleSS ### | ||
| ################################################## | ||
| + $(MAKE) -C painless-src | ||
| mv painless-src/painless painless | ||
|
|
||
| clean: | ||
| ################################################## | ||
| ### PaInleSS ### | ||
| ### Clean ### | ||
| ################################################## | ||
| + $(MAKE) clean -C solvers/kissat_mab -f makefile.in | ||
| rm -rf solvers/kissat_mab/build | ||
| + $(MAKE) clean -C solvers/GASPIKISSAT -f makefile.in | ||
| rm -rf solvers/GASPIKISSAT/build | ||
| + $(MAKE) -C solvers/mapleCOMSPS clean | ||
| + $(MAKE) clean -C painless-src | ||
| rm -f painless-mcomsps | ||
| rm -f painless |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,45 +1,93 @@ | ||
| ##### PaInleSS: A Framework for Parallel SAT Solving ##### | ||
| Painless: a Framework for Parallel SAT Solving | ||
| ============================================== | ||
|
|
||
| Authors: Ludovic LE FRIOUX, Vincent VALLADE, Souheib Baarir | ||
| * Souheib BAARIR (souheib.baarir@lip6.fr) | ||
| * Mazigh SAOUDI (mazigh.saoudi@epita.fr) | ||
|
|
||
| Contacts: Souheib.baarir@lip6.fr | ||
|
|
||
| ===== Content ===== | ||
|
|
||
| - painless-src: | ||
| Content | ||
| ------- | ||
| * painless-src/: | ||
| Contains the code of the framework. | ||
| - clauses: | ||
| * clauses/: | ||
| Contains the code to manage shared clauses. | ||
| - working: | ||
| * working/: | ||
| Code links to the worker organization. | ||
| - sharing: | ||
| * sharing/: | ||
| Code links to the learnt clause sharing management. | ||
| - solvers: | ||
| * solvers/: | ||
| Contains wrapper for the sequential solvers. | ||
| - utils: | ||
| * utils/: | ||
| Contains code for clauses management. But also useful data structures. | ||
| * preprocessors/: | ||
| Contains the imported preprocessings of [PRS](https://github.com/shaowei-cai-group/PRS-sc23/tree/PRS-sc23) and [SBVA](https://github.com/hgarrereyn/SBVA). | ||
|
|
||
| - mapleCOMSPS: | ||
| Contains the code of MapleCOMSPS from the SAT Competition 17 with some little | ||
| changes. | ||
| * solvers/: | ||
| * mapleCOMSPS/: | ||
| Contains the code of MapleCOMSPS from the SAT Competition 17 with some little changes. | ||
|
|
||
| * kissat_mab/: | ||
| Contains the code of kissat_mab. | ||
|
|
||
| * yalsat/: | ||
| Contains the code of [yalsat](https://github.com/arminbiere/yalsat). | ||
|
|
||
| ===== To compile the project ===== | ||
| * GASPIKISSAT/: | ||
| Contains the code of [GaspiKissat](https://github.com/sabrinesaouli/GASPIKISSAT). | ||
|
|
||
| - In the painless-mcomsps home directory use 'make' to compile. | ||
| To compile the project | ||
| ---------------------- | ||
| * Must install an MPI implementation, painless was tested with [OpenMpi](https://www.open-mpi.org/). | ||
| * Requires [Protobuf](https://protobuf.dev/) to be installed with its compiler and--('') shared library. | ||
|
|
||
| - In the painless-mcomsps home directory use 'make clean' to clean. | ||
| * In the main directory use 'make' to compile the code. | ||
|
|
||
| * In the main directory use 'make clean' to clean. | ||
|
|
||
| ===== To run the solvers ===== | ||
| <!-- | ||
| To run painless | ||
| --------------- | ||
| - All options have a default value except for the filename. | ||
| ```sh | ||
| nb_cpu=6 # the number of sequential solvers to instantiate | ||
| nb_nodes=3 # the number of mpi processes to launch | ||
| timeout=1000 # the timeout before giving up (in seconds) | ||
| strat=1 # 1 2 3 4 for strategies with Hordesat, 5 for Simple. 0 is the default. It is to randomize the strategy pick, can be useful with -dist. | ||
| verbose=0 # for the logs (1 for general logs) (2 for detailed logs) | ||
| gstrat=1 # 1 for AllGatherSharing, 2 for MallobSharing, and 3 for RingSharing | ||
| filename=./inputs_example/f/f2000.cnf #path to a cnf file | ||
| ``` | ||
| - Modes: | ||
| ``` sh | ||
| -str "one thread in charge of strengthening learnt clauses per sharing group" | ||
| - P-MCOMSPS-AI : | ||
| ./painless-mcomsps -c=#cpus -shr-strat=2 -shr-sleep=1500000 -lbd-limit=2 dimacs_filename | ||
| -dup "remove/promote duplicate clauses in local sharing strategy, not available in StrengtheningSharing" | ||
| - P-MCOMSPS-L2: | ||
| ./painless-mcomsps -c=#cpus -shr-strat=1 -shr-sleep=500000 -lbd-limit=2 dimacs_filename | ||
| -dist "enable distributed mode" | ||
| - P-MCOMSPS-L4: | ||
| ./painless-mcomsps -c=#cpus -shr-strat=1 -shr-sleep=500000 -lbd-limit=4 dimacs_filename | ||
| -one-sharer "use one sharer for all sharing strategies" | ||
| To use these solvers with strengthening add -strength flag and -c must be >= 2. | ||
| -simp "enable some preprocessings before launching the solvers" | ||
| ``` | ||
| * painless with kissat: | ||
| ```sh | ||
| ./painless -v=$verbose -c=$nb_cpu -solver="k" -t=$timeout -shr-strat=$strat $filename | ||
| ``` | ||
| * painless with maple: | ||
| ```sh | ||
| ./painless -v=$verbose -c=$nb_cpu -t=$timeout -shr-strat=$strat $filename | ||
| ``` | ||
| * painless-kissat with mpi each node in a separate terminal: | ||
| ```sh | ||
| mpirun -n $nb_nodes xterm -hold -e ./painless -c=$nb_cpu -solver="k" -t=$timeout -v=$verbose -shr-strat=$strat -gshr-start=$gstrat -dist $filename | ||
| ``` | ||
| * The script `scripts/launch.sh` can be used to launch a certain instance described by `parameters.sh` on multiple forumale: | ||
| ```sh | ||
| ./scripts/launch.sh ./file_with_paths_to_instances | ||
| ``` | ||
| * The file `./file_with_paths_to_instances` can be generated using the `ls` command, for example: | ||
| ```sh | ||
| ls $PWD/inputs_example/f/* > instances_f.txt | ||
| ``` | ||
| --> |
Oops, something went wrong.