# Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

88 questions
Filter by
Sorted by
Tagged with
20 views

### Three dimensional matching expressed as SAT

The posting in the website Embedding SATISFIABILITY into 3-DIMENSIONAL MATCHING seeks $3SAT$ as a $3$ dimensional matching instance. I am looking to solve the converse problem. How to solve three ...
18 views

### SAT solvers that can compute prime implicants and/or minimization

I'm looking into computing the prime implicants of a Boolean function. I have found many different algorithms in the literature, many of them relying on SAT solvers. However, I have not been able to ...
92 views

### Which features can be considered for neural network based SAT solving?

I'm trying to implement SAT solver, based on backtracking algorithm and BCP. This SAT solver is trying to pick one literal from each clause, from 3-CNF SAT instances. I've implemented a neural network ...
18 views

### Proving using a SAT solver that KB entails D

Suppose you're given this KB: $$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$ How would you show using a SAT solver that $KB \vDash D$?
52 views

### How often can a learned clause cause this solver to backtrack?

The is an improvement to the X3SAT solver I described in What is wrong with this simple proof of P=NP? I have fixed the flaw found in that solver. Now, I want to know how often the solver described ...
45 views

### Solving largely monotone SAT formulas

I just wonder if solving largely monotone SAT formulas (meaning most clauses do not contain negated literals, but some do) is in any way easier than general SAT formulas? In other words, are there ...
115 views

### Is there any algorithm for 3SAT problem that is fast and relatively easy to implement?

Here is the description for 3SAT satisfiability problem. I already know about the DPLL algorithm, but it's implementation is pretty complex. I would like some algorithm that is relatively simpler but ...
38 views

### How to leverage the fact that I'm solving 1000's of very similar SMT instances?

I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array. Then, my program takes as input k << 100,000 new clauses, and adds ...
2k views

### Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
53 views

### Find a list of actions that result in desired state

I have a problem that I need to solve, and I'm looking for which area of computer science (algorithms. etc) would be appropriate to solve this problem. In the system we have a list of actions that a ...
157 views

### What are the differences between symbolic execution and SAT solvers?

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the ...
76 views

### Clarification on "clause learning" in DPLL algorithm

I am struggling to understand the idea of conflict-driven clause learning, in particular, I can not understand why the clause we 'learned' is a substantially new (i.e. the clause database does not ...
240 views

858 views

### Is this possible to solve SAT in polynomial time by reducing it to the problem of solving system of nonlinear equations?

Every conjunctive normal form (CNF) formula can be converted to nonlinear system of equations, where each clause becomes an equation in the system and: If A and B are logical/boolean variables and ...
2k views

### CSP Forward checking with n-ary (and binary) constraints

I have implemented my own CSP solver using a Backtracking algorithm. Within the Backtracking algorithm I apply a Forward Checking algorithm (reducing domains of connected, unnasigned variables) that ...
549 views

### Is this possible to solve 4SAT in polynomial time? [closed]

I know and admit that this is long, but please read it slow and understand everything. I think that this is one of the most interesting questions asked in computer science ever. I don't expect for ...
1k views

### Is this possible to solve 3SAT in O(n^24) time and O(1) space?

Assume that n is the number variables of the given 3CNF formula (n≥3) and all clauses in the given 3CNF formula are different. That means that for each clause, each literal can be either positive ...
114 views

### These sample CNF formulas in DIMACS files are in P? (Schaefer's dichotomy theorem)

Here is my earlier question. But there was no full answer. I've decided to include specific DIMACS files: http://jarvis2.hmcloud.pl/sat/cnf.formula.10 (15.8MB) http://jarvis2.hmcloud.pl/sat/cnf....
483 views

### What's the average number of clauses modern SAT solvers can handle?

It's already known that size doesn't matter always (for SAT problems). But is there evidence (from real data from: benchmarks or real cases) on how many clauses an average SAT solver can handle ...
619 views

### Why do all recent SAT solvers work on CNF instead of circuit SAT?

After the release of the AIGER library to handle and-inverter graphs sometime in 2006 (I think), some circuit SAT solvers were released in 2006-2008, and in a few SAT Races/Competitions there were AIG ...
125 views

### Logical formula in DIMACS, SAT, Schaefer's dichotomy theorem and software to test it

I have a very complicated formula logical (CNF) in the file DIMACS. The question is as follows. The formula has hundreds of millions of clauses (assume billion) and a lot of variables. It is a ...
695 views

### Deterministic SAT solver

I have the following question. Is the SAT solvers are deterministic? I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic? If these algorithms will return unSAT ...