Skip to main content
added 236 characters in body
Source Link
Kyle Jones
  • 8.1k
  • 2
  • 29
  • 51

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has much more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself. However, an alternative would be to notice a satisfying assignment in the usual way and then undo assignments in reverse order until a clause is left unsatisfied. You would have the same $2^n$ speedup without the clause tracking overhead.

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has much more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself.

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself. However, an alternative would be to notice a satisfying assignment in the usual way and then undo assignments in reverse order until a clause is left unsatisfied. You would have the same $2^n$ speedup without the clause tracking overhead.

added addendum about adapting a SAT solver to be a #SAT solver
Source Link
Kyle Jones
  • 8.1k
  • 2
  • 29
  • 51

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has much more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself.

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has much more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself.

Source Link
Kyle Jones
  • 8.1k
  • 2
  • 29
  • 51

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.