title: Z3 select logic and set configuration parameters
body: <p>I am using z3 through Python bindings to find solutions for a dissection-puzzle (think <a href="https://en.wikipedia.org/wiki/Tangram" rel="nofollow noreferrer">Tangram</a>). I confess that I do not really know what I am doing and am viewing this as an interesting learning experience.</p>
  
  <p>Most of the code is about geometry, then I create a solver without specifying a logic (calling <code>z3.solver()</code>), create a load of Bool variables and add purely boolean constraints for them. There also are exactly-1-of-n- and at-most-1-of-n-constraints in the mix, created using <code>z3.PbEq()</code> and <code>z3.PbLe()</code>.</p>
  
  <p>My program works, but the problem is huge and I am doing an exhaustive search for all satisfying models so I am looking at weeks and months of processing. </p>
  
  <p>My general question is about wether I can help z3 in any way. More specifically I am asking about three areas listed below. Being ignorant as I am I have blindly experimented with parameters that seem to be related. </p>
  
  <p>I realize there are no easy answers to this. I would appreciate pointers to material or keywords to look up to continue my education on this stuff.</p>
  
  <p>1) Explicitly select a theory:</p>
  
  <p>Instead of <code>z3.solver()</code> I tried calling <code>z3.solverFor('QF_FD')</code>.</p>
  
  <p>This alone did not seem to make any difference. Is there way of finding out what theories there are, what it is actually using if I just call solver()? Where can I learn about which theory may be suitable to my problem?</p>
  
  <p>2) Try to enable parallelism:</p>
  
  <p>I noticed that my program does not exercize all the CPU-cores my machine has to offer. Instead of thinking for myself on how to parallelize it I tried to see what z3 can do.</p>
  
  <p>I set various parameters picked from the output of help(), that sounded like they might control parallelism/multithreading:</p>
  
  <pre><code>z3.set_param('parallel.enable', True)
  z3.set_param('parallel.threads.max', 32)
  z3.set_param('sat.local_search_threads', 3)
  z3.set_param('sat.threads', 3)
  </code></pre>
  
  <p>I did get different behaviour from this. The program did execute in multiple threads and warmed up my machine considerably when compared with the other runs. But unfortunately instead of the steady trickle of satisfying models I got of the default settings I did not get any even after days of processing.</p>
  
  <p>Where - other than the z3 source - Can I learn about the ways this works and maybe structure my problem such that it can be better parallelized?</p>
  
  <p>3) Other obscure parameters.</p>
  
  <p>I also played with these:</p>
  
  <pre><code>z3.set_param('sat.lookahead_simplify', True) 
  z3.set_param('sat.acce', True)  
  z3.set_param('sat.pb.solver', 'solver')
  </code></pre>
  
  <p>But nothing noticeably changed. Are there explanations of what these mean at a level between the one-liner from help(), and the actual code?</p>