search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
335 stars 62 forks source link

long working time on simple constraint #121

Closed Ketchynez closed 2 years ago

Ketchynez commented 4 years ago

Hi!

Found a constraint, which is rather simple, but the operating time is noticeably longer than on cvc4 and z3 (unlike other bitvector scenarious where boolector was always faster), looks kinda weird. Timings: Z3: 0.038 sec CVC4: 0.020 sec Boolector: 0.360 sec

Here is the constraint

(declare-const P1_PHASE (_ BitVec 10))
(assert 
   (and
     (or
       (= P1_PHASE #b0001110111)
       (= P1_PHASE #b0100111001)
       (= P1_PHASE #b0110110101)
       (= P1_PHASE #b0001100111)
       (= P1_PHASE #b0010000001)
       (= P1_PHASE #b0010100111)
       (= P1_PHASE #b0000110101)
       (= P1_PHASE #b0000100101)
       (= P1_PHASE #b0101111011)
       (= P1_PHASE #b0111000111)
       (= P1_PHASE #b0000110001)
       (= P1_PHASE #b0011010101)
       (= P1_PHASE #b0100101001)
       (= P1_PHASE #b0011001001)
       (= P1_PHASE #b0110001011)
       (= P1_PHASE #b0111100101)
       (= P1_PHASE #b0010101011)
       (= P1_PHASE #b0110011001)
       (= P1_PHASE #b0111100011)
       (= P1_PHASE #b0110110001)
       (= P1_PHASE #b0000001001)
       (= P1_PHASE #b0101100001)
       (= P1_PHASE #b0100010011)
       (= P1_PHASE #b0100101011)
       (= P1_PHASE #b0110010101)
       (= P1_PHASE #b0110111011)
       (= P1_PHASE #b0011111011)
       (= P1_PHASE #b0100000011)
       (= P1_PHASE #b0110011101)
       (= P1_PHASE #b0011110011)
       (= P1_PHASE #b0011111111)
       (= P1_PHASE #b0010011111)
       (= P1_PHASE #b0011010001)
       (= P1_PHASE #b0001101111)
       (= P1_PHASE #b0011101101)
       (= P1_PHASE #b0101101011)
       (= P1_PHASE #b0000101001)
       (= P1_PHASE #b0011100001)
       (= P1_PHASE #b0100001101)
       (= P1_PHASE #b0101000101)
       (= P1_PHASE #b0100100001)
       (= P1_PHASE #b0101101111)
       (= P1_PHASE #b0001000011)
       (= P1_PHASE #b0001101011)
       (= P1_PHASE #b0101010111)
       (= P1_PHASE #b0110000001)
       (= P1_PHASE #b0001010011)
       (= P1_PHASE #b0100101111)
       (= P1_PHASE #b0101110001)
       (= P1_PHASE #b0001000001)
       (= P1_PHASE #b0001101001)
       (= P1_PHASE #b0111100111)
       (= P1_PHASE #b0000010001)
       (= P1_PHASE #b0100000111)
       (= P1_PHASE #b0100001011)
       (= P1_PHASE #b0000111101)
       (= P1_PHASE #b0010011001)
       (= P1_PHASE #b0100010101)
       (= P1_PHASE #b0101001001)
       (= P1_PHASE #b0110111111)
       (= P1_PHASE #b0101000111)
       (= P1_PHASE #b0111110001)
       (= P1_PHASE #b0100100111)
       (= P1_PHASE #b0010010011)
       (= P1_PHASE #b0110110011)
       (= P1_PHASE #b0101001111)
       (= P1_PHASE #b0110100111)
       (= P1_PHASE #b0111101011)
       (= P1_PHASE #b0001100011)
       (= P1_PHASE #b0000011111)
       (= P1_PHASE #b0100011011)
       (= P1_PHASE #b0101001011)
       (= P1_PHASE #b0000110111)
       (= P1_PHASE #b0011111001)
       (= P1_PHASE #b0001111111)
       (= P1_PHASE #b0010100011)
       (= P1_PHASE #b0011001011)
       (= P1_PHASE #b0010101101)
       (= P1_PHASE #b0101101101)
       (= P1_PHASE #b0111010101)
       (= P1_PHASE #b0011101011)
       (= P1_PHASE #b0110010001)
       (= P1_PHASE #b0101011001)
       (= P1_PHASE #b0100111011)
       (= P1_PHASE #b0110011111)
       (= P1_PHASE #b0110001001)
       (= P1_PHASE #b0110001101)
       (= P1_PHASE #b0111101001)
       (= P1_PHASE #b0110000011)
       (= P1_PHASE #b0000100001)
       (= P1_PHASE #b0000101011)
       (= P1_PHASE #b0111011111)
       (= P1_PHASE #b0100000001)
       (= P1_PHASE #b0010001011)
       (= P1_PHASE #b0100110101)
       (= P1_PHASE #b0001000111)
       (= P1_PHASE #b0011011001)
       (= P1_PHASE #b0101000011)
       (= P1_PHASE #b0111101101)
       (= P1_PHASE #b0010011011)
       (= P1_PHASE #b0001011011)
       (= P1_PHASE #b0010001101)
       (= P1_PHASE #b0111001101)
       (= P1_PHASE #b0011110111)
       (= P1_PHASE #b0010111101)
       (= P1_PHASE #b0110000111)
       (= P1_PHASE #b0100110011)
       (= P1_PHASE #b0010011101)
       (= P1_PHASE #b0110100011)
       (= P1_PHASE #b0100101101)
       (= P1_PHASE #b0111111001)
       (= P1_PHASE #b0100111101)
       (= P1_PHASE #b0101100011)
       (= P1_PHASE #b0010100001)
       (= P1_PHASE #b0100011001)
       (= P1_PHASE #b0110001111)
       (= P1_PHASE #b0101010001)
       (= P1_PHASE #b0000011101)
       (= P1_PHASE #b0010111001)
       (= P1_PHASE #b0000000111)
       (= P1_PHASE #b0010101111)
       (= P1_PHASE #b0101110111)
       (= P1_PHASE #b0111010011)
       (= P1_PHASE #b0101100111)
       (= P1_PHASE #b0000001101)
       (= P1_PHASE #b0100011101)
       (= P1_PHASE #b0100010001)
       (= P1_PHASE #b0100001001)
       (= P1_PHASE #b0110011011)
       (= P1_PHASE #b0101000001)
       (= P1_PHASE #b0000000101)
       (= P1_PHASE #b0010010001)
       (= P1_PHASE #b0100100011)
       (= P1_PHASE #b0010001001)
       (= P1_PHASE #b0000111011)
       (= P1_PHASE #b0100100101)
       (= P1_PHASE #b0111000011)
       (= P1_PHASE #b0011101111)
       (= P1_PHASE #b0100000101)
       (= P1_PHASE #b0101110011)
       (= P1_PHASE #b0010000011)
       (= P1_PHASE #b0110010111)
       (= P1_PHASE #b0001110011)
       (= P1_PHASE #b0000010011)
       (= P1_PHASE #b0010110101)
       (= P1_PHASE #b0011000111)
       (= P1_PHASE #b0100111111)
       (= P1_PHASE #b0111000101)
       (= P1_PHASE #b0011000101)
       (= P1_PHASE #b0011101001)
       (= P1_PHASE #b0011110001)
       (= P1_PHASE #b0010010111)
       (= P1_PHASE #b0001001111)
       (= P1_PHASE #b0111000001)
       (= P1_PHASE #b0011111101)
       (= P1_PHASE #b0010010101)
       (= P1_PHASE #b0100010111)
       (= P1_PHASE #b0000010101)
       (= P1_PHASE #b0111011101)
       (= P1_PHASE #b0010000111)
       (= P1_PHASE #b0001110101)
       (= P1_PHASE #b0011011101)
       (= P1_PHASE #b0010100101)
       (= P1_PHASE #b0110010011)
       (= P1_PHASE #b0000101101)
       (= P1_PHASE #b0110101111)
       (= P1_PHASE #b0001010111)
       (= P1_PHASE #b0001011101)
       (= P1_PHASE #b0110100001)
       (= P1_PHASE #b0110111001)
       (= P1_PHASE #b0101110101)
       (= P1_PHASE #b0111110111)
       (= P1_PHASE #b0001001011)
       (= P1_PHASE #b0011011011)
       (= P1_PHASE #b0010110001)
       (= P1_PHASE #b0110110111)
       (= P1_PHASE #b0011000011)
       (= P1_PHASE #b0001001101)
       (= P1_PHASE #b0011000001)
       (= P1_PHASE #b0001110001)
       (= P1_PHASE #b0101101001)
       (= P1_PHASE #b0001001001)
       (= P1_PHASE #b0000001111)
       (= P1_PHASE #b0111110101)
       (= P1_PHASE #b1000000011)
       (= P1_PHASE #b0111111101)
       (= P1_PHASE #b0110000101)
       (= P1_PHASE #b0011110101)
       (= P1_PHASE #b0000011001)
       (= P1_PHASE #b0001011001)
       (= P1_PHASE #b0111001011)
       (= P1_PHASE #b0000011011)
       (= P1_PHASE #b0110101011)
       (= P1_PHASE #b0101100101)
       (= P1_PHASE #b0000001011)
       (= P1_PHASE #b0001011111)
       (= P1_PHASE #b0011010011)
       (= P1_PHASE #b0010110111)
       (= P1_PHASE #b0111110011)
       (= P1_PHASE #b0110100101)
       (= P1_PHASE #b0001010001)
       (= P1_PHASE #b0111100001)
       (= P1_PHASE #b0010000101)
       (= P1_PHASE #b0100011111)
       (= P1_PHASE #b0101111111)
       (= P1_PHASE #b0010101001)
       (= P1_PHASE #b0000111001)
       (= P1_PHASE #b0001100001)
       (= P1_PHASE #b0110101001)
       (= P1_PHASE #b0000111111)
       (= P1_PHASE #b1000000001)
       (= P1_PHASE #b0101011011)
       (= P1_PHASE #b0101010101)
       (= P1_PHASE #b0100110001)
       (= P1_PHASE #b0001100101)
       (= P1_PHASE #b0111010111)
       (= P1_PHASE #b0111011001)
       (= P1_PHASE #b0111011011)
       (= P1_PHASE #b0001111001)
       (= P1_PHASE #b0011100111)
       (= P1_PHASE #b0101010011)
       (= P1_PHASE #b0101111101)
       (= P1_PHASE #b0111001001)
       (= P1_PHASE #b0111010001)
       (= P1_PHASE #b0111111011)
       (= P1_PHASE #b0110111101)
       (= P1_PHASE #b0011100011)
       (= P1_PHASE #b0101001101)
       (= P1_PHASE #b0001111011)
       (= P1_PHASE #b0001000101)
       (= P1_PHASE #b0001101101)
       (= P1_PHASE #b0100110111)
       (= P1_PHASE #b0110101101)
       (= P1_PHASE #b0010001111)
       (= P1_PHASE #b0011001111)
       (= P1_PHASE #b0011100101)
       (= P1_PHASE #b0100001111)
       (= P1_PHASE #b0000100011)
       (= P1_PHASE #b0101111001)
       (= P1_PHASE #b0011011111)
       (= P1_PHASE #b0111111111)
       (= P1_PHASE #b0011010111)
       (= P1_PHASE #b0001010101)
       (= P1_PHASE #b0101011101)
       (= P1_PHASE #b0101011111)
       (= P1_PHASE #b0111101111)
       (= P1_PHASE #b0000010111)
       (= P1_PHASE #b0000100111)
       (= P1_PHASE #b0111001111)
       (= P1_PHASE #b0010111111)
       (= P1_PHASE #b0000110011)
       (= P1_PHASE #b0000101111)
       (= P1_PHASE #b0010111011)
       (= P1_PHASE #b0011001101)
       (= P1_PHASE #b0001111101)
       (= P1_PHASE #b0010110011)
       (= P1_PHASE #b1000000101)
       (= P1_PHASE #b1000000100))
     (not
       (bvult P1_PHASE #b0000000000))
     (or
       (bvult P1_PHASE #b1000000101)
       (= P1_PHASE #b1000000101))))
(check-sat)
(get-value (
  P1_PHASE
  ))
(get-model)
(exit)
aytey commented 4 years ago

@Ketchynez how did you configure boolector? Can you provide any more information on this?

I just ran this with the latest master and with --only-cadical (passed to ./configure.sh):

[avj@tempvm build]$ ./bin/boolector --version
3.2.1
[avj@tempvm build]$ ./bin/boolector --copyright
This software is
Copyright (c) 2007-2009 Robert Brummayer
Copyright (c) 2007-2018 Armin Biere
Copyright (c) 2012-2019 Aina Niemetz, Mathias Preiner

This software is linked against CaDiCaL
Copyright (c) 2016-2019 Armin Biere
[avj@tempvm build]$ /usr/bin/time -vvv ./bin/boolector -m ../test.smt2
sat
((P1_PHASE #b0001110111))
(model
  (define-fun P1_PHASE () (_ BitVec 10) #b0001110111)
)
(model
  (define-fun P1_PHASE () (_ BitVec 10) #b0001110111)
)
Command exited with non-zero status 10
    Command being timed: "./bin/boolector -m ../test.smt2"
    User time (seconds): 0.00
    System time (seconds): 0.00
    Percent of CPU this job got: 50%
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.00
    Average shared text size (kbytes): 0
    Average unshared data size (kbytes): 0
    Average stack size (kbytes): 0
    Average total size (kbytes): 0
    Maximum resident set size (kbytes): 3552
    Average resident set size (kbytes): 0
    Major (requiring I/O) page faults: 0
    Minor (reclaiming a frame) page faults: 322
    Voluntary context switches: 1
    Involuntary context switches: 0
    Swaps: 0
    File system inputs: 0
    File system outputs: 0
    Socket messages sent: 0
    Socket messages received: 0
    Signals delivered: 0
    Page size (bytes): 4096
    Exit status: 10
aytey commented 4 years ago

Okay, so with all the solvers enabled:

[avj@tempvm build]$ for i in cadical cms lingeling minisat picosat; do echo $i; /usr/bin/time -vvv ./bin/boolector -SE $i -m ../test.smt2 |& grep "wall"; done
cadical
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.00
cms
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.00
lingeling
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.26
minisat
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.01
picosat
    Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.00

So I guess you're doing it with Lingeling?