Boolean satisfiability algorithm heuristics - Revision history

69.151.176.180: /* Variable State Independent Decaying Sum */ I changed an incorrect subject-verb agreement

2025-03-20T22:30:55Z

Variable State Independent Decaying Sum: I changed an incorrect subject-verb agreement

← Previous revision		Revision as of 22:30, 20 March 2025
Line 21:		Line 21:
	An influential heuristic called Variable State Independent Decaying Sum (VSIDS) attempts to score each variable. VSIDS starts by looking at small portions of the Boolean expression and assigning each phase of a variable (a variable and its negated complement) a score proportional to the number of clauses that variable phase is in. As VSIDS progresses and searches more parts of the Boolean expression, periodically, all scores are divided by a constant. This discounts the effect of the presence of variables in earlier-found clauses in favor of variables with a greater presence in more recent clauses. VSIDS will select the variable phase with the highest score to determine where to branch.		An influential heuristic called Variable State Independent Decaying Sum (VSIDS) attempts to score each variable. VSIDS starts by looking at small portions of the Boolean expression and assigning each phase of a variable (a variable and its negated complement) a score proportional to the number of clauses that variable phase is in. As VSIDS progresses and searches more parts of the Boolean expression, periodically, all scores are divided by a constant. This discounts the effect of the presence of variables in earlier-found clauses in favor of variables with a greater presence in more recent clauses. VSIDS will select the variable phase with the highest score to determine where to branch.

	VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.		VSIDS is quite effective because the scores of variable phases are independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.

	== Stochastic solvers ==		== Stochastic solvers ==

JCW-CleanerBot: task, replaced: journal=Journal on Satisfiability Boolean Modeling and Computation (JSAT) → journal=Journal on Satisfiability Boolean Modeling and Computation

2025-03-09T02:21:20Z

task, replaced: journal=Journal on Satisfiability Boolean Modeling and Computation (JSAT) → journal=Journal on Satisfiability Boolean Modeling and Computation

