Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

learn more… | top users | synonyms (1)

4
votes
2answers
53 views

Interesting small SAT problems?

I'm noodling around with making a hardware SAT solver on an FPGA, and I'm wondering if there are any interesting SAT problems smaller than, say, 50 variables both to stay within the limits of the FPGA ...
1
vote
1answer
35 views

How exactly does a Max 2 Sat reduce to a 3 Sat?

I've been reading this article which tries and explains how the max 2 sat problem is essentially a 3-sat problem and is NP-hard. However, if you see the article, I'm not able to understand why, after ...
4
votes
1answer
45 views

What happens to uninterpreted predicates in Ackermann's reduction?

I know the procedure to apply the Ackermann's reduction to a formula that doesn't involve uninterpreted predicates. But, how do we treat the uninterpreted boolean predicates? Nearly all the examples I ...
1
vote
0answers
24 views

Complexity Measure and Practical Hardness of SAT

I am study this paper "Relating Proof Complexity Measures and Practical Hardness of SAT". Here the authors propose to use pebble formulas to find a relation between these and practical SAT ...
1
vote
0answers
10 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
-1
votes
1answer
97 views

How can one reduce 3-CNF-SAT and k-CNF-SAT to each other?

I am studying for NP problems. To prove k-CNF-SAT is NP-hard, there must exists something that can be reduced to k-CNF-SAT. So what I thought is to reduce 3-CNF-SAT to k-CNF-SAT and reduce k-CNF-SAT ...
1
vote
1answer
32 views

What's non-algorithm-specific

I am reading the paper "Understanding Random SAT beyond the Clauses-to-Variables Ratio" and at beginning of the page 2 say the hardest region corresponds exactly to a phase transition in a ...
1
vote
1answer
64 views

NP to SAT. How does it works? [closed]

Let's start here: It is said that all NP problems can be reduced to SAT(boolean satisfiability problem). To be more accurate to Circuit SAT, because all decision problems like NP should end up with ...
0
votes
1answer
47 views

How can you check if a 2SAT problem has a bad loop

im trying to figure out why this is true The clauses {a,b}, {b,~c}, {c,~a} constitute a 2SAT problem with an implication graph without bad loops. Can someone show me how to illustrate this and ...
1
vote
2answers
83 views

Find hamilton cycle in a directed graph reduced to sat problem

I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...
1
vote
0answers
30 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
2
votes
1answer
27 views

Schaefer's dichotomy theorem and reformulating 3-literal clauses

Does Schaefer's dichotomy theorem establish that a general 3-sat clause cannot be transformed into an equivalent set of 2-sat/Hornsat/affine clauses (using auxiliary variables) or just that this would ...
1
vote
1answer
40 views

Non-deterministic algorithms and Tautologies

I am studying the lecture The Complexity of Propositional Proofs. ​Here there is a definition together with a discussion (page 3). I don't understand that discussion. Let $F$ denote the set of ...
0
votes
0answers
61 views

Step by step of a modification of the Beame-Pitassi Algorithm

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
1
vote
1answer
21 views

Strahler of tree like refutations

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
2
votes
1answer
34 views

The Space of an Unsatisfiable Formula

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to ...
1
vote
0answers
36 views

How to get all tree-like refutations of a formula

I need to extract all tree-like refutations of this formula $$(a+b)(a+ b')(a'+c)(a'+c')\,.$$ I get understand this one but how do I get the other ones?
2
votes
1answer
35 views

Measuring the hardness of SAT instances Lemma

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF).I have two questions ...
3
votes
1answer
51 views

What does a square mean in a Boolean formula

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF) and I would like to ...
5
votes
0answers
71 views

Any Natural Problems shown Easy by Reduction to Horn SAT?

