Questions tagged [sat-solvers]

Questions regarding solver programs for the boolean satisfiability problem.

Filter by
Sorted by
Tagged with
0 votes
0 answers
35 views

resolving in CDCL

When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
-1 votes
1 answer
31 views

Can you help me find some examples of 3co-SAT for 4 variables?

I've been studying the examples of 3co-SAT recently. It's easy to find an example of one variable. $(x_1\lor x_1\lor x_1)\land (\overline{x_1}\lor \overline{x_1}\lor \overline{x_1})$ Examples of 2 ...
  • 161
1 vote
2 answers
49 views

what does **input** mean for the $3SAT$ question? Is it the number of variables $n$ or the number of clauses $m$

We know that $3SAT \in NP$, and the definition of $NP$ is as follows: $NP$ is the class of languages that have polynomial time verifiers. But I have a question: what does input mean for the $3SAT$ ...
  • 161
0 votes
1 answer
66 views

Time-complexity of evaluating a CNF formula

Given a Boolean formula over $n$ variables in CNF and a partial assignment to it, all the algorithms I can think of to evaluate the assignment run in time $\Theta(n^2)$. Is it possible to do it in $O(...
1 vote
1 answer
39 views

MAX-SAT 2-Approximation algorithm

I have the two following questions: I know SAT -> MAX-SAT but how can I show that if MAX-SAT is solved in polynomial time then SAT is solved in polynomial time as well?(I guess using approximation ...
  • 37
1 vote
1 answer
41 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 ...
  • 23
0 votes
0 answers
19 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 ...
4 votes
1 answer
109 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 ...
  • 43
2 votes
0 answers
36 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 ...
  • 145
2 votes
1 answer
42 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 ...
3 votes
1 answer
46 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 ...
  • 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 ...
6 votes
1 answer
96 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 ...
0 votes
0 answers
15 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 ...
1 vote
1 answer
36 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 ...
  • 2,824
0 votes
0 answers
25 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 ...
1 vote
0 answers
130 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 ...
  • 71
1 vote
1 answer
55 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$?
  • 13
1 vote
0 answers
57 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 ...
2 votes
1 answer
54 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 ...
  • 359
1 vote
2 answers
240 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 ...
3 votes
1 answer
46 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 ...
  • 213
12 votes
4 answers
2k views

Are there competitions for integer programming?

Are there competitions for integer programming like there are for SAT and MAXSAT?
2 votes
1 answer
77 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 ...
0 votes
1 answer
384 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 ...
3 votes
1 answer
94 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 ...
  • 677
4 votes
2 answers
328 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,...
  • 549
3 votes
1 answer
71 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 ...
  • 131
3 votes
1 answer
385 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 (...
2 votes
1 answer
85 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 ...
7 votes
1 answer
779 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. ...
  • 386
1 vote
1 answer
85 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'...
3 votes
1 answer
208 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 ...
  • 209
0 votes
1 answer
103 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 ...
  • 183
3 votes
0 answers
181 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 ...
4 votes
0 answers
61 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 ...
  • 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 ...
  • 123
0 votes
1 answer
146 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 ...
1 vote
1 answer
77 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 ...
  • 113
3 votes
1 answer
297 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: ...
2 votes
2 answers
420 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 ...
1 vote
0 answers
151 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 ...
  • 1,911
3 votes
1 answer
549 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 ...
  • 1,911
-2 votes
1 answer
253 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): ...
  • 1,911
1 vote
1 answer
249 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)$, ...
0 votes
1 answer
69 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 ...
  • 153
3 votes
0 answers
131 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 ...
  • 31
0 votes
1 answer
280 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 ...
3 votes
1 answer
186 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?
2 votes
1 answer
230 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 ...