![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Chapter and Conference Paper
A Tableau Calculus for Non-clausal Maximum Satisfiability
We define a non-clausal MaxSAT tableau calculus. Given a multiset o...
-
Chapter and Conference Paper
On Inconsistent Clause-Subsets for Max-SAT Solving
Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to find conflicts and to quickl...
-
Chapter and Conference Paper
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensu...
-
Chapter and Conference Paper
Characterizing SAT Problems with the Row Convexity Property
Using the literal encoding of the satisfiability problem (SAT) as a binary constraint satisfaction problem (CSP), we relate the path consistency concept and the row convexity of CSPs with the inference rules i...
-
Chapter and Conference Paper
A Hybrid Approach for SAT
Exploiting variable dependencies has been shown very useful in local search algorithms for SAT. In this paper, we extend the use of such dependencies by hybridizing a local search algorithm, Walksat, and the D...
-
Chapter and Conference Paper
Look-ahead versus look-back for satisfiability problems
CNF propositional satisfiability (SAT) is a special kind of the more general Constraint Satisfaction Problem (CSP). While lookback techniques appear to be of little use to solve hard random SAT problems, it is...