About STP Aborted

[zfx-code]

Dear Author:
When I run stp like "./stp test.smt2 > test.out --threads=4".
It aborted and returned the information:
"""
stp: /root/stp/deps/cms/src/watched.h:106: CMSat::Watched::Watched(CMSat::Lit, bool, int32_t): Assertion `ID < 1
LL<< (EFFECTIVELY_USEABLE_BITS-2) && "Please compile with -DLARGEMEM"' failed.
Aborted
"""
Does this error mean that there is not enough memory?

Looking forward to your reply.
Best wishes to you!

[TrevorHansen]

My understanding is that by default Cryptominisat can't use all your computer's RAM, beyond some limit. Compiling it with -DLARGEMEM substantially increases the amount of RAM it can use. Here's some background:
#356 (comment)

My guess is that your computer has enough memory, but Cryptominisat as it's compiled can't use it all.

[zfx-code]

Thanks for your reply, I will try this solution.

Best wishes to you!

[zfx-code]

My understanding is that by default Cryptominisat can't use all your computer's RAM, beyond some limit. Compiling it with -DLARGEMEM substantially increases the amount of RAM it can use. Here's some background: #356 (comment)

My guess is that your computer has enough memory, but Cryptominisat as it's compiled can't use it all.

Hello
When I tried to Compiling with -DLARGEMEM, I used "cmake -DLARGEMEM=ON .."
It returned:
"""
-- Generating done
CMake Warning:
Manually-specified variables were not used by the project:

LARGEMEM

"""
It seems that LARGEMEM is invalid(STP After running for a while still Aborted).
Maybe my compiling method has problems.

By the way, I was able to compile it before, but now it errors....
So maybe you can give me some help?
Thank you.

[aytey]

You need to build CryptoMiniSat with -DLARGEMEM:BOOL=ON when you call its CMake. Once you've build CMS with -DLARGEMEM:BOOL=ON, you then build STP "normally" (but linking against your large-mem-enabled CMS).

[zfx-code]

You need to build CryptoMiniSat with -DLARGEMEM:BOOL=ON when you call its CMake. Once you've build CMS with -DLARGEMEM:BOOL=ON, you then build STP "normally" (but linking against your large-mem-enabled CMS).

Thank you very much!
I build CryptoMiniSat with -DLARGEMEM:BOOL=ON successfully(Maybe), because I looked the "CMakeCache.txt".
It shows:
"""
//Allow memory usage to grow to Terabyte values -- uses 64b offsets.
// Slower, but allows the solver to run for much longer.
LARGEMEM:BOOL=ON
"""

I think it's OK(CMS) and then build STP.
Everything's fine this time. I don't think it'll ever be "Aborted".

Best wishes to you!

[zfx-code]

I'm sorry to bother you again, when I ran a few days later a new problem arose:
"""
stp: /root/cryptominisat/src/watchalgos.h:160: CMSat::Watched& CMSat::findWatchedOfBin(CMSat::watch_array&, CMSa
t::Lit, CMSat::Lit, bool, int32_t): Assertion `false' failed.
Aborted
"""
Does this mean really out of memory, but I observed that the memory was sufficient.
Maybe something bug when I run many threads, this running time is 24 hours in 5 threads.

Looking forward to your reply, thank you!

[TrevorHansen]

hi @msoos, do you know what might cause this error?

