Questions regarding solver programs for the boolean satisfiability problem.

learn more… | top users | synonyms

5
votes
1answer
30 views

Why is pure literal elimination absent in DPLL-based algorithms like Chaff?

I'm looking into various SAT-solvers and trying to understand how they work and why they are designed in certain ways. (But I'm not in a university at the moment and I do not know anyone who is a ...
8
votes
2answers
78 views

Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
6
votes
1answer
40 views

Conflict Driven Clause Learning backtracking clarification

On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack ...
1
vote
0answers
14 views

A query regarding the Max3SAT Approximation Algorithm's Application

Its known that a polynomial time Approximation Algorithm that satisfies 3MaxSAT in 7/8+e clauses implies P=NP. If given that the given 3MaxSAT is satisfiable, it is still difficult to find a 7/8+e ...
2
votes
2answers
92 views

Why don't modern SAT solvers use the notion of a “watched clause”, in the same way they use the notion of a “watched literal”?

Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched ...
2
votes
1answer
42 views

Basic question about backjumping in SAT solvers

I am reading "Formalization and Implementation of Modern SAT Solvers", by Filip Marić. My question is about how backjumping is defined. In an example [1], there is a conflict clause C equal to ...
3
votes
1answer
62 views

Are there any open source SAT solvers with UNSAT core extraction algorithm built in?

Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose ...
1
vote
1answer
28 views

How is the complexity of algorithms to solve 3CNF (decision problem) specified? [duplicate]

For k inputs, the complexity of naive algorithm is O(2^k). I understood this one. What is meant by "the size of the instance to be solved should be polynomial in k". Is it equivalent to the statement ...
0
votes
1answer
56 views

SAT for arithmetic

Given two integers $X$ and $Y$, each can be encoded in binary $X=(x_4 x_3 x_2 x_1)$ and $Y=(y_4 y_3 y_2 y_1)$, how do I encode the constraint $$|X-Y|\geq n \quad\text{and}\quad|X-Y|= n$$ when $n$ is ...
6
votes
2answers
74 views

Common method for solving satisfiability problems which lie in P

I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific ...
0
votes
1answer
44 views

Constrain certain variables in CNF to unique satisfying assignments

[Reposted because the original question was deleted by the poster.] I'm looking for a way to add additional clauses (and maybe additional variables) to an already existing SAT instance so that ...
1
vote
0answers
19 views

SMT solves with functions for free varibles

So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions ...
5
votes
1answer
84 views

Why is DPLL better than brute force?

I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course ...
2
votes
1answer
45 views

Sound and complete algorithms for boolean satifiability

To my best knowledge, these are the sound and complete algorithms for boolean satisfiability Variations of DPLL algorithm (e.g. CDCL, Look-ahead solvers) Stalmarks method Binary Decision Diagram ...
10
votes
3answers
118 views

Recipe book for SAT encodings?

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific ...
4
votes
3answers
149 views

Detection of redundant boolean constraints

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin ...
5
votes
0answers
68 views

Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
3
votes
1answer
104 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
1
vote
1answer
84 views

Fast Consequence FInders

I have been struggling in the search for a modern fast "consequence finder". That is, an implementation based on state-of-the-art theory; things of the ilk of Z3, Prover9, OTTER, etc. To describe ...
10
votes
3answers
183 views

Multicore SAT Solver

I am trying to solve a 25k clauses 5k variables SAT problem. As it has been running for an hour (precosat) and I'd like to solve bigger ones afterwards, I'm looking for a multi-core SAT-Solver. As ...
5
votes
2answers
138 views

Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer. Can you do better than ...
3
votes
0answers
93 views

Why Is Alloy not an Answer Set Programming system?

Alloy's front page doesn't mention ASP, but the description sounds like ASP (finding solutions consistent with a logical spec). And Alloy isn't listed in the Wikipedia ASP article. Yet ASP systems ...
10
votes
1answer
616 views

Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest ...
6
votes
1answer
254 views

When to use SAT vs Constraint Satisfaction?

If I have a hard problem, one standard approach is to express it as a SAT instance and try running a SAT solver on it. Another standard approach is to express it as a constraint satisfaction problem, ...
4
votes
2answers
1k views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
6
votes
2answers
166 views

Complexity of GF(2) and applications to cryptography

If I have a system of N polynomial equations with N unknowns in GF(2): What are some good methods to solve them? What are some software packages or libraries that implement this? What's the highest ...
9
votes
1answer
240 views

Unification vs. SAT solver

I read on Wikipedia that unification is a process of solving the satisfability problem. At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
7
votes
2answers
249 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
5
votes
1answer
203 views

Running time of CDCL compared to DPLL

What's the complexity of Conflict-Driven Clause Learning SAT solvers, compared to DPLL solvers? Was it proven that CDCL is faster in general? Are there instances of SAT that are hard for CDCL but easy ...
10
votes
1answer
284 views

Can top SAT-solvers factor easy numbers?

Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA ...
4
votes
1answer
317 views

Resolution complexity versus a constrained SAT algorithm

EDIT: ad hoc speed-ups are excluded. We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a ...
4
votes
1answer
1k views

Forward checking vs arc consistency on 3-SAT

If I were to let the variables be the propositions and, constraint be all clauses being satisfied, which technique would be more effective in solving 3-SAT? Forward checking or arc consistency? From ...
10
votes
1answer
1k views

Proving that the conversion from CNF to DNF is NP-Hard

How can I prove that the conversion from CNF to DNF is NP-Hard? I'm not asking for an answer, just some suggestions about how to go about proving it.