← Previous revision		Revision as of 02:21, 9 March 2025
Line 1:		Line 1:
	In [[computer science]], there are certain classes of algorithms ([[Heuristic (~~computer_science~~)\|heuristics]]) that solves types of the [[Boolean satisfiability problem]] despite there being [[P versus NP problem\|no known efficient algorithm]] in the general case.		In [[computer science]], there are certain classes of algorithms ([[Heuristic (computer science)\|heuristics]]) that solves types of the [[Boolean satisfiability problem]] despite there being [[P versus NP problem\|no known efficient algorithm]] in the general case.

	== Overview ==		== Overview ==

	The Boolean satisfiability (or SAT) problem can be stated formally as:		The Boolean satisfiability (or SAT) problem can be stated formally as:
	given a Boolean expression <Math>B</Math> with <Math>V = \{v_0, \ldots , v_n\}</Math> variables, finding an assignment <Math>V^</Math> of the variables such that <Math>B(V^)</Math> is true. It is seen as the canonical [[NP-complete]] problem. Although no known algorithm is known to solve SAT in polynomial time, there are classes of SAT problems which do have efficient algorithms that solve them.		given a Boolean expression <Math>B</Math> with <Math>V = \{v_0, \ldots , v_n\}</Math> variables, finding an assignment <Math>V^</Math> of the variables such that <Math>B(V^)</Math> is true. It is seen as the canonical [[NP-complete]] problem. Although no known algorithm is known to solve SAT in polynomial time, there are classes of SAT problems which do have efficient algorithms that solve them.

	The classes of problems amenable to SAT heuristics arise from many practical problems in [[AI planning]], [[Circuit satisfiability problem\|circuit testing]], and software verification.<ref>Aloul, Fadi A., "On Solving Optimization Problems Using Boolean Satisfiability", American University of Sharjah (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf</ref><ref name = "princeton">Zhang, Lintao. Malik, Sharad. "The Quest for Efficient Boolean Satisfiability Solvers", Department of Electrical Engineering, Princeton University. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf</ref> Research on constructing efficient SAT solvers has been based on various principles such as [[Resolution (logic)\|resolution]], search, local search and random walk, binary decisions, and Stalmarck's algorithm.<ref name = "princeton"/> Some of these algorithms are [[Deterministic algorithm\|deterministic]], while others may be [[Randomized algorithm\|stochastic]].		The classes of problems amenable to SAT heuristics arise from many practical problems in [[AI planning]], [[Circuit satisfiability problem\|circuit testing]], and software verification.<ref>Aloul, Fadi A., "On Solving Optimization Problems Using Boolean Satisfiability", American University of Sharjah (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf</ref><ref name = "princeton">Zhang, Lintao. Malik, Sharad. "The Quest for Efficient Boolean Satisfiability Solvers", Department of Electrical Engineering, Princeton University. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf</ref> Research on constructing efficient SAT solvers has been based on various principles such as [[Resolution (logic)\|resolution]], search, local search and random walk, binary decisions, and Stalmarck's algorithm.<ref name = "princeton"/> Some of these algorithms are [[Deterministic algorithm\|deterministic]], while others may be [[Randomized algorithm\|stochastic]].
Line 61:		Line 61:
	with <Math>a,a_1,a_2,\ldots,a_n</Math> being all distinct variables.		with <Math>a,a_1,a_2,\ldots,a_n</Math> being all distinct variables.

	This relaxes the problem by introducing new variables into the Boolean expression,<ref name="jsat">{{cite journal \|last1=Pipatsrisawat \|first1=Knot \|last2=Palyan \|first2=Akop \|last3=Chavira \|first3=Mark \|last4=Choi \|first4=Arthur \|last5=Darwiche \|first5=Adnan \|title=Solving Weighted Max-SAT Problems in a Reduced Search Space: A Performance Analysis \|journal=Journal on Satisfiability Boolean Modeling and Computation ~~(JSAT)~~ \|date=2008 \|volume=4(2008) \|page=4 \|url=http://reasoning.cs.ucla.edu/fetch.php?id=86&type=pdf \|access-date=18 April 2022 \|publisher=UCLA}}</ref> which has the effect of removing many of the constraints in the expression. Because any assignment of variables in <Math>B</Math> can be represented by an assignment of variables in <Math>B^</Math>, the minimization and maximization of the weights of <Math>B^</Math> represent lower and upper bounds on the minimization and maximization of the weights of <Math>B</Math>.		This relaxes the problem by introducing new variables into the Boolean expression,<ref name="jsat">{{cite journal \|last1=Pipatsrisawat \|first1=Knot \|last2=Palyan \|first2=Akop \|last3=Chavira \|first3=Mark \|last4=Choi \|first4=Arthur \|last5=Darwiche \|first5=Adnan \|title=Solving Weighted Max-SAT Problems in a Reduced Search Space: A Performance Analysis \|journal=Journal on Satisfiability Boolean Modeling and Computation \|date=2008 \|volume=4(2008) \|page=4 \|url=http://reasoning.cs.ucla.edu/fetch.php?id=86&type=pdf \|access-date=18 April 2022 \|publisher=UCLA}}</ref> which has the effect of removing many of the constraints in the expression. Because any assignment of variables in <Math>B</Math> can be represented by an assignment of variables in <Math>B^</Math>, the minimization and maximization of the weights of <Math>B^</Math> represent lower and upper bounds on the minimization and maximization of the weights of <Math>B</Math>.

	=== Partial Max-SAT ===		=== Partial Max-SAT ===

WikiCleanerBot: v2.05b - Bot T20 CW#61 - Fix errors for CW project (Reference before punctuation)

2024-11-19T03:59:52Z

v2.05b - Bot T20 CW#61 - Fix errors for CW project (Reference before punctuation)

← Previous revision		Revision as of 03:59, 19 November 2024
Line 12:		Line 12:
	== Branching heuristics in conflict-driven algorithms ==		== Branching heuristics in conflict-driven algorithms ==

	One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]]<ref name = "princeton"/>. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.		One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]].<ref name = "princeton"/> The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.

	=== Early branching Heuristics ===		=== Early branching Heuristics ===
