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)

3
votes
0answers
26 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
70 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
58 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
16 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 ...
4
votes
2answers
361 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
274 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
31 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 ...
-2
votes
0answers
24 views

Polynomial verifier in computation theory (Schedule Problem)

P is an integer and M a matrix such as M ∈ {0,1}^k×m, M(i,j) = 1 signifies that a student i is inscribed in the activity j question: is there a Schedule at most P period that allows us to place ...
-2
votes
1answer
38 views

Proof of Circuit-Sat to Nand-Sat polynomial time many–one reducibility

Given a gate called Nand with the following truth table: A | B | A Nand B ------------------ 0 | 0 | 1 0 | 1 | 1 1 | 0 | 1 1 | 1 | 0 We can ...
3
votes
1answer
45 views

Understanding terms related to 2SAT algorithm [closed]

Recently I am learning about solution of the 2-satiability problem using strongly connected components. There is a theorem related to this problem given below: Let $F = Q_lx_1 Q_2x_2\ldots Q_nx_n C$ ...
-4
votes
1answer
29 views

Complexity if special case of SAT

I have the following problem: How to show that the special case of SAT, in which each clause has either exactly two literals or at most one negative literal, is NP-complete?
2
votes
1answer
64 views

Are there name and literature for this SAT-like problem?

Given $f : \{0,1\}^* \to \{0,1\}$ and $n \in \mathbb{N}$, we define $\textsf{Prob}(f,n)$ as the following problem: Find an $x \in \{0,1\}^n$ such that $f(x) = 1$. A machine solving ...
3
votes
3answers
306 views

The relation between 2SAT and 3SAT

Show that proving 2SAT is not NP-Complete would prove that 3SAT is not in P. Or eqivalently - Show that proving 3SAT is in P would prove that 2SAT is NP-Complete. I can see there is an ...
3
votes
1answer
32 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
18 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 ...
4
votes
1answer
130 views

Algorithm for a special case of SAT/#SAT

