I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory. Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to w...

I'm working on a streaming rules engine, and some of my customers have a few hundred rules they'd like to evaluate on every event that arrives at the system. The rules are pure (i.e. non-side-effec...

In SAT solving by conflict-driven clause learning, each time a solver detects that a candidate set of variable assignments leads to a conflict, it must look at the causes of the conflict, derive a ...

I need to find all triples of 16-bit numbers (x, y, z) (well, actually only bits which perfectly match up in different triples with bits on same positions), such that y | x = 0x49ab (y >> 2) ...

I have a list of Employee and a list of Mission. Each mission have a start time and a duration. In the cp model (Google CpSat, from or-tools package), I defined shifts = Dictionary<(int,int),Int...

Recently, I started to study formal verification techniques. In literature, model checker and solver are used somehow interchangeably. But, how model checker and solver are connected with each othe...

I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,..,xN. I want to express the constraint that exactly K out of N of them should be true. How can I do ...

I'm trying to solve a big CNF formula using a SAT solver. The formula (in DIMACS format) has 4,697,898,048 = 2^32 + 402,930,752 clauses, and all SAT solvers I could find are having trouble with it:...

I asked few days ago, a question about how to transform a University Class Scheduling Problem into a Boolean Satisfiability Problem. (Class Scheduling to Boolean satisfiability [Polynomial-time r...

I have some theoretical/practical problem and I don't have clue for now on how to manage, Here it is: I create a SAT solver able to find a model when one is existing and to prove the contradictio...