Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

Filter by
Sorted by
Tagged with
1 vote
1 answer
40 views

prove that if $SAT\notin Size(2^{n/100})$ then CorrectSATSolver$\in P$

I need to prove that if $SAT\notin Size(2^{n/100})$ then CorrectSATSolver$\in P$. Where CorrectSATSolver $= \{C | C(\varphi) = 1 \iff \varphi$ is satisfiable$\}$. In other words, CorrectSATSolver ...
user avatar
  • 23
0 votes
0 answers
15 views

How overapproximation of boolean abstraction function works?

I just found that if original formula is unsat, using boolean abstraction function can result in sat. Clearly this is overapproximate. I wonder if I have contingent formula, does that means my boolean ...
user avatar
4 votes
1 answer
68 views

What are efficient approaches to implement unit propagation in DPLL-based SAT solvers?

I'm trying to decompose deduction steps of DPLL algorithm -- unit propagation and pure literal elimination -- for parallelization. However, I want a baseline and asymptotic analysis to compare to my ...
user avatar
  • 43
2 votes
0 answers
28 views

Quantum Boolean SAT algorithm?

Is there a quantum SAT algorithm, a quantum analogue of the DPLL or CDCL algorithms? Note: I'm not looking for the quantum analogue of the Boolean satisfiability problem (though that would be ...
user avatar
  • 145
2 votes
1 answer
33 views

How to determine if clause will change the satisfiability of the 3SAT formula?

I have satisfiable 3SAT formula like: (x1 or x2 or x3) and (not x1 or x2 or not x3) and some clause which is not in this formula ...
user avatar
3 votes
1 answer
42 views

Stalmarck's method: x ≡ x → z, does z have to be true?

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that: y $\to$ z $\equiv$ x where x, y and z are booleans which ...
user avatar
  • 53
2 votes
0 answers
33 views

Non-trivial reduction form SAT to $3$-SAT

Looking for any idea for reduction from $SAT \leq 3-SAT$ where $SAT$ is known to have $d$ variables at most in each clause. I am looking for a reduction in which the resulting formula will not depend ...
user avatar
6 votes
1 answer
84 views

Why is this SAT problem hard and what can I do about it?

For a graph theory problem I need to solve hundreds of millions of CNF problems that typically have around 200 variables and 15,000 clauses no larger than 10. By default I use glucose, which usually ...
user avatar
0 votes
0 answers
14 views

Getting maximum information regarding question key from students answers

You are given a multi-dimensional array with each index consisting of two attributes (Score, Answers) Each element in the array represents the test results of a student on a True or False exam. Each ...
user avatar
1 vote
1 answer
32 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 ...
user avatar
  • 2,820
0 votes
0 answers
23 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 ...
user avatar
1 vote
0 answers
121 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 ...
user avatar
  • 71
1 vote
1 answer
52 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$?
user avatar
  • 13
1 vote
0 answers
55 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 ...
user avatar
2 votes
1 answer
52 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 ...
user avatar
  • 359
1 vote
2 answers
210 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 ...
user avatar
3 votes
1 answer
43 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 ...
user avatar
  • 213
11 votes
3 answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
user avatar
2 votes
1 answer
69 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 ...
user avatar
0 votes
1 answer
316 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 ...
user avatar
3 votes
1 answer
91 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 ...
user avatar
  • 677
4 votes
2 answers
311 views

Is it feasible to solve this subset cover problem with SAT solver?