Does anyone know of an algorithm that can solve the following special case of SAT in polynomial time? Are there any algorithms that can solve the counting (#SAT) version of it in polynomial time? ...
0
votes
1answer
49 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 ...
0
votes
1answer
51 views

Satisfying assignments, twice-3SAT NP complete [duplicate]

I wanted to solve the following problem about 3SAT . The question is 1. to show if the problem is NP-complete and 2. whether the problem has two different satisfying assignments. "TWICE-3SAT Input: ...
3
votes
2answers
45 views

Getting a variable assignment of a Tseitin transformed formula

Let $\phi$ be a Boolean formula and $\mathrm{Tseitin}(\phi)$ the corresponding Tseitin transformed equisatifiable formula. It is well-known that one can get a variable assignment for $\phi$ by ...
7
votes
2answers
209 views

Explaining SAT to high school science teachers

I am a high school sophomore who is interested in computer science. I developed a cool algorithm for #SAT, and I'm implementing and doing a science fair project on it. My adviser, who is the best ...
6
votes
2answers
67 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 ...
2
votes
1answer
42 views

How do I prove a certain upper bound on the runtime of a probabilistic 2-SAT solver?

As a homework we had to prove a set of upper bounds on a given probabilistic algorithm to find a satisfying assignment for a satisfiable 2-CNF formula. The problem is reproduced below. I'm sorry for ...
5
votes
2answers
191 views

Why do we care about random Boolean SAT formula?

I've been looking for a reference for the above question. As far as I know the answer is: If we can make a solver that is efficient for all randomly generated instances, it should be efficient for ...
1
vote
1answer
27 views

Hardness of 3SAT-k

According to these scribe notes (and a paper), 3SAT-5 is NP-hard. The problem is defined to be: given a 3SAT formula, each variable occurs in at most 5 clauses. It is also proven that 3SAT-4 is ...
2
votes
0answers
18 views

Applications for balanced Boolean function satisfiability

Assume the following problem: Input: A Boolean black-box $U$ of a balanced Boolean function (balanced meaning equal number of satisfying and unsatisfying truth assignments) Output: A satisfying ...
0
votes
1answer
31 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
1answer
49 views

How many satisfying assignments are there in a set of 3-CNF clauses where no clause share the same variable?

Say I have a set of 3-CNF clauses $$\mathcal{S} = \{ x_1 \vee x_2 \vee \bar{x_3}, ~~x_4 \vee x_5 \vee x_6\}$$ where $\bar{x}$ is the negation of $x$. Each variable range over $\mathbb{Z}^2$. How ...
0
votes
0answers
39 views

Is there a constant for size of disjoint clauses in 3-CNF

We are given a 3-CNF formula $\Phi$ on n variables, and a guarantee that at least $\epsilon$ fraction of $2^n$ possible assignments satisfy all clauses in $\Phi$. Now construct set $S$ of disjoint ...
0
votes
0answers
63 views

#SAT Complexity [on hold]

I have been looking at algorithms for solving #SAT and calculated that simply extending a SAT algorithm like DPLL by adding the negation of a solution to the original formula and solving again takes ...
5
votes
1answer
63 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 ...
1
vote
1answer
72 views

What complexity class is this ciruit problem?

I'm exploring an algorithm that solves k-SAT. It uses a ton of preprocessing, so I'm thinking that this will be a circuit bounds. Without knowing the runtime, I speculate on how quickly it will ...
4
votes
0answers
107 views

If one shows s that UNIQUE k-SAT is in P, does it imply P=NP?

Valiant & Vazirani proved SAT transforms UNIQUE SAT under randomized probabilistic reductions in polynomial time. Calabro et al. showed that UNIQUE k-SAT is as hard as k-SAT. Now the question is, ...
1
vote
1answer
67 views

Encoding the pigeonhole principle in CBMC

CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and ...
2
votes
1answer
43 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 ...
0
votes
1answer
42 views

Doesn't a formula that tests each boolean string of length $N$ force SAT to execute at least $2^N$ tests?

Since you are free to chose any formula for the SAT problem, doesn't the choice of a formula that requires a test for each subset of the group of variables force it to perform $2^N$, essentially ...
1
vote
0answers
32 views

infinite system MAX-SAT

Is there a generalization of maximal satisfaction (MAX-SAT) based on infinitely many variables? One natural occurrence of such problem is the general Ising model in material science.
-1
votes
1answer
33 views

Co NP problem correponding to SAT

I've been reading lately about SAT problem, NP and co-NP. Many sources say that the SAT problem is co NP, though, I can't find a co-NP problem equivalent to SAT. Does anyone have any idea about ...
9
votes
3answers
111 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 ...
1
vote
1answer
59 views

Satisfiability of first-order logic is undecidable?

I struggle with understanding why the satisfiability in the first-order logic is undecidable. Could you explain it with some examples? I've also seen that satisfiability in some first-order formulas ...
8
votes
1answer
94 views

What is the name of the problem? (partitioning graph into three covers)

I was wondering if this problem has a name: Given a simple graph whose edges are colored red, blue and green, $G=(V,B\cup R\cup G)$, is there a vertex-coloring $c:V\to \{B,R,G\}$ such that every edge ...
3
votes
1answer
131 views

Is finding a solution of a satisfiability problem harder than deciding satisfiability?

Is the problem of determining whether or not a given Boolean expression is satisfiable computationally distinct from actually finding a solution to the expression? In other words, is there another ...
4
votes
3answers
141 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 ...
2
votes
1answer
75 views

Reduce Set problem to SAT

So the problem is, given some set $M = \{x_1,x_2,\ldots,x_n\}$ and a set of subsets $S = \{S_1, S_2, \ldots, S_m\}$ where $S_i \subseteq M$. We want to find some set $X \subseteq M$ such that $|X| \le ...
3
votes
1answer
83 views

A Reduction from XORSAT to 2-SAT

Does anyone know of a non-trivial reduction from XORSAT to 2-sat since they are both in P? (By non-trivial I mean one that does not just solve the instance of XORSAT and map it to a fixed instance of ...
2
votes
1answer
203 views

Monotone boolean satisfiability with at most k 1s is NP-Complete

I am to prove that monotone boolean formula satisfiability checking when at most k variables are set to 1 is an NP-Complete problem. Proving that it is in NP is easy, but I'm having difficulty ...
-2
votes
2answers
99 views

Example for an unsatisfiable formula that can be made satisfiable by reordering quantifiers [closed]

Please give me an example of an unsatisfiable quantified 2 CNF formula. I need it in my proof and I am unable to think of one. I am looking for such an unsatisfiable quantified 2 CNF formula which ...
3
votes
1answer
103 views

Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?

Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables. Example: $\qquad ...
0
votes
1answer
67 views

Check constraint under some condition in linear programming

I would like to minimize linear pseudo-boolean function $$\mathrm{obj} = \sum_i c_i \mathrm{sel}_i$$ subject to $$\sum_i c_i sel_i \geq \mathrm{Value} \qquad\qquad(1)$$ where $c_1,\dots c_5, ...
-3
votes
1answer
49 views

Why is Mixed Quantified Horn SAT in PSPACE?

I want to prove that Mixed Quantified Horn SAT is a PSPACE-complete problem. I have proved that it is PSPACE-hard. How can I prove that it is in PSPACE? My study: To prove QSAT to be in PSPACE: ...
3
votes
1answer
59 views

Why do we assume that a nondeterministic Turing machine decides a language in NP in $n^k-3$ in Sipser's proof

At page 277 of Sipser's Introduction to the Theory of Computation, a proof of the NP-completeness of SAT is given. The following comment is made on the trace of some machine $N$ which can decide a ...