13 Result(s)
within
English
Computer Science
Artificial Intelligence
Logics and Meanings of Programs
Chu-Min Li
Chapter
-
Chapter and Conference Paper
Incremental MaxSAT Reasoning to Reduce Branches in a Branch-and-Bound Algorithm for MaxClique
When searching for a maximum clique of a graph using a branch-and-bound algorithm, it is usually believed that one should minimize the set of branching vertices from which search is necessary. It this paper, w...
-
Chapter and Conference Paper
Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability
Variable properties such as score and age are used to select a variable to flip. The score of a variable x refers to the decrease in the number of unsatisfied clauses if x is flipped. The age of x refers to the n...
-
Chapter and Conference Paper
Satisfying versus Falsifying in Local Search for Satisfiability
During local search, clauses may frequently be satisfied or falsified. Modern SLS algorithms often exploit the falsifying history of clauses to select a variable to flip, together with variable properties such...
-
Chapter and Conference Paper
Analyzing the Instances of the MaxSAT Evaluation
The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: ...
-
Chapter and Conference Paper
Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation
We define a new heuristic that guides the application of cycle resolution (CR) in MaxSAT, and show that it produces better lower bounds than those obtained by applying CR exhaustively as in Max-DPLL, and by ap...
-
Chapter and Conference Paper
Switching among Non-Weighting, Clause Weighting, and Variable Weighting in Local Search for SAT
One way to design a local search algorithm that is effective on many types of instances is allowing this algorithm to switch among heuristics. In this paper, we refer to the way in which non-weighting algorithm a...
-
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
A Two-Level Search Strategy for Packing Unequal Circles into a Circle Container
We propose a two-level search strategy to solve a two dimensional circle packing problem. At the first level, a good enough packing algorithm called A1.0 uses a simple heuristic to select the next circle to be pa...
-
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...
-
Chapter and Conference Paper
ProQuery: Logical access to an OODB