The problem is to find $\mathcal{S}$, a minimal collect of subsets of $\{1,\dots, 17\}$ such that the two conditions are satisfied: if $S \subseteq \mathcal{S}$ then $|S|=6$; for any $A \subseteq \{1,...
user avatar
  • 549
3 votes
1 answer
65 views

CNF satisfiability with a bound on number of clauses

Consider the CNF-sat problem with n literals and k clauses. If k scales linearly in n, we get np-completeness (e.g., 3-sat where each literal appears at most 4 times). Do we still get np-completeness ...
user avatar
  • 131
3 votes
1 answer
318 views

Practical hard 3-sat instances

The $3-SAT$ problem is known to be NP-complete problem. Which means that (as far as I understand), unless $P \neq NP$, for every algorithm $A$ which decides $3-SAT$, $A$ runs in super polynomial time (...
user avatar
2 votes
1 answer
70 views

Non-Boolean SAT

I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
user avatar
7 votes
1 answer
765 views

Random restarts for unsatisfiable instances

In the worst case, Boolean satisfiability (assuming P!=NP) takes exponential time. Nonetheless, modern SAT solvers using variants of DPLL, are able to solve enough instances to be useful in practice. ...
user avatar
  • 386
1 vote
1 answer
77 views

Can an optimization algorithm be "universal"?

I am wondering if a Bayesian Optimization framework (e.g. Google's Vizier) can be used in lieu of a traditional solver like Gurobi or CPLEX. In trying to answer this question, I realized that I don'...
user avatar
3 votes
1 answer
187 views

Sum of unique integers to cnf constraint

As a study project I try to solve the kakuro puzzle problem using SAT SOLVER. I can't really find an efficient way to convert the sum of k unique integers (1...9) to a CNF constraint. What I had in ...
user avatar
  • 209
0 votes
1 answer
96 views

Encoding a "not-k-out-of-n" constraint for SAT solvers

I'm finding myself needing to encode a "not-k-out-of-n" constraint in a SAT solver. The "at-most-k-out-of-n" constraint for SAT solvers is something I can find research about -- this paper by Frisch ...
user avatar
  • 183
3 votes
0 answers
171 views

Determine if a graph has exactly 1 cycle using a SAT solver

I have a connected undirected graph whose edges are either enabled or disabled. I want to create a set of clauses that are SAT iff all enabled edges are part of a single loop. If I assert that each ...
user avatar
4 votes
0 answers
59 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
user avatar
  • 243
2 votes
1 answer
42 views

Translation of diagnosis problem to SAT

I have the following diagnosis problem: h(A): z1 = not(in1) h(D): z2 = not(in2) h(B): z3 = z1 or z2 h(C): out1 = not(z3) h(E): out2 = not(z3) This is an image of the system: I have an observation ...
user avatar
  • 123
0 votes
1 answer
139 views

Fine-grained complexity of 3-CNF formula evaluation

It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed ...
user avatar
1 vote
1 answer
74 views

Why not do these checks on the number of clauses in 3-SAT?

I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious ...
user avatar
  • 113
3 votes
1 answer
281 views

Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3

I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language). The proposed solution was: ...
user avatar
2 votes
2 answers
406 views

Is any sudoku solver an SAT solver?

I have recently created a sudoku solver using C#, which outputs the solution to a sudoku after a reasonable amount of time in many cases. I have used the basic sudoku SAT-reduction (i.e. x111 meaning ...
user avatar
1 vote
0 answers
146 views

General Understanding of SMT Solving Across Multiple Theories

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
user avatar
  • 1,853
3 votes
1 answer
533 views

How the Abstract DPLL Algorithm Works in SAT Solving

I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with ...
user avatar
  • 1,853
-2 votes
1 answer
250 views

How a SMT / SAT Solver Generates Valuations for this Example

First, an example of a set of constraints which turned out not to be solvable (I don't think): ...
user avatar
  • 1,853
1 vote
1 answer
242 views

Counting solutions of a particular type in HORN SAT

I am interested in counting the number of solutions of a particular type (say #) in HORN SAT. I have 2 questions concerning the same. Suppose we have a HORN SAT -: $(x_1) \land (x_2 \implies x_1)$, ...
user avatar
0 votes
1 answer
67 views

How to find a nearly-optimal covering of a set using SAT?

I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem. I think one of the interesting problems where SAT ...
user avatar
  • 153
3 votes
0 answers
124 views

How hard is APPROXIMATE-#SAT? [closed]

It is well known that the problem of counting the satisfying assignments of SAT, namely the problem #SAT, is #P-complete. It is also suspected (somewhat less widely) that even deciding SAT should ...
user avatar
  • 31
0 votes
1 answer
269 views

SAT solver optimizations of DPLL for unsatisfiable formulas [duplicate]

I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is ...
user avatar
3 votes
1 answer
181 views

If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?

If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?
user avatar
2 votes
1 answer
226 views

What is the complexity of determining Satisfiability of a CNF containing both Horn and Dual Horn clauses?

If a CNF contains both horn and dual horn clauses and does not contain clauses of other types, then can its Satisfiability always be determined in polynomial time? If the answer to the above problem ...
user avatar
2 votes
1 answer
2k views

Bit Blasting Algorithm

I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example: Assume our bit-vectors ...
user avatar
  • 637
0 votes
0 answers
151 views

When to use SAT vs solving?

Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver? Is there any guidance anyone can offer about which ...
user avatar
  • 101
0 votes
1 answer
143 views

Another way to solve SAT. Was it known?

Theorem. If and only if SAT instance $\varphi$ is satisfiable, there is a way to negate variables in $\varphi$ and get $\varphi'$ where all clauses have at least one positive literal. Also we can ...
user avatar
  • 1,371
1 vote
1 answer
1k 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 ...
user avatar
3 votes
2 answers
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 ...
user avatar