To show that a problem is polynomial-time solvable, an often-successful technique is to reduce it to 2SAT (that is the problem of deciding satisfiability of CNF formulas with every clause containing ...
1
vote
1answer
68 views

Half-SAT intractability proof

I've been struggling lately with a problem that was in my last complex algorithms exam, and I can't find a solution. The problem is as follows: Half-SAT is a problem where C is a CNF boolean ...
5
votes
1answer
60 views

Complexity of black box satisfiablty

Say I have a black box $f : 2^n \to 2$ and I want to determine if it is satisfiable. That is, does there exist an input how which it returns true. I am for the purposes of this considering $n$ to be ...
1
vote
0answers
84 views

DPLL time complexity analysis

Consider the most naïve backtracking for CNF-SAT. It only checks if an assignment satisfies the input formula $\phi$ when all the $n$ variables have values assigned. Let $m$ be the size of $\phi$. ...
1
vote
1answer
29 views

Shaefer's Dichotomy Theorem [duplicate]

Could you please resolve a confusion with Schaefer's theorem for me? Namely, why does it not imply many problems in P are NP-complete? For example, primality testing surely cannot be reduced to one of ...
4
votes
0answers
70 views

“Balancing” positive and negative literals in 2-sat

I saw in an answer to this post that it is possible to construct 3-sat clauses with extra variables such that the number of positive and negative literals for each variable are equal. Does anyone ...
2
votes
1answer
91 views

Complexity of a SAT related problem

Given a set of (propositional) formulae $\Phi$, two formulae $\phi$ and $\xi$, determine whether there exists $\Psi\subseteq \Phi$ such that $\Psi\models \phi$ and $\Psi\not\models \xi$. Question: ...
6
votes
1answer
84 views

Is weighted XOR-SAT NP-hard?

Given $n$ boolean variables $x_1,\ldots,x_n$ each of which is assigned a positive cost $c_1,\ldots,c_n\in\mathbb{Z}_{>0}$ and a boolean function $f$ on these variables given in the form ...
10
votes
1answer
1k views

Why do Shaefer's and Mahaney's Theorems not imply P = NP?

I'm sure someone has thought about this before or immediately dismissed it, but why does Schaefer's dichotomy theory along with Mahaney's theorem on sparse sets not imply P = NP ? Here's my ...
0
votes
1answer
61 views

Can Tarjan's SCC algorithm find satisfying assignment to just 'any' digraph?

Is Tarjan's algorithm capable of finding satisfying assignment to any digraph consists of variables (vertices) and implications (edges)? I know that it solves implication graphs constructed by 2SAT ...
8
votes
2answers
94 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
100 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
1answer
112 views

Can Circuit Value Problem or HORN-SAT be reduced to PATH problem?

PATH = {(X,R,S,T) | exists an x in S that is admissible} Where R is a relation of X x X x X, S is a unary relation of X and T is a unary relation of X aswell. An x element of X is admissible if it is ...
0
votes
0answers
20 views

Arthur-Merlin protocol to decide a set size

Please look at the example here at the bottom of page 3, http://www.cs.nyu.edu/~khot/CSCI-GA.3350-001-2014/sol3.pdf Here it seems that the set whose size Arthur is trying to approximate is known in ...
2
votes
0answers
28 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
2
votes
1answer
91 views

The initial NP-complete problem

It is always claimed that Cook and Levin gives the very first NP-complete problem and proof of it. But when I look at the actual proof I think what Cook and Levin did was reduced (or transformed) SAT ...
7
votes
2answers
726 views

Why does Schaefer's theorem not prove that P=NP?

This is probably a stupid question, but I just don't understand. In another question they came up with Schaefer's dichotomy theorem. To me it looks like it proves that every CSP problem is either in P ...
2
votes
2answers
175 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 ...
6
votes
3answers
249 views

Is 2-SAT with XOR-relations NP-complete?

I'm wondering if there is a polynomial algorithm for "2-SAT with XOR-relations". Both 2-SAT and XOR-SAT are in P, but is its combination? Example Input: 2-SAT part: ...
2
votes
1answer
39 views

If in all satisfying assignments all pair of variables can take all possible values is this tautology?

I suppose this is both easy and false. Let $\phi$ be propositional boolean formula on variables $x_1 \ldots x_n$. Suppose in all satisfying assignments of $\phi$, all pairs of variables $(x_i,x_j),i ...
2
votes
1answer
89 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 ...
2
votes
1answer
51 views

How does derandomization of 3SAT work via conditional expectations?

Given a single SAT clause with its 3 literals coming from 3 different variables it is obvious that a random assignment of values will satisfy it with probability 7/8 But I do not understand how ...
-1
votes
1answer
304 views

How to prove a Double CNF SAT is in NP [duplicate]

So I've been stuck trying to figure this problem out for a while. I've looked on wikis and all over stack exchange but I'm really stumped. This isn't my best subject, so any sort of explanation would ...
-1
votes
1answer
97 views

Restricted version fo CNF-SAT

Given formula $\phi$ on CNF-form in CNF-SAT. Clauses can be arbitrarily long. The problem is NP-complete and it is also given that part of the problem is that a variable can occur many times in a ...
3
votes
0answers
89 views

smallest satisfiability-equivalent formulas (generalized Tseitin transform)?

What is known about the following optimization problem for formulas in propositional logic: input: formula $F$ output: formula $G$ in CNF with $\mathrm{Var}(G) \supseteq \mathrm{Var}(F)$ such that ...
7
votes
2answers
107 views

Switching Lemma and AC0 reductions between SAT problems

Have there been efforts to show (using the Switching Lemma), for example, that SAT or 3SAT cannot have an AC$^0$ reduction to 2SAT? What are the issues or difficulties involved? SAT and 3SAT are ...
2
votes
1answer
75 views

How to choose between several constraints for a SAT task using quality metric?

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 ...
1
vote
0answers
23 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
7
votes
2answers
567 views

Is generalized XOR-SAT efficiently solvable?

I've seen how XOR-3-SAT is efficiently solvable (for instance, see the "XOR-satisfiability" section in the Wikipedia entry for Boolean satisfiability problem). I'm wondering a basic question: Is ...
7
votes
1answer
535 views

DNF to CNF conversion: Easy or Hard

In relation to the thread CNF to DNF — conversion is NP Hard (and a related Math thread): How about the other direction, from DNF to CNF? Is it easy or hard? On Page 2 of this paper, they seem to ...
2
votes
1answer
87 views

Constructing solution to 3SAT formulas using oracle queries [duplicate]

I'm interested in 3SAT and querying an oracle. Suppose we had an oracle that can decide, on an input boolean formula $\phi$, whether there exists any assignment to the variables that makes the formula ...