Line 25:		Line 25:
	== Stochastic solvers ==		== Stochastic solvers ==

	For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is		For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms.<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref> If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is
	:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.		:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.
	This is because each variable in <Math>c</Math> has probability {{sfrac\|1\|2}} of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so		This is because each variable in <Math>c</Math> has probability {{sfrac\|1\|2}} of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so
Line 68:		Line 68:
	== Data structures for storing clauses ==		== Data structures for storing clauses ==

	As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used <ref name = "princeton"/>.		As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used.<ref name = "princeton"/>

	Expressions can be stored as a list of clauses, where each clause is a list of variables, much like an [[adjacency list]]. Though these data structures are convenient for manipulation (adding elements, deleting elements, etc.), they rely on many pointers, which increases their memory overhead, decreases [[cache locality]], and increases [[cache misses]], which renders them impractical for problems with large clause counts and large clause sizes.		Expressions can be stored as a list of clauses, where each clause is a list of variables, much like an [[adjacency list]]. Though these data structures are convenient for manipulation (adding elements, deleting elements, etc.), they rely on many pointers, which increases their memory overhead, decreases [[cache locality]], and increases [[cache misses]], which renders them impractical for problems with large clause counts and large clause sizes.

Beland: convert special characters found by Wikipedia:Typo Team/moss (via WP:JWB)

2024-11-14T05:26:40Z

convert special characters found by Wikipedia:Typo Team/moss (via WP:JWB)

← Previous revision		Revision as of 05:26, 14 November 2024
Line 27:		Line 27:
	For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is		For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is
	:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.		:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.
	This is because each variable in <Math>c</Math> has probability ½ of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so		This is because each variable in <Math>c</Math> has probability {{sfrac\|1\|2}} of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so
	: Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.		: Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.

	Now we show that randomly assigning variable values is a ½-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and		Now we show that randomly assigning variable values is a {{sfrac\|1\|2}}-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and

	: <math>\delta_{ij} = \begin{cases}		: <math>\delta_{ij} = \begin{cases}

Genusfour: clean up language and references

2024-11-07T05:21:09Z

clean up language and references

← Previous revision		Revision as of 05:21, 7 November 2024
Line 1:		Line 1:
			In [[computer science]], there are certain classes of algorithms ([[Heuristic (computer_science)\|heuristics]]) that solves types of the [[Boolean satisfiability problem]] despite there being [[P versus NP problem\|no known efficient algorithm]] in the general case.
⚫	The [[Boolean satisfiability ~~problem]]~~ (~~frequently abbreviated~~ SAT) can be stated formally as:
⚫	given a Boolean expression <Math>B</Math> with <Math>V = \{v_0, \ldots , v_n\}</Math> variables, finding an assignment <Math>V^</Math> of the variables such that <Math>B(V^)</Math> is true. It is seen as the canonical [[NP-complete]] problem. ~~While~~ no ~~efficient~~ algorithm is known to solve ~~this problem~~ in ~~the~~ ~~general case~~, there are ~~certain~~ ~~[[heuristic]]s,~~ ~~informally~~ ~~called~~ ~~'rules~~ of ~~thumb'~~ in ~~programming,~~ that ~~can usually help~~ solve ~~the~~ ~~problem reasonably efficiently.~~

			== Overview ==