stp: /root/cryptominisat/src/watchalgos.h:160: CMSat::Watched& CMSat::findWatchedOfBin(CMSat::watch_array&, CMSa
t::Lit, CMSat::Lit, bool, int32_t): Assertion `false' failed.
Aborted

[zfx-code]

By the way, may someone knows if can convert SMT model to SAT model?
In SMT model only use BITVECTOR, +(BVPLUS) and <(BVLT).
The problem likes find sum(cost) < target, cost and target are Integer(ARRAY BITVECTOR), others variables are in {0, 1}.
I mean STP solves some problems based on SAT Solver.
So can convert some special SMT problem to CNF format, then use SAT Solver solve directly?

[TrevorHansen]

By the way, may someone knows if can convert SMT model to SAT model? In SMT model only use BITVECTOR, +(BVPLUS) and <(BVLT). The problem likes find sum(cost) < target, cost and target are Integer(ARRAY BITVECTOR), others variables are in {0, 1}. I mean STP solves some problems based on SAT Solver. So can convert some special SMT problem to CNF format, then use SAT Solver solve directly?

Yes, If you use the

 --exit-after-CNF --ackermanize --output-CNF 

you'll get a CNF saved into that folder that you can send to the a SAT solver. Currently we don't have any way of mapping the model that the SAT solver gives you back into a bit-vector model though.

[zfx-code]

By the way, may someone knows if can convert SMT model to SAT model? In SMT model only use BITVECTOR, +(BVPLUS) and <(BVLT). The problem likes find sum(cost) < target, cost and target are Integer(ARRAY BITVECTOR), others variables are in {0, 1}. I mean STP solves some problems based on SAT Solver. So can convert some special SMT problem to CNF format, then use SAT Solver solve directly?

Yes, If you use the

 --exit-after-CNF --ackermanize --output-CNF 

you'll get a CNF saved into that folder that you can send to the a SAT solver. Currently we don't have any way of mapping the model that the SAT solver gives you back into a bit-vector model though.

Thanks for your reply.
If I understand you correctly, do you mean that we can find an equivalent SAT model.
SMT => SAT(.cvc or .smt2 => .cnf)
However, the result of solve SAT model can't map back SMT model yet.
It could be done in theory, but it hasn't been done in practice, has it?
What's a pity, it seems that solve the SMT model consumes more memory, and solving the SAT model has rarely been out of memory(Aborted or Killed).

[aytey]

However, the result of solve SAT model can't map back SMT model yet.

So STP does this internally (e.g., that's how it is able to generate a model on the SMT-level from a solution to the SAT problem), but once you've generated an eager SAT instance to a CNF file, STP has no method to read in that SAT output back in to generate you an SMT model.

Also, if you're using the theory of arrays, it won't be possible to generate a purely eager CNF file, as solving the theory of arrays is an iterative process (i.e., it calls the SAT solver in a refinement-style loop).

and solving the SAT model has rarely been out of memory(Aborted or Killed).

I don't yet know this is a memory issue; are you able to share your input to STP so we can see what the cause of this issue could be?

[zfx-code]

However, the result of solve SAT model can't map back SMT model yet.

So STP does this internally (e.g., that's how it is able to generate a model on the SMT-level from a solution to the SAT problem), but once you've generated an eager SAT instance to a CNF file, STP has no method to read in that SAT output back in to generate you an SMT model.

Also, if you're using the theory of arrays, it won't be possible to generate a purely eager CNF file, as solving the theory of arrays is an iterative process (i.e., it calls the SAT solver in a refinement-style loop).

and solving the SAT model has rarely been out of memory(Aborted or Killed).

I don't yet know this is a memory issue; are you able to share your input to STP so we can see what the cause of this issue could be?

test.zip
I use BitVec 1, BitVec 8 and (Array (_ BitVec 7) (_ BitVec 8) ).
Run cmd is

stp test.smt2 > test.out --threads=5

Maybe this instance is hard to solve(24 hour in 5 threads), some easy instances not Aborted.
I noticed that I used the "Array Bit Vec", but I can avoid doing that.
From (set-logic QF_ABV) to (set-logic QF_BV).

[aytey]

Maybe this instance is hard to solve(24 hour in 5 threads), some easy instances not Aborted.

Ah, okay, so it could be a memory issue then, if things take too long.

How does your system look before it dies? Close to out of memory?

[zfx-code]

Maybe this instance is hard to solve(24 hour in 5 threads), some easy instances not Aborted.

Ah, okay, so it could be a memory issue then, if things take too long.

How does your system look before it dies? Close to out of memory?

The memory usage was not very high(memory is 32G and usage < 50%).
Suddenly it's dead.

[TrevorHansen]

Also, if you're using the theory of arrays, it won't be possible to generate a purely eager CNF file, as solving the theory of arrays is an iterative process (i.e., it calls the SAT solver in a refinement-style loop).

A quick clarification about this. The --ackermanize flag should eagerly encode array problems. It just might make the CNF encoding very large. Hey, can't have it all..