domschrei / mallob Goto Github PK
View Code? Open in Web Editor NEWMalleable Load Balancer. Massively Parallel Logic Backend. Award-winning SAT solving for the cloud.
License: GNU Lesser General Public License v3.0
Malleable Load Balancer. Massively Parallel Logic Backend. Award-winning SAT solving for the cloud.
License: GNU Lesser General Public License v3.0
/usr/bin/ld: CMakeFiles/mallob_sat_process.dir/src/app/sat/solvers/cadical.cpp.o: in function `Cadical::solve(unsigned long, int const*)':
/mallob/src/app/sat/solvers/cadical.cpp:177: undefined reference to `CaDiCaL::Solver::flush_proof_trace(bool)'
/usr/bin/ld: /mallob/src/app/sat/solvers/cadical.cpp:178: undefined reference to `CaDiCaL::Solver::close_proof_trace(bool)'
collect2: error: ld returned 1 exit status
master branch, try to build a docker image using docker/leader/Dockerfile but get the errors above.
could anyone be kind to help me?
I am trying to run a mono job using mallob using the following command:
./mallob -mono-app=sat -mono=/some/path/myproblem.cnf
but i keep getting this execl return errno 2 error which seems to imply that mallob is unable to find my cnf file?
Any idea where i could start debugging this
[1] -np 1 -t=1 -mono=instances/r3sat_300.cnf -satsolver=llck -appmode=fork -assertresult=SAT
[mpiexec@challenger] match_arg (utils/args/args.c:163): unrecognized argument oversubscribe
[mpiexec@challenger] HYDU_parse_array (utils/args/args.c:178): argument matching returned error
[mpiexec@challenger] parse_args (ui/mpich/utils.c:1642): error parsing input array
[mpiexec@challenger] HYD_uii_mpx_get_parameters (ui/mpich/utils.c:1694): unable to parse user arguments
[mpiexec@challenger] main (ui/mpich/mpiexec.c:148): error parsing parameters
I think the problem is related to the fact that the "oversubscribe" option is unsupported in my version of mpirun (3.3.2)
It can be easily fixed by removing the "--oversubscribe" option in the "run()" function in scripts/run/systest_commons.sh but I don't know if you require a specific version of mpi for some reason.
Thank you.
Regards,
Marco
Hi dom,
again, congrats to your great results in 2021 sat race ;) I'm trying to build mallob on mac os for docker. I do docker build .
in the root folder, and at first I get the following error:
...
=> CACHED [builder 8/9] RUN mkdir build 0.0s
=> CACHED [builder 9/9] RUN cd build && cmake -DCMAKE_BUILD_TYPE=RELEASE 0.0s
=> CACHED [mallob_liaison 2/8] COPY --from=builder build/mallob mallob 0.0s
=> CACHED [mallob_liaison 3/8] COPY --from=builder build/mallob_sat_proc 0.0s
=> CACHED [mallob_liaison 4/8] RUN chmod 755 mallob 0.0s
=> CACHED [mallob_liaison 5/8] RUN chmod 755 mallob_sat_process 0.0s
=> CACHED [mallob_liaison 6/8] ADD mpi-run-aws.sh supervised-scripts/mpi 0.0s
=> CACHED [mallob_liaison 7/8] RUN chmod 755 supervised-scripts/mpi-run. 0.0s
=> ERROR [mallob_liaison 8/8] ADD test.cnf test.cnf 0.0s
------
> [mallob_liaison 8/8] ADD test.cnf test.cnf:
------
failed to compute cache key: "/test.cnf" not found: not found
After adding a random test.cnf
file, the next reads
...
=> [builder 5/9] ADD CMakeLists.txt . 0.0s
=> [builder 6/9] RUN ls -lt 0.2s
=> ERROR [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh 0.8s
------
> [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh && cd ..:
#15 0.311 Cloning into 'mergesat'...
#15 0.721 Host key verification failed.
#15 0.722 fatal: Could not read from remote repository.
#15 0.722
#15 0.722 Please make sure you have the correct access rights
#15 0.722 and the repository exists.
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh && cd ..]: exit code: 128
Tried to workaround this by manually cloning mergesat and commenting out all git-related commands in fetch_and_build_sat_solvers.sh
But then the build fails while compiling minisat:
...
=> [builder 5/9] ADD CMakeLists.txt . 0.0s
=> [builder 6/9] RUN ls -lt 0.2s
=> ERROR [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh 5.7s
------
> [builder 7/9] RUN cd lib && bash fetch_and_build_sat_solvers.sh && cd ..:
#15 0.159 sed: can't read mtl/*.cc: No such file or directory
#15 0.160 sed: can't read mtl/*.cc: No such file or directory
#15 0.161 sed: can't read mtl/*.cc: No such file or directory
#15 0.161 sed: can't read mtl/*.cc: No such file or directory
#15 0.225 Compiling: build/release/minisat/simp/Main.o
#15 0.226 Compiling: build/release/minisat/simp/ipasir.o
#15 0.226 Compiling: build/release/minisat/core/Solver.o
#15 0.226 Compiling: build/release/minisat/simp/SimpSolver.o
#15 0.499 minisat/simp/Main.cc: In function 'int main(int, char**)':
#15 0.499 minisat/simp/Main.cc:127:27: error: '_FPU_EXTENDED' was not declared in this scope
#15 0.499 127 | newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 0.499 | ^~~~~~~~~~~~~
#15 0.502 minisat/simp/Main.cc:127:44: error: '_FPU_DOUBLE' was not declared in this scope
#15 0.502 127 | newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
#15 0.502 | ^~~~~~~~~~~
#15 0.592 At global scope:
#15 0.592 cc1plus: warning: unrecognized command line option '-Wno-unknown-warning-option'
#15 0.603 make: *** [Makefile:148: build/release/minisat/simp/Main.o] Error 1
#15 0.603 make: *** Waiting for unfinished jobs....
------
executor failed running [/bin/sh -c cd lib && bash fetch_and_build_sat_solvers.sh && cd ..]: exit code: 2
I'm really not sure, weather my workarounds are legal, maybe there is a proper way of getting docker build .
to work?
https://github.com/domschrei/mallob/blob/master/lib/fetch_solvers.sh#L54
https://github.com/domschrei/mallob/blob/master/lib/fetch_solvers.sh#L67
those two commits are missing in the original CaDiCaL and Kissat project.
If we just checkout the master branch, there are some compilation errors, like
/mallob/src/app/sat/execution/../solvers/cadical_clause_export.hpp:39:14: error: 'void CadicalClauseExport::append_literal(int)' marked 'override', but does not override
39 | void append_literal(int lit) override {
| ^~~~~~~~~~~~~~
/mallob/src/app/sat/execution/../solvers/cadical_clause_export.hpp:45:14: error: 'void CadicalClauseExport::publish_clause(uint64_t, int)' marked 'override', but does not override
45 | void publish_clause (uint64_t id, int glue) override {
| ^~~~~~~~~~~~~~
Could anyone be kind to help me with this problem?
Running 37f5bb5
As soon as I introduce a job, the following happens:
0.388 0 Program options: -0o=0 -J=0 -T=0 -ajpc=0 -aold=0 -appmode=fork -ba=4 -c=1 -cbbs=1500 -cbdf=0.9 -cfhl=0 -cg=1 -ch=0 -chaf=5 -checksums=0 -chstms=60 -colors=0 -delaymonkey=0 -derandomize=1 -evu=0 -fapii=0 -fhlbd=9999999 -filelog=1 -fslbd=9999999 -g=0 -h=0 -hbbfs=10 -hmcl=30 -hubfs=9999999 -huca=0 -icpr=0 -ihlbd=9999999 -islbd=9999999 -isp=0 -jc=4 -jcl=0 -jcup=0 -jjp=1 -jwl=0 -l=1 -latencymonkey=0 -mbfsd=4 -mbt=1000000 -md=0 -mid=0 -mlbdps=8 -mmpi=0 -p=0.1 -phasediv=1 -q=0 -r=bisec -rto=0 -s=1 -satsolver=L -shufshcls=0 -sleep=100 -slpp=0 -smcl=30 -t=1 -v=2 -wam=60000 -warmup=0 -wr=0 -yield=0
0.320 63 API operational at .api/jobs.0/
1.122 63 sysstate entered=0 parsed=0 scheduled=0 processed=0
1.192 0 sysstate busyratio=0.000 jobs=0 globmem=0.00GB newreqs=0 hops=0
2.122 63 sysstate entered=0 parsed=0 scheduled=0 processed=0
2.192 0 sysstate busyratio=0.000 jobs=0 globmem=0.00GB newreqs=0 hops=0
3.123 63 sysstate entered=0 parsed=0 scheduled=0 processed=0
3.193 0 sysstate busyratio=0.000 jobs=0 globmem=0.00GB newreqs=0 hops=0
3.820 63 Introducing job #1 rev. 0 : r.#1:0 rev. 0 <- [63] born=3.820 hops=0 epoch=-1 => [0]
mallob: /home/solomon/mallob/mallob/src/app/job.hpp:230: int Job::getRevision() const: Assertion `hasDescription()' failed.
3.891 0 Caught signal 6
4.123 63 sysstate entered=1 parsed=1 scheduled=1 processed=0
4.911 0 [ERROR] pid=134123 tid=134344 signal=6
--------------------------------------------------------------------------
Primary job terminated normally, but 1 process returned
a non-zero exit code. Per user-direction, the job has been aborted.
--------------------------------------------------------------------------
Hi Dom and congrats for your great SAT Race 2020 results ;)
I'm trying to use mallob for testing on a single node in mono-mode on a single instance using mpirun -np 1 build/mallob -mono=../myhardsatproblem.cnf
and I get this error message. Not sure this is a real issue, but maybe a missing hint in how to run mallob.
--------------------------------------------------------------------------
[[47230,1],0]: A high-performance Open MPI point-to-point messaging module
was unable to find any relevant network interfaces:
Module: OpenFabrics (openib)
Host: v2201911108090102223
Another transport will be used instead, although this may result in
lower performance.
NOTE: You can disable this warning by setting the MCA parameter
btl_base_warn_component_unused to 0.
--------------------------------------------------------------------------
c 0.124 0 Program options: T=0, appmode=fork, ba=4, bm=ed, c=0, cbbs=1500, cbdf=1.0, cfhl=0, cpuh-per-instance=0, g=0.0, icpr=0.8, jc=0, l=1.0, lbc=0, log=., mcl=0, md=0, mono=/home/cwahle/mark8.cnf, p=0.01, r=bisec, rto=0, s=1.0, s2f, satsolver=1, sleep=100, t=2, td=0.01, time-per-instance=0, v=2
[v2201911108090102223:10355] *** Process received signal ***
[v2201911108090102223:10355] Signal: Floating point exception (8)
[v2201911108090102223:10355] Signal code: Integer divide-by-zero (1)
[v2201911108090102223:10355] Failing at address: 0x56243c544d05
[v2201911108090102223:10355] [ 0] /lib/x86_64-linux-gnu/libpthread.so.0(+0x12890)[0x7fa8b3d33890]
[v2201911108090102223:10355] [ 1] build/mallob(_ZN19EventDrivenBalancer13getChildRanksEb+0xd9)[0x56243c544d05]
[v2201911108090102223:10355] [ 2] build/mallob(_ZN19EventDrivenBalancerC1ERP19ompi_communicator_tR10Parameters+0x142)[0x56243c5439fe]
[v2201911108090102223:10355] [ 3] build/mallob(_ZN11JobDatabaseC1ER10ParametersRP19ompi_communicator_t+0x3b6)[0x56243c51a2d0]
[v2201911108090102223:10355] [ 4] build/mallob(_ZN6WorkerC1EP19ompi_communicator_tR10ParametersRKSt3setIiSt4lessIiESaIiEE+0x8a)[0x56243c4f471c]
[v2201911108090102223:10355] [ 5] build/mallob(_Z19doWorkerNodeProgramRP19ompi_communicator_tR10ParametersRKSt3setIiSt4lessIiESaIiEE+0x57)[0x56243c4eea5c]
[v2201911108090102223:10355] [ 6] build/mallob(main+0x75b)[0x56243c4ef222]
[v2201911108090102223:10355] [ 7] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7)[0x7fa8b28feb97]
[v2201911108090102223:10355] [ 8] build/mallob(_start+0x2a)[0x56243c4ee71a]
[v2201911108090102223:10355] *** End of error message ***
README (Building) gets the name wrong?
( cd lib && bash fetch_and_build_sat_solvers.sh )
Does mallob support finding multiple answers for a CNF problem? I tried using -s2f to write the solutions to a file but i am only getting one solution. Is there another option to toggle to get multiple solutions?
I'm trying to build mallob using Docker on Mac OS Sonoma 14.1.2 on a Macbook Pro with an M1 Max, and it fails immediately with the following error:
❯ cd docker/leader
❯ docker build -t mallob:leader ../.. -f ./Dockerfile
[+] Building 1.4s (3/3) FINISHED docker:desktop-linux
=> [internal] load build definition from Dockerfile 0.0s
=> => transferring dockerfile: 3.75kB 0.0s
=> [internal] load .dockerignore 0.0s
=> => transferring context: 2B 0.0s
=> ERROR [internal] load metadata for docker.io/library/satcomp-base:leader 1.3s
------
> [internal] load metadata for docker.io/library/satcomp-base:leader:
------
Dockerfile:47
--------------------
45 |
46 | ################### Extract Mallob in run stage
47 | >>> FROM satcomp-base:leader AS mallob_liaison
48 | RUN whoami
49 | USER root
--------------------
ERROR: failed to solve: satcomp-base:leader: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed
Do you have any recommendations for pulling satcomp-base? I'm new to Docker, so maybe there's something obvious I'm missing.
Hi,
it would be great to have Mallob in a .deb package so that it can be easily installed. This could also be helpful for dependencies (I'm thinking for example OpenMPI instead of Mpich)
Thank you.
Regards,
Marco
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.