⚫	~~Although no known algorithm is known to solve SAT in polynomial time, there are~~ classes of ~~SAT~~ problems ~~which~~ do ~~have~~ ~~efficient algorithms that solve them. These classes of problems~~ arise from many practical problems in [[AI planning]], [[Circuit satisfiability problem\|circuit testing]], and software verification.<ref>Aloul, Fadi A., "On Solving Optimization Problems Using Boolean Satisfiability", American University of Sharjah (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf</ref><ref name = "princeton">Zhang, Lintao. Malik, Sharad. "The Quest for Efficient Boolean Satisfiability Solvers", Department of Electrical Engineering, Princeton University. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf</ref> Research on constructing efficient SAT solvers has been based on various principles such as [[Resolution (logic)\|resolution]], search, local search and random walk, binary decisions, and Stalmarck's algorithm.<ref name = "princeton"/> Some of these algorithms are [[Deterministic algorithm\|deterministic]], while others may be [[Randomized algorithm\|stochastic]].

		⚫	The Boolean satisfiability (or SAT) problem can be stated formally as:
		⚫	given a Boolean expression <Math>B</Math> with <Math>V = \{v_0, \ldots , v_n\}</Math> variables, finding an assignment <Math>V^</Math> of the variables such that <Math>B(V^)</Math> is true. It is seen as the canonical [[NP-complete]] problem. Although no known algorithm is known to solve SAT in polynomial time, there are classes of SAT problems which do have efficient algorithms that solve them.

		⚫	The classes of problems amenable to SAT heuristics arise from many practical problems in [[AI planning]], [[Circuit satisfiability problem\|circuit testing]], and software verification.<ref>Aloul, Fadi A., "On Solving Optimization Problems Using Boolean Satisfiability", American University of Sharjah (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf</ref><ref name = "princeton">Zhang, Lintao. Malik, Sharad. "The Quest for Efficient Boolean Satisfiability Solvers", Department of Electrical Engineering, Princeton University. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf</ref> Research on constructing efficient SAT solvers has been based on various principles such as [[Resolution (logic)\|resolution]], search, local search and random walk, binary decisions, and Stalmarck's algorithm.<ref name = "princeton"/> Some of these algorithms are [[Deterministic algorithm\|deterministic]], while others may be [[Randomized algorithm\|stochastic]].

	As there exist polynomial-time algorithms to convert any Boolean expression to [[conjunctive normal form]] such as [[Tseytin transformation\|Tseitin's algorithm]], posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process.<ref name = "princeton"/>		As there exist polynomial-time algorithms to convert any Boolean expression to [[conjunctive normal form]] such as [[Tseytin transformation\|Tseitin's algorithm]], posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process.<ref name = "princeton"/>
Line 8:		Line 12:
	== Branching heuristics in conflict-driven algorithms ==		== Branching heuristics in conflict-driven algorithms ==

		⚫	One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]]<ref name = "princeton"/>. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.
	Source:<ref name = "princeton"/>

			=== Early branching Heuristics ===
