Stack Overflow
Stack Overflow

Questions tagged [sat-solvers]

SAT solvers are a class of algorithms for solving satisfiability problem of boolean formulas.

SAT solvers are a class of algorithms for solving satisfiability problem of boolean formulas.

SAT was the first known example of an NP-complete problem. Since then, there are a lot of research regarding how to efficiently solve a large enough subset of SAT instances to be useful in various practical areas.

References:

80 questions
11
votes
1 answer

SAT solving with more than 2^32 clauses

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: (P)lingeling reports that there are "too many…
Dominik Peters
  • 230
  • 1
  • 8
9
votes
1 answer

(get-unsat-core) returns empty in Z3

I am using Z3 to extract the unsat-core of an unsatisfiable formula. I am using Z3@Rise interface (web based) to write the following code, (set-logic QF_LIA) (set-option :produce-unsat-cores true) (declare-fun ph1 () Int) (declare-fun ph1p ()…
chinu
  • 239
  • 2
  • 6
7
votes
1 answer

Interpretation of Z3 Statistics

I obtained several statistics from runs of Z3. I need to understand what these mean. I am rather rusty and non up to date for the recent developments of sat and SMT solving, for this reason I tried to find explanations myself and I might be dead…
gapag
  • 71
  • 3
6
votes
1 answer

Incremental SMT solver with ability to drop specific constraint

Is there an incremental SMT solver or an API for some incremental SMT solver where I can add constraints incrementally, where I can uniquely identify each constraint by some label/name? The reason I want to identify the constraints uniquely is so…
srg
  • 265
  • 2
  • 8
5
votes
2 answers

Determine upper/lower bound for variables in an arbitrary propositional formula

Given an arbitrary propositional formula PHI (linear constraints on some variables), what is the best way to determine the (approximate) upper and lower bound for each variable? Some variables may be unbounded. In this case, an algorithm should…
liyistc
  • 83
  • 1
  • 5
5
votes
2 answers

Looking for practical examples of SMT Z3 usecases (like DbC) and open source alternative to Z3?

I have got interested in and looking for practical examples of SMT Z3 usage (like DbC) with code and open source alternatives to this tool. So, in fact, I am interested in similar Z3 formal solving tools, but: it must be open source provide both…
Yauhen Yakimovich
  • 13,635
  • 8
  • 60
  • 67
5
votes
3 answers

Input CNF for SAT4J solver

I a totally new to sat4j solver.. it says some cnf file should be given as input is there any possible way to give the rule as input and get whether it is satisfiable or not? my rule will be of the kind : Problem = ( ( staff_1 <=> …
karthi
  • 2,762
  • 4
  • 30
  • 28
5
votes
1 answer

Z3py: Convert a Z3 formula to clauses used by picosat

LINKS: Z3 theorem prover picosat with pyhton bindings I've used Z3 as a SAT-solver. For larger formulae there seem to be performance issues which is why I wanted to check out picosat to see whether it's a faster alternative. My existing python code…
mrsteve
  • 4,082
  • 1
  • 26
  • 63
4
votes
1 answer

Z3 giving unsat result for equation Solving

Given a set of possible values for each variable and two equations, I wrote the below code to get the exact variable values. But Z3 is giving Unsat results. I have created 7 instances and combined them to make a single one. And passed the instance…
Sumana bagchi
  • 55
  • 3
4
votes
1 answer

Solving using DPLL sat solver

I found a sat solver in http://code.google.com/p/aima-java/ I tried the following code to solve an expression using dpllsolver the input is (A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E)) CNF transformer…
karthi
  • 2,762
  • 4
  • 30
  • 28
4
votes
1 answer

How to install a minizinc solver

In MiniZinc (windows IDE) How can I resolve: flatzinc: error: variables of type `var float' are not supported by the FD solver backend. I realize I need a different solver but could not find a procedure installing one and the Preferences dlg does…
Jim Lewis
  • 349
  • 2
  • 14
4
votes
2 answers

Learning material on SAT (Boolean Satisfiability Problem)

What are good documents to read on SAT (Boolean satisfiability problem) solvers. I have not been able to find good material via Google. The documents I found were either birds eye view, too advanced or corrupted PDF files... Which papers/documents…
Jules
  • 6,318
  • 2
  • 29
  • 40
4
votes
1 answer

improving performance of a dpll algorithm

I'm implementing a DPLL algorithm in C++ as described in wikipedia: function DPLL(Φ) if Φ is a consistent set of literals then return true; if Φ contains an empty clause then return false; for every unit clause l in Φ Φ…
none
  • 11,793
  • 9
  • 51
  • 87
3
votes
1 answer

Wrong result from z3

I'm trying to proof the following with Z3 SMT Solver: ((x*x) + x) = ((~x * ~x) + ~x). This is correct, because of overflow semantic in the c programming language. Now I have written the following smt-lib code: (declare-fun a () Int) (define-fun…
Thomas
  • 31
  • 1
3
votes
1 answer

Is there way to give input as normal expression to Z3 Solver?

The Z3 input format is an extension of the one defined by SMT-LIB 2.0 standard. The input expressions need to write in prefix form. As for example rise4fun, x + (y * 2) = 20 needs to be given input in the form of " (= (+ x (* 2 y)) 20)) ". Z3…
Rituraj Singh
  • 579
  • 1
  • 5
  • 16
1
2 3 4 5 6