⚫	One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]]. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.

	~~Early~~ ~~branching~~ ~~Heuristics~~ (Bohm's Heuristic, Maximum Occurrences on Minimum sized clauses heuristic, and Jeroslow-Wang heuristic) can be regarded as [[greedy algorithms]]. Their basic premise is to choose a free variable assignment that will satisfy the most already unsatisfied clauses in the Boolean expression. However, as Boolean expressions get larger, more complicated, or more structured, these heuristics fail to capture useful information about these problems that could improve efficiency; they often get stuck in local maxima or do not consider the distribution of variables. Additionally, larger problems require more processing, as the operation of counting free variables in unsatisfied clauses dominates the run-time.		Heuristics such as Bohm's Heuristic, Maximum Occurrences on Minimum sized clauses heuristic, and Jeroslow-Wang heuristic can be regarded as [[greedy algorithms]]. Their basic premise is to choose a free variable assignment that will satisfy the most already unsatisfied clauses in the Boolean expression. However, as Boolean expressions get larger, more complicated, or more structured, these heuristics fail to capture useful information about these problems that could improve efficiency; they often get stuck in local maxima or do not consider the distribution of variables. Additionally, larger problems require more processing, as the operation of counting free variables in unsatisfied clauses dominates the run-time.

			=== Variable State Independent Decaying Sum ===
	~~Another~~ heuristic called Variable State Independent Decaying Sum (VSIDS) attempts to score each variable. VSIDS starts by looking at small portions of the Boolean expression and assigning each phase of a variable (a variable and its negated complement) a score proportional to the number of clauses that variable phase is in. As VSIDS progresses and searches more parts of the Boolean expression, periodically, all scores are divided by a constant. This discounts the effect of the presence of variables in earlier-found clauses in favor of variables with a greater presence in more recent clauses. VSIDS will select the variable phase with the highest score to determine where to branch.		An influential heuristic called Variable State Independent Decaying Sum (VSIDS) attempts to score each variable. VSIDS starts by looking at small portions of the Boolean expression and assigning each phase of a variable (a variable and its negated complement) a score proportional to the number of clauses that variable phase is in. As VSIDS progresses and searches more parts of the Boolean expression, periodically, all scores are divided by a constant. This discounts the effect of the presence of variables in earlier-found clauses in favor of variables with a greater presence in more recent clauses. VSIDS will select the variable phase with the highest score to determine where to branch.

	VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.		VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.
Line 20:		Line 25:
	== Stochastic solvers ==		== Stochastic solvers ==

	~~Source:~~<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>		For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is
			:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.
			This is because each variable in <Math>c</Math> has probability ½ of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so
			: Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.

		⚫	Now we show that randomly assigning variable values is a ½-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and
	[[MAX-SAT]] (the version of SAT in which the number of satisfied clauses is maximized) solvers can also be solved using probabilistic algorithms. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, has a chance of being satisfied by a particular variable assignment Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>. This is because each variable in <Math>c</Math> has <Math>\frac{1}{2}</Math> probability of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works <Math>\forall ~\|c\| \geq 1</Math>, so Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.

⚫	Now we show that randomly assigning variable values is a ~~<Math>\frac{1}{2}</Math>~~-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and

	: <math>\delta_{ij} = \begin{cases}		: <math>\delta_{ij} = \begin{cases}
Line 30:		Line 36:
	1 &\text{if } c_i \text{ is not satisfied}. \end{cases}</math>		1 &\text{if } c_i \text{ is not satisfied}. \end{cases}</math>

			then we have that
	: <Math>		: <Math>
	\begin{align}		\begin{align}
Line 39:		Line 46:
	This algorithm cannot be further optimized by the [[PCP theorem]] unless P = NP.		This algorithm cannot be further optimized by the [[PCP theorem]] unless P = NP.

	Other ~~Stochastic~~ SAT solvers, such as [[WalkSAT]] and [[GSAT]] are an improvement to the above procedure. They start by randomly assigning values to each variable and then traverse the given Boolean expression to identify which variables to flip to minimize the number of unsatisfied clauses. They may randomly select a variable to flip or select a new random variable assignment to escape local maxima, much like a [[simulated annealing]] algorithm.		Other stochastic SAT solvers, such as [[WalkSAT]] and [[GSAT]] are an improvement to the above procedure. They start by randomly assigning values to each variable and then traverse the given Boolean expression to identify which variables to flip to minimize the number of unsatisfied clauses. They may randomly select a variable to flip or select a new random variable assignment to escape local maxima, much like a [[simulated annealing]] algorithm.

	== Weighted SAT problems ==		== Weighted SAT problems ==
Line 61:		Line 68:
	== Data structures for storing clauses ==		== Data structures for storing clauses ==

		⚫	As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used <ref name = "princeton"/>.
	Source:<ref name = "princeton"/>

⚫	As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used.

	Expressions can be stored as a list of clauses, where each clause is a list of variables, much like an [[adjacency list]]. Though these data structures are convenient for manipulation (adding elements, deleting elements, etc.), they rely on many pointers, which increases their memory overhead, decreases [[cache locality]], and increases [[cache misses]], which renders them impractical for problems with large clause counts and large clause sizes.		Expressions can be stored as a list of clauses, where each clause is a list of variables, much like an [[adjacency list]]. Though these data structures are convenient for manipulation (adding elements, deleting elements, etc.), they rely on many pointers, which increases their memory overhead, decreases [[cache locality]], and increases [[cache misses]], which renders them impractical for problems with large clause counts and large clause sizes.

David Eppstein: unsourced, misplaced, not a heuristic, and confusingly written

2024-04-17T06:26:56Z

unsourced, misplaced, not a heuristic, and confusingly written

← Previous revision		Revision as of 06:26, 17 April 2024
Line 40:		Line 40:

	Other Stochastic SAT solvers, such as [[WalkSAT]] and [[GSAT]] are an improvement to the above procedure. They start by randomly assigning values to each variable and then traverse the given Boolean expression to identify which variables to flip to minimize the number of unsatisfied clauses. They may randomly select a variable to flip or select a new random variable assignment to escape local maxima, much like a [[simulated annealing]] algorithm.		Other Stochastic SAT solvers, such as [[WalkSAT]] and [[GSAT]] are an improvement to the above procedure. They start by randomly assigning values to each variable and then traverse the given Boolean expression to identify which variables to flip to minimize the number of unsatisfied clauses. They may randomly select a variable to flip or select a new random variable assignment to escape local maxima, much like a [[simulated annealing]] algorithm.

	== 2-SAT heuristics ==

	Unlike general SAT problems, [[2-SAT]] problems are [[Tractable problem\|tractable]]. There exist algorithms that can compute the satisfiability of a 2-SAT problem in polynomial time. This is a result of the constraint that each clause has only two variables, so when an algorithm sets a variable <Math>v_i</Math>, the satisfaction of clauses, which contain <Math>v_i</Math> but are not satisfied by that variable assignment, depend on the satisfaction of the second variable in those clauses, which leaves only one possible assignment for those variables.

	=== Backtracking ===

	Suppose we{{who?\|date=November 2018}} are given a Boolean expressions:

	: <Math>B_1 = (v_3 \lor \neg v_2) \wedge (\neg v_1 \lor \neg v_3)</Math>

	: <Math>B_2 = (v_3 \lor \neg v_2) \wedge (\neg v_1 \lor \neg v_3) \wedge (\neg v_1 \lor v_2). </Math>

	With <Math>B_1</Math>, the algorithm can select <Math>v_1 = \text{true}</Math>, so to satisfy the second clause, the algorithm will need to set <Math>v_3 = \text{false}</Math>, and resultantly to satisfy the first clause, the algorithm will set <Math>v_2 = \text{false}</Math>.

	If the algorithm tries to satisfy <Math>B_2</Math> in the same way it tried to solve <Math>B_1</Math>, then the third clause will remain unsatisfied. This will cause the algorithm to backtrack and set <Math>v_1 = \text{false}</Math> and continue assigning variables further.

	=== Graph reduction ===

	Source:<ref>Griffith, Richard. "Strongly Connected Components and the 2-SAT Problem in Dart". http://www.greatandlittle.com/studios/index.php?post/2013/03/26/Strongly-Connected-Components-and-the-2-SAT-Problem-in-Dart</ref>

	2-SAT problems can also be reduced to running a [[depth-first search]] on a [[strongly connected components]] of a graph. Each variable phase (a variable and its negated complement) is connected to other variable phases based on implications. In the same way when the algorithm above tried to solve

	: <Math>B_1, v_1 = \text{true} \implies v_3 = \text{false} \implies v_2 = \text{false} \implies v_1 = \text{true}.</Math>

	However, when the algorithm tried solve

	: <Math>
	\begin{align}
	B_2, v_1 = \text{true} & \implies v_3 = \text{false} \implies v_2 = \text{false} \\ & \implies v_1 = \text{false} \implies \cdots \implies v_1 = \text{true},
	\end{align}
	</Math>

	which is a contradiction.

	Once a 2-SAT problem is reduced to a graph, then if a depth first search finds a strongly connected component with both phases of a variable, then the 2-SAT problem is not satisfiable. Likewise, if the depth first search does not find a strongly connected component with both phases of a variable, then the 2-SAT problem is satisfiable.

	== Weighted SAT problems ==		== Weighted SAT problems ==

RJFJR: /* Graph reduction Griffith, Richard. "Strongly Connected Components and the 2-SAT Problem in Dart". http://www.greatandlittle.com/studios/index.php?post/2013/03/26/Strongly-Connected-Components-and-the-2-SAT-Problem-in-Dart */ move ref out of heading

2023-12-21T17:18:11Z

Graph reduction Griffith, Richard. "Strongly Connected Components and the 2-SAT Problem in Dart". http://www.greatandlittle.com/studios/index.php?post/2013/03/26/Strongly-Connected-Components-and-the-2-SAT-Problem-in-Dart: move ref out of heading

← Previous revision		Revision as of 17:18, 21 December 2023
Line 57:		Line 57:
	If the algorithm tries to satisfy <Math>B_2</Math> in the same way it tried to solve <Math>B_1</Math>, then the third clause will remain unsatisfied. This will cause the algorithm to backtrack and set <Math>v_1 = \text{false}</Math> and continue assigning variables further.		If the algorithm tries to satisfy <Math>B_2</Math> in the same way it tried to solve <Math>B_1</Math>, then the third clause will remain unsatisfied. This will cause the algorithm to backtrack and set <Math>v_1 = \text{false}</Math> and continue assigning variables further.

			=== Graph reduction ===
⚫	~~=== Graph reduction~~ <ref>Griffith, Richard. "Strongly Connected Components and the 2-SAT Problem in Dart". http://www.greatandlittle.com/studios/index.php?post/2013/03/26/Strongly-Connected-Components-and-the-2-SAT-Problem-in-Dart</ref> ~~===~~

		⚫	Source:<ref>Griffith, Richard. "Strongly Connected Components and the 2-SAT Problem in Dart". http://www.greatandlittle.com/studios/index.php?post/2013/03/26/Strongly-Connected-Components-and-the-2-SAT-Problem-in-Dart</ref>

	2-SAT problems can also be reduced to running a [[depth-first search]] on a [[strongly connected components]] of a graph. Each variable phase (a variable and its negated complement) is connected to other variable phases based on implications. In the same way when the algorithm above tried to solve		2-SAT problems can also be reduced to running a [[depth-first search]] on a [[strongly connected components]] of a graph. Each variable phase (a variable and its negated complement) is connected to other variable phases based on implications. In the same way when the algorithm above tried to solve

RJFJR: /* Data structures for storing clauses */ move ref out of heading

2023-12-21T17:17:42Z

Data structures for storing clauses: move ref out of heading

← Previous revision		Revision as of 17:17, 21 December 2023
Line 93:		Line 93:
	Partial Max-SAT can be solved by first considering all of the hard clauses and solving them as an instance of SAT. The total maximum (or minimum) weight of the soft clauses can be evaluated given the variable assignment necessary to satisfy the hard clauses and trying to optimize the free variables (the variables that the satisfaction of the hard clauses does not depend on). The latter step is an implementation of Max-SAT given some pre-defined variables. Of course, different variable assignments that satisfy the hard clauses might have different optimal free variable assignments, so it is necessary to check different hard clause satisfaction variable assignments.		Partial Max-SAT can be solved by first considering all of the hard clauses and solving them as an instance of SAT. The total maximum (or minimum) weight of the soft clauses can be evaluated given the variable assignment necessary to satisfy the hard clauses and trying to optimize the free variables (the variables that the satisfaction of the hard clauses does not depend on). The latter step is an implementation of Max-SAT given some pre-defined variables. Of course, different variable assignments that satisfy the hard clauses might have different optimal free variable assignments, so it is necessary to check different hard clause satisfaction variable assignments.

	== Data structures for storing clauses <ref name = "princeton"/> ==		== Data structures for storing clauses ==

			Source:<ref name = "princeton"/>

	As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used.		As SAT solvers and practical SAT problems (e.g. circuit verification) get more advanced, the Boolean expressions of interest may exceed millions of variables with several million clauses; therefore, efficient data structures to store and evaluate the clauses must be used.

RJFJR: /* Stochastic solvers Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf */ move ref out of heading

2023-12-21T17:17:21Z

Stochastic solvers Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf: move ref out of heading

← Previous revision		Revision as of 17:17, 21 December 2023
Line 18:		Line 18:
	VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.		VSIDS is quite effective because the scores of variable phases is independent of the current variable assignment, so backtracking is much easier. Further, VSIDS guarantees that each variable assignment satisfies the greatest number of recently searched segments of the Boolean expression.

	== Stochastic solvers <ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref> ==		== Stochastic solvers ==

			Source:<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>

	[[MAX-SAT]] (the version of SAT in which the number of satisfied clauses is maximized) solvers can also be solved using probabilistic algorithms. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, has a chance of being satisfied by a particular variable assignment Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>. This is because each variable in <Math>c</Math> has <Math>\frac{1}{2}</Math> probability of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works <Math>\forall ~\|c\| \geq 1</Math>, so Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.		[[MAX-SAT]] (the version of SAT in which the number of satisfied clauses is maximized) solvers can also be solved using probabilistic algorithms. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, has a chance of being satisfied by a particular variable assignment Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>. This is because each variable in <Math>c</Math> has <Math>\frac{1}{2}</Math> probability of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works <Math>\forall ~\|c\| \geq 1</Math>, so Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.

RJFJR: /* Branching heuristics in conflict-driven algorithms */ move ref out of heading

2023-12-21T17:17:03Z

Branching heuristics in conflict-driven algorithms: move ref out of heading

← Previous revision		Revision as of 17:17, 21 December 2023
Line 6:		Line 6:
	As there exist polynomial-time algorithms to convert any Boolean expression to [[conjunctive normal form]] such as [[Tseytin transformation\|Tseitin's algorithm]], posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process.<ref name = "princeton"/>		As there exist polynomial-time algorithms to convert any Boolean expression to [[conjunctive normal form]] such as [[Tseytin transformation\|Tseitin's algorithm]], posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process.<ref name = "princeton"/>

	== Branching heuristics in conflict-driven algorithms <ref name = "princeton"/> ==		== Branching heuristics in conflict-driven algorithms ==

			Source:<ref name = "princeton"/>

	One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]]. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.		One of the cornerstone [[Conflict-Driven Clause Learning]] SAT solver algorithms is the [[DPLL algorithm]]. The algorithm works by iteratively assigning free variables, and when the algorithm encounters a bad assignment, then it backtracks to a previous iteration and chooses a different assignment of variables. It relies on a Branching Heuristic to pick the next free variable assignment; the branching algorithm effectively makes choosing the variable assignment into a decision tree. Different implementations of this heuristic produce markedly different decision trees, and thus have significant effect on the efficiency of the solver.

← Previous revision		Revision as of 05:26, 14 November 2024
Line 27:		Line 27:
	For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is		For [[MAX-SAT]], the version of SAT in which the number of satisfied clauses is maximized, solvers also use probabilistic algorithms<ref>Sung, Phil. "Maximum Satisfiability" (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf</ref>. If we are given a Boolean expression <Math>B</Math>, with <Math>V = \{v_0, \ldots , v_n\}</Math> variables and we set each variable randomly, then each clause <Math>c</Math>, with <Math>\|c\|</Math> variables, then the chance of <math>B</math> being satisfied by a particular variable assignment is
	:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.		:Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|}</Math>.
	This is because each variable in <Math>c</Math> has probability ½ of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so		This is because each variable in <Math>c</Math> has probability {{sfrac\|1\|2}} of being satisfied, and we only need one variable in <Math>c</Math> to be satisfied. This works for all <Math> \|c\| \geq 1</Math>, so
	: Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.		: Pr(<Math>c</Math> is satisfied) = <Math>1-2^{-\|c\|} \geq \frac{1}{2}</Math>.

	Now we show that randomly assigning variable values is a ½-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and		Now we show that randomly assigning variable values is a {{sfrac\|1\|2}}-approximation algorithm, which means that is an optimal approximation algorithm unless P = NP. Suppose we are given a Boolean expression <Math>B = \{c_i\}_{i=1}^n</Math> and

	: <math>\delta_{ij} = \begin{cases}		: <math>\delta_{ij} = \begin{cases}